• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
      • Vwsim
      • Fgl
      • 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-plainarglist->exprs
          • Vl-class
          • Vl-taskdecllist->names
          • Vl-sort-blockitems-aux
          • Vl-fundecllist->names
          • Expressions-and-datatypes
            • Vl-atts
            • Vl-expr
            • Vl-datatype
            • New-expression-representation
              • Vl-paramargs
              • Vl-evatom
              • Vl-maybe-paramargs
              • Vl-evatomlist
              • Vl-call-namedargs
              • Vl-paramvaluelist
              • Vl-namedparamvaluelist
            • 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-udpsymbol-p
            • Vl-final
            • Vl-maybe-clkskew
            • 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-modelement->loc
            • Vl-ctxelement
            • Vl-ctxelement->loc
            • Statements
            • Vl-interface->ifports
            • Vl-blockitem
            • Vl-vardecllist
            • Vl-module->ifports
            • Vl-lifetime-p
            • Vl-syntaxversion
            • Vl-nettypename-p
            • Vl-paramdecllist
            • Vl-modelementlist->genelements
            • Vl-importlist
            • Vl-gatetype-p
            • Vl-typedeflist
            • Vl-genelement->loc
            • Vl-cstrength-p
            • Vl-port->name
            • Vl-elabtask->loc
            • Vl-delayoreventcontrol
            • Vl-udpentry-p
            • Vl-portdecllist
            • Vl-port->loc
            • Property-expressions
            • Vl-taskdecllist
            • 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-blockstmt-p
            • Vl-bindlist
            • Vl-initiallist
            • Vl-genvarlist
            • Vl-gclkdecllist
            • Vl-finallist
            • Vl-elabtasklist
            • Vl-defaultdisablelist
            • Vl-clkdecllist
            • Vl-cassertionlist
            • 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-casekey-p
            • Vl-blockitemlist
            • Vl-ansi-portdecllist
            • Vl-regularportlist
            • Vl-paramdecllist-list
            • Vl-modelementlist
            • Vl-interfaceportlist
          • Loader
          • Warnings
          • Getting-started
          • Utilities
          • Printer
          • Kit
          • Mlib
          • Transforms
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Testing-utilities
      • Math
    • Expressions-and-datatypes

    New-expression-representation

    Notes about the new expression representation in vl, and how and why it diverges from the vl2014::expressions.

    In earlier versions of VL such as vl2014, we used a fairly simple, AST-like representation. This representation had some nice features: it kept mutual recursion to a minimum and made it easy to recur through expressions. However, it also had some severe weaknesses.

    The most significant of these was the lack of type safety. We often expected expressions to have certain shapes. For instance, we typically expected that any hierarchical identifier, like foo.bar[2].baz, would consist of special "hid pieces" joined together by certain "hid dot" and "hid array index" operators with a certain recursive structure. But the expression representation did not enforce this, so nothing prevented you from creating nonsensical expressions like foo.(3 + 4).baz.

    The ability to create degenerate/nonsense expressions is not necessarily so bad—just don't create nonsense expressions and what's the a problem? But the possibility of these degenerate expressions might exist turned out to have a pervasive impact when writing code to process expressions: VL's many transforms and utilities always had to defend against such malformed expressions.

    This defense was generally carried out by adding guards or explicit run-time tests that expressions were sensible. The result was copious error handling code, difficult and tedious proofs about well-formedness (e.g., see vl2014::welltyped), and additional interfacing layers such as the vl2014::hid-tools to hide the problem. These layers became ever more complex as we implemented more of SystemVerilog, e.g., scope expressions and datatype indexing greatly complicated the handling of hierarchical identifiers.

    Reflecting on these problems, and considering our improving ability to handle mutual-recursion via macro libraries such as fty and defines, we decided to overhaul the expression representation and replace it with a much more strongly typed, mutually recursive approach.

    Our new expression format is much more complex than before. However, it also intrinsically rules out many expressions that were previously allowed, which helps to avoid needing error checking code when processing expressions, and generally makes it easier to write safe expression-processing code.