• 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
          • Vl-module
          • Vl-vardecl
          • Expressions
            • Vl-atts
            • Vl-constint
            • *vl-ops-table*
            • Vl-weirdint
            • Vl-expr
            • Vl-id
            • Vl-hidpiece
            • Vl-time
            • Vl-maybe-exprtype
            • Vl-op-p
            • Vl-maybe-expr
            • Vl-expr->finaltype
            • Vl-real
            • Vl-expr->finalwidth
            • Vl-tagname
            • Vl-sysfunname
            • Vl-string
            • Vl-op-arity
            • Vl-keyguts
            • Vl-exprtype-p
            • Vl-typename
            • Vl-funname
            • Vl-basictype
            • Vl-extint
            • Vl-atomlist-p
            • Vl-atomguts
            • Vl-nbits-fix
            • Vl-atom-p
            • Vl-arity-fix
            • Vl-arity-ok-p
            • Vl-op-text
            • Vl-exprlist
            • Vl-oplist
            • Vl-exprlistlist
            • Vl-ops-table
            • *vl-default-expr*
          • Vl-fundecl
          • Vl-assign
          • Vl-gateinst
          • Vl-modinst
          • Vl-commentmap
          • Vl-portdecl
          • Vl-taskdecl
          • Vl-design
          • Vl-interface
          • Vl-plainarglist->exprs
          • Vl-taskdecllist->names
          • Vl-fundecllist->names
          • Vl-package
          • Vl-port
          • Vl-udp
          • Vl-paramdecl
          • Vl-genelement
          • Vl-cycledelayrange
          • Vl-namedarg
          • Vl-sort-blockitems-aux
          • Vl-distitem
          • Vl-gatedelay
          • Vl-repetition
          • Vl-typedef
          • Vl-range
          • Vl-gatestrength
          • Vl-program
          • Vl-config
          • Vl-always
          • Vl-datatype-update-dims
          • Vl-import
          • Vl-enumbasetype
          • Vl-repeateventcontrol
          • Vl-paramargs
          • Vl-initial
          • Vl-eventcontrol
          • Vl-udpsymbol-p
          • Vl-maybe-range
          • Vl-maybe-nettypename
          • Vl-maybe-gatestrength
          • Vl-maybe-gatedelay
          • Vl-maybe-delayoreventcontrol
          • Vl-alias
          • Maybe-string-fix
          • Vl-maybe-packeddimension
          • Vl-fwdtypedef
          • Vl-evatom
          • Vl-packeddimension-p
          • Vl-maybe-udpsymbol
          • Vl-maybe-module
          • Vl-maybe-direction
          • Vl-maybe-datatype
          • Vl-maybe-cstrength
          • Vl-direction-p
          • Vl-arguments
          • Vl-maybe-design
          • Vl-udpline
          • Vl-exprdist
          • Vl-context1
          • Vl-genvar
          • Vl-enumitem
          • Vl-datatype-update-udims
          • Vl-datatype-update-pdims
          • Vl-modelement
          • Vl-udpedge
          • Vl-delaycontrol
          • Vl-context
          • Vl-sort-blockitems
          • Vl-distweighttype-p
          • Vl-ctxelement->loc
          • Vl-blockitem
          • Vl-vardecllist
          • Vl-module->ifports
          • Vl-modelement->loc
          • Vl-ctxelement
          • Vl-coretypename-p
          • Vl-packeddimensionlist
          • Vl-modelementlist->genelements
          • Vl-gatetype-p
          • Vl-paramdecllist
          • Vl-lifetime-p
          • Vl-datatype->udims
          • Vl-datatype->pdims
          • Vl-timeunit-p
          • Vl-repetitiontype-p
          • Vl-port->name
          • Vl-importlist
          • Vl-genelement->loc
          • Vl-delayoreventcontrol
          • Vl-cstrength-p
          • Statements
          • Vl-udpentry-p
          • Vl-packeddimension-fix
          • Vl-nettypename-p
          • Vl-portdecllist
          • Vl-port->loc
          • Vl-enumbasekind-fix
          • Vl-arguments->args
          • Vl-taskdecllist
          • Vl-portlist
          • Vl-importpart-p
          • Vl-importpart-fix
          • Vl-fundecllist
          • Vl-blockstmt-p
          • Vl-assignlist
          • Vl-alwaystype-p
          • Vl-typedeflist
          • Vl-syntaxversion-p
          • Vl-randomqualifier-p
          • Vl-modinstlist
          • Vl-gateinstlist
          • Vl-blockitemlist
          • Vl-udptable
          • Vl-udplist
          • Vl-udpentrylist
          • Vl-programlist
          • Vl-paramvaluelist
          • Vl-packagelist
          • Vl-namedparamvaluelist
          • Vl-namedarglist
          • Vl-modulelist
          • Vl-modportlist
          • Vl-modport-portlist
          • Vl-interfacelist
          • Vl-initiallist
          • Vl-genvarlist
          • Vl-fwdtypedeflist
          • Vl-evatomlist
          • Vl-enumitemlist
          • Vl-distlist
          • Vl-configlist
          • Vl-alwayslist
          • Vl-aliaslist
          • Vl-regularportlist
          • Vl-rangelist-list
          • Vl-rangelist
          • Vl-paramdecllist-list
          • Vl-modelementlist
          • Vl-maybe-range-list
          • Vl-interfaceportlist
          • Vl-argumentlist
          • Data-types
        • Getting-started
        • Utilities
        • Loader
        • Transforms
        • Lint
        • Mlib
        • Server
        • Kit
        • Printer
        • Esim-vl
        • Well-formedness
      • Sv
      • Fgl
      • Vwsim
      • Vl
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Math
    • Testing-utilities
  • Syntax

Expressions

Representation of Verilog expressions.

One goal of our expression representation was for the recursive structure of expressions to be as simple as possible. More specifically, I did not want to have a different representation for a unary expression than for a binary expression, etc. Instead, I just wanted each operator to take a list of arguments, each of which were themselves valid subexpressions.

Basic Terminology

Atomic Expressions

The atomic expressions are recognized by vl-atom-p. Each atomic expression includes some guts, which refer to either an:

  • vl-id-p: a simple, non-hierarchical identifier,
  • vl-constint-p: an integer literal with no X or Z bits,
  • vl-weirdint-p: an integer literal with some X or Z bits,
  • vl-extint-p: an unbased, unsized integer literal like '0 or 'x,
  • vl-real-p: a "real literal", i.e., a floating point number,
  • vl-string-p: a string literal,
  • vl-time-p: time literals like 3ns,
  • vl-keyguts-p: special atomic expressions like null, this, super, $, local, etc.
  • vl-hidpiece-p: one piece of a hierarchical identifier,
  • vl-funname-p: the name of an ordinary function, or
  • vl-sysfunname-p: the name of a system function (e.g., $display).
  • vl-basictype-p: simple type names like byte, shortint, time, logic, etc.
  • vl-tagname-p: the name of a tagged union type member.

Some of these are probably not things you would ordinarily think of as atomic expressions. However, accepting them as atomic expressions lets us achieve the straightforward recursive structure we desire.

In addition to their guts, each vl-atom-p includes a

  • finalwidth, which is a maybe-natp and
  • finaltype, which is a vl-maybe-exprtype-p.

Typically, when we have just parsed the modules, these fields are left nil: their values are only filled in during our expression typing and sizing computations.

Finally, an atom has atts, which is a vl-atts-p. These attributes are generally nil upon parsing since the Verilog or SystemVerilog grammars don't really provide anywhere for (* foo = bar, baz *) style attributes to be attached to atomic expressions. However, we occasionally find it convenient to put our own attributes on atoms, e.g., it allows us to record that a particular atom came from a parameter.

Non-Atomic Expressions

A non-atomic expression represents an operator being applied to some arguments.

Like atomic expressions, each vl-nonatom-p includes finalwidth and finaltype fields, which are nil upon parsing and may later be filled in by our expression typing and sizing computations.

Additionally, each non-atomic expression includes:

  • op, the operation being applied. For structural validity, op must be one of the known operators found in *vl-ops-table*.
  • args, the arguments the operation is being applied to. No structural constraints are imposed upon args.
  • atts, which represent any attributes written in the (* foo = bar, baz *) style that Verilog-2005 permits. No structural constraints are placed upon atts.
Valid Expressions

The valid expressions are recognized by vl-expr-p, which extends our basic structural checks recursively over the expression, and also ensures that each operator has the proper arity.

Subtopics

Vl-atts
Representation of (* foo = 3, bar *) style attributes.
Vl-constint
Representation for constant integer literals with no X or Z bits.
*vl-ops-table*
Table binding valid operators to their vl-opinfo structures.
Vl-weirdint
Representation for constant integer literals with X or Z bits.
Vl-expr
Vl-id
Representation for simple identifiers.
Vl-hidpiece
Represents one piece of a hierarchical identifier.
Vl-time
Representation of time amounts.
Vl-maybe-exprtype
Recognizer for an vl-exprtype-p or nil.
Vl-op-p
Recognizer for valid operators.
Vl-maybe-expr
Vl-expr->finaltype
Get the finaltype from an expression.
Vl-real
Representation of real (floating point) literals.
Vl-expr->finalwidth
Get the finalwidth from an expression.
Vl-tagname
Represents a tagged union member name.
Vl-sysfunname
Represents a system function name.
Vl-string
Representation for string literals.
Vl-op-arity
Look up the arity of an operator.
Vl-keyguts
Representation of special, atomic SystemVerilog expressions, distinguished by keywords such as null, this, super, $, local, etc.
Vl-exprtype-p
Valid types for expressions.
Vl-typename
Represents a user-defined type name.
Vl-funname
Represents a (non-system) function name.
Vl-basictype
Atomic SystemVerilog types, like byte, int. These can be used, e.g., in casting and streaming concatenation expressions.
Vl-extint
Representation for unbased, unsized integer literals, viz. '0, '1, 'x, and 'z.
Vl-atomlist-p
(vl-atomlist-p x) recognizes lists where every element satisfies vl-atom-p.
Vl-atomguts
The main contents of a vl-atom-p.
Vl-nbits-fix
Vl-atom-p
Vl-arity-fix
Vl-arity-ok-p
Vl-op-text
Look up the text of an operator.
Vl-exprlist
A list of vl-expr-p objects.
Vl-oplist
A list of vl-op-p objects.
Vl-exprlistlist
A list of vl-exprlist-p objects.
Vl-ops-table
*vl-default-expr*