• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
        • Warnings
        • Primitives
        • Use-set
        • Syntax
        • Getting-started
        • Utilities
        • Loader
        • Transforms
        • Lint
        • Mlib
          • Scopestack
          • Filtering-by-name
          • Vl-namefactory
          • Substitution
          • Allexprs
          • Hid-tools
            • Following-hids
            • Vl-hidexpr-traverse-datatype
            • Abstract-hids
              • Vl-hidexpr-p
              • Vl-hidindex-p
              • Vl-hidexpr-collect-indices
              • Vl-hidindex->indices
              • Vl-hidexpr->rest
              • Vl-indexexpr->indices
              • Vl-hidexpr->first
              • Vl-indexexpr->scopeexpr
              • Vl-scopeexpr->scopes
              • Vl-hidname-p
              • Vl-hidexpr->endp
              • Vl-scopeexpr->hid
              • Vl-hidname->name
              • Vl-hidindex->name
              • Vl-hidindex-count-indices
              • Vl-scopeexpr-p
              • Vl-scopeatom->name
              • Vl-scopename-p
              • Vl-scopename-fix
              • Vl-indexexpr-p
              • Vl-fast-keyguts-p
              • Vl-scopeatom-p
              • Vl-scopenamelist
            • Vl-hidexpr-find-type
          • Vl-consteval
          • Range-tools
          • Lvalexprs
          • Hierarchy
          • Finding-by-name
          • Expr-tools
          • Expr-slicing
          • Stripping-functions
          • Stmt-tools
          • Modnamespace
          • Vl-parse-expr-from-str
          • Welltyped
          • Reordering-by-name
          • Flat-warnings
          • Genblob
          • Expr-building
          • Datatype-tools
          • Syscalls
          • Relocate
          • Expr-cleaning
          • Namemangle
          • Caremask
          • Port-tools
          • Lvalues
        • Server
        • Kit
        • Printer
        • Esim-vl
        • Well-formedness
      • Sv
      • Fgl
      • Vwsim
      • Vl
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Math
    • Testing-utilities
  • Hid-tools

Abstract-hids

Recognizers for certain kinds of HID expressions.

We now develop wrapper functionality that allows us to treat hierarchical, scope, and index expressions in a sensible way. Note that these are technical terms with precise meanings; see hid-tools for background.

Quick guide, working bottom up:

vl-hidname-p
A single ID or HIDPIECE atom without any indices or dots.
Examples: bar, \foo$bar
vl-hidname->name gets the name as a string.
vl-hidindex-p
A single ID with perhaps some indices.
Examples: bar, bar[1], bar[3][5].
vl-hidindex->name gets the name as a string.
vl-hidindex->indices gets the indices as an expression list.
vl-hidexpr-p
A full HID with dots and interior indices, but no "external" indices.
Examples: foo, foo.bar, foo[3].bar
vl-hidexpr->endp says whether there's a dot.
vl-hidexpr->first gets the first hidindex, e.g., foo[3] for foo[3].bar. In the endp case this is just the whole expression.
vl-hidexpr->rest gets the rest. Can't be used in the endp case.
vl-scopename-p
Name of a scope. For instance, :vl-local, :vl-$unit, or a string.
vl-scopeexpr-p
Extends hidexprs with scope operators.
Example: ape::bat::cat.dog[3].elf
vl-scopeexpr->scopes lists the scope names, e.g., ape, bat.
vl-scopeexpr->hid gets the hidexpr, i.e., cat.dog[3].elf
vl-indexexpr-p
Extends scopeexprs with indexing operators.
Example: foo::bar.baz[3][4][5]
vl-indexexpr->scopeexpr gets the scope expression.
vl-indexexpr->indices gets the indices as an expression list.

Note that none of these functions places any restrictions on the expressions that can occur in index positions. That is, expressions like foo[width-1].bar are perfectly acceptable.

Subtopics

Vl-hidexpr-p
Recognizes well-formed hierarchical identifier expressions.
Vl-hidindex-p
Recognizes well-formed index expressions into hierarchical identifier pieces, e.g., the bar[3][4][5] part of foo.bar[3][4][5].baz.
Vl-hidexpr-collect-indices
Collect all expressions from index positions in a hid expression, e.g., for foo[3][4].bar[5].baz, we would return a list of expressions for 3 4 5.
Vl-hidindex->indices
For instance, bar[3][4][5] → (3 4 5).
Vl-hidexpr->rest
Vl-indexexpr->indices
Vl-hidexpr->first
Get the leftmost vl-hidindex-p in a hid expression.
Vl-indexexpr->scopeexpr
Vl-scopeexpr->scopes
Vl-hidname-p
Recognizes simple name expression: either a hidpiece or an id.
Vl-hidexpr->endp
Vl-scopeexpr->hid
Vl-hidname->name
Get the name from a vl-hidname-p as a string.
Vl-hidindex->name
For instance, bar[3][4][5] → bar.
Vl-hidindex-count-indices
Vl-scopeexpr-p
Recognizes well-formed hierarchical scope expressions.
Vl-scopeatom->name
Vl-scopename-p
Recognizes names that can be used in scope operators.
Vl-scopename-fix
Vl-indexexpr-p
Vl-fast-keyguts-p
Vl-scopeatom-p
Vl-scopenamelist
A list of vl-scopename-p objects.