• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
      • Fgl
      • Vwsim
      • Vl
        • Syntax
          • Vl-module
          • Vl-vardecl
          • Vl-fundecl
          • Vl-interface
          • Vl-design
          • Vl-assign
          • Vl-modinst
          • Vl-gateinst
          • Vl-taskdecl
          • Vl-portdecl
          • Vl-commentmap
          • Vl-dpiimport
          • Vl-ansi-portdecl
          • Vl-package
          • Vl-paramdecl
          • Vl-dpiexport
          • Vl-class
          • Vl-sort-blockitems-aux
          • Vl-plainarglist->exprs
          • Vl-taskdecllist->names
          • Expressions-and-datatypes
            • Vl-atts
            • Vl-expr
              • Vl-expr-p
              • Vl-expr->atts
              • Vl-index
              • Vl-call
              • Vl-exprsign
              • Vl-maybe-expr
              • Vl-stream
              • Vl-expr-case
              • Vl-pattern
                • Vl-patternkey
                  • Vl-patternkey-ambiguity
                  • Vl-patternkey-case
                  • Vl-patternkey-equiv
                  • Vl-patternkey-structmem
                  • Vl-patternkey-p
                  • Vl-patternkey-expr
                  • Vl-patternkey-type
                  • Vl-patternkey-kind
                  • Vl-patternkey-default
                  • Vl-patternkey-fix
                  • Vl-patternkey-count
                • Vl-assignpat
                • Vl-pattern->pattype
                • Make-vl-pattern
                • Vl-pattern->pat
                • Vl-pattern->atts
                • Change-vl-pattern
                • Vl-keyvallist
              • Vl-literal
              • Vl-binary
              • Vl-expr-update-atts
              • Vl-unary
              • Vl-special
              • Vl-qmark
              • Vl-inside
              • Vl-cast
              • Vl-multiconcat
              • Vl-mintypmax
              • Vl-partselect-expr
              • Vl-bitselect-expr
              • Vl-tagged
              • Vl-concat
              • Vl-expr-equiv
              • Vl-eventexpr
              • Vl-expr-kind
              • Vl-exprlist
              • Vl-maybe-exprlist
              • Vl-expr-fix
              • Vl-expr-count
            • Vl-datatype
            • New-expression-representation
            • Vl-paramargs
            • Vl-evatom
            • Vl-maybe-paramargs
            • Vl-evatomlist
            • Vl-call-namedargs
            • Vl-paramvaluelist
            • Vl-namedparamvaluelist
          • Vl-fundecllist->names
          • Vl-udp
          • Vl-port
          • Vl-genelement
          • Vl-clkdecl
          • Vl-parse-temps
          • Vl-bind
          • Vl-namedarg
          • Vl-exprdist
          • Vl-clkassign
          • Vl-range
          • Vl-propport
          • Vl-typedef
          • Vl-gatedelay
          • Vl-dimension
          • Vl-sequence
          • Vl-clkskew
          • Vl-program
          • Vl-gatestrength
          • Vl-property
          • Vl-config
          • Vl-always
          • Vl-import
          • Vl-repeateventcontrol
          • Vl-timeliteral
          • Vl-initial
          • Vl-eventcontrol
          • Vl-final
          • Vl-udpsymbol-p
          • Vl-maybe-clkskew
          • Vl-function-specialization
          • Vl-alias
          • Vl-maybe-nettypename
          • Vl-maybe-gatedelay
          • Vl-letdecl
          • Vl-direction-p
          • Vl-modelement
          • Vl-maybe-timeprecisiondecl
          • Vl-maybe-scopeid
          • Vl-maybe-gatestrength
          • Vl-maybe-direction
          • Vl-maybe-delayoreventcontrol
          • Vl-gclkdecl
          • Vl-fwdtypedef
          • Vl-maybe-udpsymbol-p
          • Vl-maybe-timeunitdecl
          • Vl-maybe-timeliteral
          • Vl-maybe-parse-temps
          • Vl-maybe-cstrength
          • Vl-arguments
          • Vl-maybe-module
          • Vl-maybe-design
          • Vl-covergroup
          • Vl-udpline
          • Vl-timeunitdecl
          • Vl-genvar
          • Vl-defaultdisable
          • Vl-context1
          • Vl-timeprecisiondecl
          • Vl-sort-blockitems
          • Vl-elabtask
          • Vl-udpedge
          • Vl-delaycontrol
          • Vl-context
          • Vl-ctxelement
          • Vl-ctxelement->loc
          • Vl-modelement->loc
          • Statements
          • Vl-blockitem
          • Vl-vardecllist
          • Vl-interface->ifports
          • Vl-syntaxversion
          • Vl-nettypename-p
          • Vl-module->ifports
          • Vl-lifetime-p
          • Vl-paramdecllist
          • Vl-modelementlist->genelements
          • Vl-importlist
          • Vl-typedeflist
          • Vl-gatetype-p
          • Vl-cstrength-p
          • Vl-port->name
          • Vl-genelement->loc
          • Vl-delayoreventcontrol
          • Vl-udpentry-p
          • Vl-portdecllist
          • Vl-elabtask->loc
          • Property-expressions
          • Vl-taskdecllist
          • Vl-port->loc
          • Vl-fundecllist
          • Vl-sequencelist
          • Vl-propertylist
          • Vl-portlist
          • Vl-dpiimportlist
          • Vl-dpiexportlist
          • Vl-classlist
          • Vl-arguments->args
          • Vl-alwaystype-p
          • Vl-modinstlist
          • Vl-importpart-p
          • Vl-importpart-fix
          • Vl-bindlist
          • Vl-initiallist
          • Vl-genvarlist
          • Vl-gclkdecllist
          • Vl-function-specialization-map
          • Vl-finallist
          • Vl-elabtasklist
          • Vl-defaultdisablelist
          • Vl-clkdecllist
          • Vl-cassertionlist
          • Vl-blockstmt-p
          • Vl-assignlist
          • Vl-assertionlist
          • Vl-alwayslist
          • Vl-aliaslist
          • Vl-udptable
          • Vl-udplist
          • Vl-udpentrylist
          • Vl-propportlist
          • Vl-programlist
          • Vl-packagelist
          • Vl-namedarglist
          • Vl-modulelist
          • Vl-modportlist
          • Vl-modport-portlist
          • Vl-letdecllist
          • Vl-interfacelist
          • Vl-gateinstlist
          • Vl-fwdtypedeflist
          • Vl-covergrouplist
          • Vl-configlist
          • Vl-clkassignlist
          • Vl-blockitemlist
          • Vl-ansi-portdecllist
          • Vl-regularportlist
          • Vl-paramdecllist-list
          • Vl-modelementlist
          • Vl-interfaceportlist
          • Vl-casekey-p
          • Sv::maybe-4veclist
        • Loader
        • Warnings
        • Getting-started
        • Utilities
        • Printer
        • Kit
        • Mlib
        • Transforms
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Math
    • Testing-utilities
  • Vl-pattern

Vl-patternkey

A key in an assignment pattern.

This is a tagged union type, introduced by deftagsum.

Member Tags → Types
:expr → vl-patternkey-expr
An unambiguous array index pattern key like 5 or foo + bar.
:structmem → vl-patternkey-structmem
A struct member pattern key like opcode. Note that until annotate is done, this may be a type name which needs to be disambiguated.
:type → vl-patternkey-type
A type pattern key like integer or mytype_t.
:default → vl-patternkey-default
The special default pattern key.

A vl-patternkey represents a single key in an key/value style assignment pattern, such as:

'{ 0: a, 1: b, 2: c, default: 0 }    // assign to some array indices, default others...
'{ foo: 3, bar: 5 }                  // assign to struct members by name (maybe)
'{ integer: 5, opcode_t: 7 }         // assign to struct members by type (maybe)

These kinds of pattern keys are, in general, somewhat ambiguous and difficult to resolve until elaboration time. To avoid the worst of these ambiguities we impose certain restrictions on the kinds of assignment patterns we support; vl-patternkey-ambiguity for some notes about this.

Subtopics

Vl-patternkey-ambiguity
Notes about our handling of vl-patternkeys.
Vl-patternkey-case
Case macro for the different kinds of vl-patternkey structures.
Vl-patternkey-equiv
Basic equivalence relation for vl-patternkey structures.
Vl-patternkey-structmem
A struct member pattern key like opcode. Note that until annotate is done, this may be a type name which needs to be disambiguated.
Vl-patternkey-p
Recognizer for vl-patternkey structures.
Vl-patternkey-expr
An unambiguous array index pattern key like 5 or foo + bar.
Vl-patternkey-type
A type pattern key like integer or mytype_t.
Vl-patternkey-kind
Get the kind (tag) of a vl-patternkey structure.
Vl-patternkey-default
The special default pattern key.
Vl-patternkey-fix
Fixing function for vl-patternkey structures.
Vl-patternkey-count
Measure for recurring over vl-patternkey structures.