• 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-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
  • Vl2014

Syntax

Representation of Verilog structures.

We now describe our representation of Verilog's syntactic structures. For each kind of Verilog construct (expressions, statements, declarations, instances, etc.) we introduce recognizer, constructor, and accessor functions that enforce certain basic well-formedness criteria.

These structures correspond fairly closely to parse trees in the Verilog grammar, although we make many simplifcations and generally present a much more regular view of the source code.

Subtopics

Vl-module
Representation of a single module.
Vl-vardecl
Representation of a single variable or net (e.g., wire) declaration.
Expressions
Representation of Verilog expressions.
Vl-fundecl
Representation of a single Verilog function.
Vl-assign
Representation of a continuous assignment statement.
Vl-gateinst
Representation of a single gate instantiation.
Vl-modinst
Representation of a single module instance, user-defined primitive instance, or a direct interface instance (not an interface port).
Vl-commentmap
Representation of comments within a top-level design elements.
Vl-portdecl
Representation of Verilog port declarations.
Vl-taskdecl
Representation of a single Verilog task.
Vl-design
Top level representation of all modules, interfaces, programs, etc., resulting from parsing some Verilog source code.
Vl-interface
Representation of a single interface.
Vl-plainarglist->exprs
(vl-plainarglist->exprs x) maps vl-plainarg->expr across a list.
Vl-taskdecllist->names
(vl-taskdecllist->names x) maps vl-taskdecl->name across a list.
Vl-fundecllist->names
(vl-fundecllist->names x) maps vl-fundecl->name across a list.
Vl-package
Representation of a single package.
Vl-port
Representation of a single port.
Vl-udp
Representation of a user defined primitive.
Vl-paramdecl
Representation of a single parameter or localparam declaration.
Vl-genelement
Vl-cycledelayrange
Representation of cycle delay ranges in SystemVerilog sequences.
Vl-namedarg
Representation of a single argument in a named argument list.
Vl-sort-blockitems-aux
Vl-distitem
Representation of weighted distribution information.
Vl-gatedelay
Representation of delay expressions.
Vl-repetition
Representation of a SystemVerilog assertion sequence repetition.
Vl-typedef
Representation of a basic type declaration like typedef struct ... foo_t;.
Vl-range
Representation of ranges on wire declarations, instance array declarations, and so forth.
Vl-gatestrength
Representation of strengths for a assignment statements, gate instances, and module instances.
Vl-program
Representation of a single program.
Vl-config
Representation of a single config.
Vl-always
Representation of an always statement.
Vl-datatype-update-dims
Vl-import
Representation of a single import item, i.e., import foo::bar;.
Vl-enumbasetype
The base types for SystemVerilog enumerations.
Vl-repeateventcontrol
Representation of repeat constructs in intra-assignment delays.
Vl-paramargs
Representation of the values to use for a module instance's parameters (not ports).
Vl-initial
Representation of an initial statement.
Vl-eventcontrol
Representation of an event controller like @(posedge clk) or @(a or b).
Vl-udpsymbol-p
Symbols that can occur in a UDP table
Vl-maybe-range
Option type; vl-range or nil.
Vl-maybe-nettypename
Option type; vl-nettypename-p or nil.
Vl-maybe-gatestrength
Option type; vl-gatestrength or nil.
Vl-maybe-gatedelay
Option type; vl-gatedelay or nil.
Vl-maybe-delayoreventcontrol
Option type; vl-delayoreventcontrol or nil.
Vl-alias
Representation of an alias declaration.
Maybe-string-fix
Vl-maybe-packeddimension
Option type; vl-packeddimension or nil.
Vl-fwdtypedef
Representation of a forward typedef like typedef struct foo_t;.
Vl-evatom
A single item in an event control list.
Vl-packeddimension-p
Recognizes ranges and unsized dimensions.
Vl-maybe-udpsymbol
Option type; vl-udpsymbol-p or nil.
Vl-maybe-module
Recognizer for an vl-module-p or nil.
Vl-maybe-direction
Option type; vl-direction-p or nil.
Vl-maybe-datatype
Option type; vl-datatype or nil.
Vl-maybe-cstrength
Option type; vl-cstrength-p or nil.
Vl-direction-p
Direction for a port declaration (input, output, or inout).
Vl-arguments
Representation of arguments to a module instance (for ports, not parameters).
Vl-maybe-design
Option type; vl-design or nil.
Vl-udpline
Representation of one line of a UDP table.
Vl-exprdist
Representation of expr dist { ... } constructs.
Vl-context1
Description of where an expression occurs.
Vl-genvar
Representation of a genvar declaration.
Vl-enumitem
A single member of an enum.
Vl-datatype-update-udims
Vl-datatype-update-pdims
Vl-modelement
Recognizer for an arbitrary module element.
Vl-udpedge
Representation of an explicit edge that can occur in a UDP table, e.g., (01) or (1?).
Vl-delaycontrol
Representation of a delay controller like #6.
Vl-context
A context for warnings.
Vl-sort-blockitems
Vl-distweighttype-p
Representation of the := or :/ weight operators.
Vl-ctxelement->loc
Vl-blockitem
Recognizer for a valid block item.
Vl-vardecllist
A list of vl-vardecl-p objects.
Vl-module->ifports
Collect just the interface ports for a module.
Vl-modelement->loc
Vl-ctxelement
Vl-coretypename-p
Basic kinds of data types.
Vl-packeddimensionlist
A list of vl-packeddimension-p objects.
Vl-modelementlist->genelements
Vl-gatetype-p
Representation of gate types.
Vl-paramdecllist
A list of vl-paramdecl-p objects.
Vl-lifetime-p
Representation of the lifetime of a variable.
Vl-datatype->udims
Vl-datatype->pdims
Vl-timeunit-p
Representation for SystemVerilog time units (s, ms, ps, ...)
Vl-repetitiontype-p
Representation of SystemVerilog assertion sequence repetition types, i.e., [*...], [->...], or [=...] style repetition.
Vl-port->name
Vl-importlist
A list of vl-import-p objects.
Vl-genelement->loc
Vl-delayoreventcontrol
BOZO document this.
Vl-cstrength-p
Representation of charge strengths.
Statements
Representation of a statement.
Vl-udpentry-p
Representation of any entry in a UDP table.
Vl-packeddimension-fix
Vl-nettypename-p
Representation of wire types.
Vl-portdecllist
A list of vl-portdecl-p objects.
Vl-port->loc
Vl-enumbasekind-fix
Vl-arguments->args
Vl-taskdecllist
A list of vl-taskdecl-p objects.
Vl-portlist
A list of vl-port-p objects.
Vl-importpart-p
Vl-importpart-fix
Vl-fundecllist
A list of vl-fundecl-p objects.
Vl-blockstmt-p
Vl-assignlist
A list of vl-assign-p objects.
Vl-alwaystype-p
Indicates the kind of an always statement.
Vl-typedeflist
A list of vl-typedef-p objects.
Vl-syntaxversion-p
Vl-randomqualifier-p
Random qualifiers that can be put on struct or union members.
Vl-modinstlist
A list of vl-modinst-p objects.
Vl-gateinstlist
A list of vl-gateinst-p objects.
Vl-blockitemlist
A list of vl-blockitem-p objects.
Vl-udptable
A list of vl-udpline-p objects.
Vl-udplist
A list of vl-udp-p objects.
Vl-udpentrylist
A list of vl-udpentry-p objects.
Vl-programlist
A list of vl-program-p objects.
Vl-paramvaluelist
A list of vl-paramvalue-p objects.
Vl-packagelist
A list of vl-package-p objects.
Vl-namedparamvaluelist
A list of vl-namedparamvalue-p objects.
Vl-namedarglist
A list of vl-namedarg-p objects.
Vl-modulelist
A list of vl-module-p objects.
Vl-modportlist
A list of vl-modport-p objects.
Vl-modport-portlist
A list of vl-modport-port-p objects.
Vl-interfacelist
A list of vl-interface-p objects.
Vl-initiallist
A list of vl-initial-p objects.
Vl-genvarlist
A list of vl-genvar-p objects.
Vl-fwdtypedeflist
A list of vl-fwdtypedef-p objects.
Vl-evatomlist
A list of vl-evatom-p objects.
Vl-enumitemlist
A list of vl-enumitem-p objects.
Vl-distlist
A list of vl-distitem-p objects.
Vl-configlist
A list of vl-config-p objects.
Vl-alwayslist
A list of vl-always-p objects.
Vl-aliaslist
A list of vl-alias-p objects.
Vl-regularportlist
A list of vl-regularport-p objects.
Vl-rangelist-list
A list of vl-rangelist-p objects.
Vl-rangelist
A list of vl-range-p objects.
Vl-paramdecllist-list
A list of vl-paramdecllist-p objects.
Vl-modelementlist
A list of vl-modelement-p objects.
Vl-maybe-range-list
A list of vl-maybe-range-p objects.
Vl-interfaceportlist
A list of vl-interfaceport-p objects.
Vl-argumentlist
A list of vl-arguments-p objects.
Data-types