• 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-context-p
            • Ctxexprs
              • Vl-make-exprctxalist
              • Vl-paramdecllist-ctxexprs
              • Vl-taskdecllist-ctxexprs
              • Vl-portdecllist-ctxexprs
              • Vl-gateinstlist-ctxexprs
              • Vl-vardecllist-ctxexprs
              • Vl-modinstlist-ctxexprs
              • Vl-initiallist-ctxexprs
              • Vl-fundecllist-ctxexprs
              • Vl-assignlist-ctxexprs
              • Vl-alwayslist-ctxexprs
              • Vl-portlist-ctxexprs
              • Vl-taskdecl-ctxexprs
              • Vl-portdecl-ctxexprs
              • Vl-paramdecl-ctxexprs
              • Vl-gateinst-ctxexprs
              • Vl-vardecl-ctxexprs
              • Vl-modinst-ctxexprs
              • Vl-initial-ctxexprs
              • Vl-fundecl-ctxexprs
              • Vl-assign-ctxexprs
              • Vl-always-ctxexprs
              • Vl-port-ctxexprs
              • Vl-exprctxalist
            • Vl-pp-ctxelement-summary
            • Vl-pp-ctxelement-full
            • Vl-context-fix
            • Vl-ctxelement-summary
            • Vl-context-summary
            • Vl-pp-context-summary
            • Vl-pp-context-full
          • 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
  • Vl-context

Ctxexprs

Functions for gathering expressions and the context in which they occur.

Like the allexprs family of functions, these functions gather up what we regard as the "top level" expressions used throughout some module. But whereas the allexprs functions just return flat lists of expressions, we return a vl-exprctxalist-p that associates each expression with a vl-context-p describing its origin.

Subtopics

Vl-make-exprctxalist
Bind some expressions to their context.
Vl-paramdecllist-ctxexprs
Collect up a vl-exprctxalist-p from a list of vl-paramdecllist-ps.
Vl-taskdecllist-ctxexprs
Collect up a vl-exprctxalist-p from a list of vl-taskdecllist-ps.
Vl-portdecllist-ctxexprs
Collect up a vl-exprctxalist-p from a list of vl-portdecllist-ps.
Vl-gateinstlist-ctxexprs
Collect up a vl-exprctxalist-p from a list of vl-gateinstlist-ps.
Vl-vardecllist-ctxexprs
Collect up a vl-exprctxalist-p from a list of vl-vardecllist-ps.
Vl-modinstlist-ctxexprs
Collect up a vl-exprctxalist-p from a list of vl-modinstlist-ps.
Vl-initiallist-ctxexprs
Collect up a vl-exprctxalist-p from a list of vl-initiallist-ps.
Vl-fundecllist-ctxexprs
Collect up a vl-exprctxalist-p from a list of vl-fundecllist-ps.
Vl-assignlist-ctxexprs
Collect up a vl-exprctxalist-p from a list of vl-assignlist-ps.
Vl-alwayslist-ctxexprs
Collect up a vl-exprctxalist-p from a list of vl-alwayslist-ps.
Vl-portlist-ctxexprs
Collect up a vl-exprctxalist-p from a list of vl-portlist-ps.
Vl-taskdecl-ctxexprs
Vl-portdecl-ctxexprs
Vl-paramdecl-ctxexprs
Vl-gateinst-ctxexprs
Vl-vardecl-ctxexprs
Vl-modinst-ctxexprs
Vl-initial-ctxexprs
Vl-fundecl-ctxexprs
Vl-assign-ctxexprs
Vl-always-ctxexprs
Vl-port-ctxexprs
Vl-exprctxalist
An alist binding vl-expr-ps to vl-context-ps.