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

Syntax

Internal representation of the syntax of Verilog and SystemVerilog.

Introduction

A core component of vl is its internal representation of Verilog's syntactic structures. For each kind of Verilog construct (expressions, statements, declarations, instances, etc.) we introduce corresponding ``types'' with their own recognizer, constructor, and accessor functions.

These structures generally correspond fairly closely to parse trees in the SystemVerilog grammar, except that:

  • We sometimes make certain simplifications to present a more regular view of the source code. For instance, whereas in a normal Verilog module you might write something like wire [3:0] a, b, c; to simultaneously declare several wires, our internal representation treats each wire declaration separately, as if you had instead written wire [3:0] a; wire [3:0] b; wire [3:0] c;.
  • We generally separate the various kinds of parsed elements (e.g., assignments, declarations, etc.) out into distinct lists, whereas in the source code these elements may be all mixed together. This is sometimes slightly tricky; see also the loader and the annotate transform.
  • Many structures also contain various additional fields that are not purely part of the syntax. For instance, many structures include vl-location annotations to say where they came from, expressions include annotations about whether they have explicit parentheses, and high-level design elements like modules have warnings attached to them.

We introduce all of these structures using the fty library and following the fixtype discipline. This generally means that each type has an associated fixing function, equivalence relation, etc. If you aren't familiar with fty, you may want to learn a bit about it before trying to understand these structures.

Quick Guide

SystemVerilog is a huge language (the grammar is about 45 pages!) so it can be easy to get lost in all of the different kinds of constructs. Here is a quick guide to the most major syntactic definitions:

  • vl-design is our top-level representation of an entire design, including all of the modules, interfaces, packages, programs, etc., typically spread out across many Verilog or SystemVerilog source files. If you start here and then drive down into the fields, you'll eventually explore all of our syntactic constructs.
  • Many kinds of major design elements can occur in a design, e.g., modules, interfaces, packages, programs, configs, user defined primitives, etc. We represent these with, e.g., vl-module, vl-interface, vl-package, vl-program, vl-config, vl-udp, etc.
  • Modules are the mainstay of most designs. Most modules contain things like assignments, gate and module instances, always blocks, initial blocks, aliases, and so on. We represent these module elements using, e.g., vl-assign, vl-gateinst, vl-modinst, vl-always, vl-initial, vl-final, vl-alias, etc.
  • Other widely used constructs include declarations of many kinds, e.g., variables, ports, parameters, functions, tasks, types. See for instance vl-vardecl, vl-port and vl-portdecl, vl-paramdecl, vl-fundecl, vl-taskdecl, and vl-typedef.
  • Underpinning all of the above are Expressions and Datatypes. These are mutually recursive since expressions like casts can include types while many datatypes use expressions for indexes and so forth.
  • Various constructs like always/initial/final blocks and functions and tasks also make use of procedural statements like if/else, case statements, and for loops. Some notable statements include vl-assertstmt and vl-cassertstmt for immediate and concurrent SystemVerilog assertions. Note that concurrent assertions also involve an elaborate notion of property-expressions.

The above isn't entirely comprehensive; for instance a good deal of stuff is needed to represent generate statements; see vl-genelement. There are also various unfinished areas like support for SystemVerilog assertions.

Subtopics

Vl-module
Representation of a single module.
Vl-vardecl
Representation of a single variable or net (e.g., wire) declaration.
Vl-fundecl
Representation of a single Verilog function.
Vl-interface
Representation of a single interface.
Vl-design
Top level representation of all modules, interfaces, programs, etc., resulting from parsing some Verilog source code.
Vl-assign
Representation of a continuous assignment statement.
Vl-modinst
Representation of a single module instance, user-defined primitive instance, or a direct interface instance (not an interface port).
Vl-gateinst
Representation of a single gate instantiation.
Vl-taskdecl
Representation of a single Verilog task.
Vl-portdecl
Representation of Verilog port declarations.
Vl-commentmap
Representation of comments within a top-level design elements.
Vl-dpiimport
Represents a single import of a C function into SystemVerilog via the Direct Programming Interface.
Vl-ansi-portdecl
Temporary representation for port declarations.
Vl-package
Representation of a single package.
Vl-paramdecl
Representation of a single parameter or localparam declaration.
Vl-dpiexport
Represents a single export of a SystemVerilog function/task for use in C programs via the Direct Programming Interface.
Vl-class
Representation of a single class.
Vl-sort-blockitems-aux
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.
Expressions-and-datatypes
Representation of expressions, datatypes, and other related, mutually recursive concepts.
Vl-fundecllist->names
(vl-fundecllist->names x) maps vl-fundecl->name across a list.
Vl-udp
Representation of a user defined primitive.
Vl-port
Representation of a single port.
Vl-genelement
Representation of an arbitrary module element or generate construct.
Vl-clkdecl
Representation of a (non-global) clocking block declaration.
Vl-parse-temps
Temporary stuff recorded by parsing that's used to generate real module items by the first annotate transforms, and should be ignored after that.
Vl-bind
Representation of a bind directive.
Vl-namedarg
Representation of a single argument in a named argument list.
Vl-exprdist
Representation of expr dist { ... } constructs.
Vl-clkassign
Representation of a single clocking assignment (clocking blocks).
Vl-range
A simple [msb:lsb] style range.
Vl-propport
Representation of a single property or sequence port.
Vl-typedef
Representation of a basic type declaration like typedef struct ... foo_t;.
Vl-gatedelay
Representation of delay expressions.
Vl-dimension
Representation of a single packed or unpacked dimension. These could be a range like [3:0] or something more exotic, like [], [*], or [logic [3:0]].
Vl-sequence
Represents a single sequence...endsequence declaration.
Vl-clkskew
Representation of a clock skew (clocking blocks).
Vl-program
Representation of a single program.
Vl-gatestrength
Representation of strengths for a assignment statements, gate instances, and module instances.
Vl-property
Represents a single property...endproperty declaration.
Vl-config
Representation of a single config.
Vl-always
Representation of an always statement.
Vl-import
Representation of a single import item, i.e., import foo::bar;.
Vl-repeateventcontrol
Representation of repeat constructs in intra-assignment delays.
Vl-timeliteral
Representation of a single time_literal token.
Vl-initial
Representation of an initial statement.
Vl-eventcontrol
Representation of an event controller like @(posedge clk) or @(a or b).
Vl-final
Representation of a final statement.
Vl-udpsymbol-p
Symbols that can occur in a UDP table
Vl-maybe-clkskew
Option type; vl-clkskew or nil.
Vl-function-specialization
Vl-alias
Representation of an alias declaration.
Vl-maybe-nettypename
Option type; vl-nettypename-p or nil.
Vl-maybe-gatedelay
Option type; vl-gatedelay or nil.
Vl-letdecl
Vl-direction-p
Direction for a port declaration (input, output, or inout).
Vl-modelement
Recognizer for an arbitrary module element.
Vl-maybe-timeprecisiondecl
Option type; vl-timeprecisiondecl or nil.
Vl-maybe-scopeid
Option type; vl-scopeid or nil.
Vl-maybe-gatestrength
Option type; vl-gatestrength or nil.
Vl-maybe-direction
Option type; vl-direction-p or nil.
Vl-maybe-delayoreventcontrol
Option type; vl-delayoreventcontrol or nil.
Vl-gclkdecl
Representation of a global clocking declaration.
Vl-fwdtypedef
Representation of a forward typedef like typedef struct foo_t;.
Vl-maybe-udpsymbol-p
Option type; vl-udpsymbol-p or nil.
Vl-maybe-timeunitdecl
Option type; vl-timeunitdecl or nil.
Vl-maybe-timeliteral
Option type; vl-timeliteral or nil.
Vl-maybe-parse-temps
Option type; vl-parse-temps or nil.
Vl-maybe-cstrength
Option type; vl-cstrength-p or nil.
Vl-arguments
Representation of arguments to a module instance (for ports, not parameters).
Vl-maybe-module
Recognizer for an vl-module-p or nil.
Vl-maybe-design
Option type; vl-design or nil.
Vl-covergroup
Representation of a single covergroup.
Vl-udpline
Representation of one line of a UDP table.
Vl-timeunitdecl
Representation of a 'timeunit' declaration.
Vl-genvar
Representation of a genvar declaration.
Vl-defaultdisable
Representation of a default disable iff construct.
Vl-context1
Description of where an expression occurs.
Vl-timeprecisiondecl
Representation of a 'timeprecision' declaration.
Vl-sort-blockitems
Vl-elabtask
Representation of a SystemVerilog elaboration_system_task.
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-ctxelement
Vl-ctxelement->loc
Vl-modelement->loc
Statements
Representation of a statement.
Vl-blockitem
Recognizer for a valid block item.
Vl-vardecllist
A list of vl-vardecl-p objects.
Vl-interface->ifports
Collect just the interface ports for a interface.
Vl-syntaxversion
Version of VL syntax being used.
Vl-nettypename-p
Representation of wire (net) types, i.e., resolution function.
Vl-module->ifports
Collect just the interface ports for a module.
Vl-lifetime-p
Representation of the lifetime of a variable, function, task, etc.
Vl-paramdecllist
A list of vl-paramdecl-p objects.
Vl-modelementlist->genelements
Vl-importlist
A list of vl-import-p objects.
Vl-typedeflist
A list of vl-typedef-p objects.
Vl-gatetype-p
Representation of gate types.
Vl-cstrength-p
Representation of charge strengths.
Vl-port->name
Vl-genelement->loc
Vl-delayoreventcontrol
BOZO document this.
Vl-udpentry-p
Representation of any entry in a UDP table.
Vl-portdecllist
A list of vl-portdecl-p objects.
Vl-elabtask->loc
Property-expressions
Representation of SystemVerilog property and sequence expressions.
Vl-taskdecllist
A list of vl-taskdecl-p objects.
Vl-port->loc
Vl-fundecllist
A list of vl-fundecl-p objects.
Vl-sequencelist
A list of vl-sequence-p objects.
Vl-propertylist
A list of vl-property-p objects.
Vl-portlist
A list of vl-port-p objects.
Vl-dpiimportlist
A list of vl-dpiimport-p objects.
Vl-dpiexportlist
A list of vl-dpiexport-p objects.
Vl-classlist
A list of vl-class-p objects.
Vl-arguments->args
Vl-alwaystype-p
Indicates the kind of an always statement.
Vl-modinstlist
A list of vl-modinst-p objects.
Vl-importpart-p
Vl-importpart-fix
Vl-bindlist
A list of vl-bind-p objects.
Vl-initiallist
A list of vl-initial-p objects.
Vl-genvarlist
A list of vl-genvar-p objects.
Vl-gclkdecllist
A list of vl-gclkdecl-p objects.
Vl-function-specialization-map
An alist mapping sv::maybe-4veclist-p to vl-function-specialization-p.
Vl-finallist
A list of vl-final-p objects.
Vl-elabtasklist
A list of vl-elabtask-p objects.
Vl-defaultdisablelist
A list of vl-defaultdisable-p objects.
Vl-clkdecllist
A list of vl-clkdecl-p objects.
Vl-cassertionlist
A list of vl-cassertion-p objects.
Vl-blockstmt-p
Vl-assignlist
A list of vl-assign-p objects.
Vl-assertionlist
A list of vl-assertion-p objects.
Vl-alwayslist
A list of vl-always-p objects.
Vl-aliaslist
A list of vl-alias-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-propportlist
A list of vl-propport-p objects.
Vl-programlist
A list of vl-program-p objects.
Vl-packagelist
A list of vl-package-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-letdecllist
A list of vl-letdecl-p objects.
Vl-interfacelist
A list of vl-interface-p objects.
Vl-gateinstlist
A list of vl-gateinst-p objects.
Vl-fwdtypedeflist
A list of vl-fwdtypedef-p objects.
Vl-covergrouplist
A list of vl-covergroup-p objects.
Vl-configlist
A list of vl-config-p objects.
Vl-clkassignlist
A list of vl-clkassign-p objects.
Vl-blockitemlist
A list of vl-blockitem-p objects.
Vl-ansi-portdecllist
A list of vl-ansi-portdecl-p objects.
Vl-regularportlist
A list of vl-regularport-p objects.
Vl-paramdecllist-list
A list of vl-paramdecllist-p objects.
Vl-modelementlist
A list of vl-modelement-p objects.
Vl-interfaceportlist
A list of vl-interfaceport-p objects.
Vl-casekey-p
Sv::maybe-4veclist
A list of sv::maybe-4vec-p objects.