• 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
        • Getting-started
        • Utilities
        • Loader
        • Transforms
        • Lint
        • Mlib
          • Scopestack
          • Filtering-by-name
          • Vl-namefactory
          • Substitution
            • Vl-packeddimensionlist-subst
            • Vl-namedparamvaluelist-subst
            • Vl-paramvaluelist-subst
            • Vl-paramdecllist-subst
            • Vl-portdecllist-subst
            • Vl-plainarglist-subst
            • Vl-namedarglist-subst
            • Vl-gateinstlist-subst
            • Vl-enumitemlist-subst
            • Vl-vardecllist-subst
            • Vl-modinstlist-subst
            • Vl-initiallist-subst
            • Vl-fundecllist-subst
            • Vl-expr-subst
            • Vl-modulelist-subst
            • Vl-evatomlist-subst
            • Vl-assignlist-subst
            • Vl-alwayslist-subst
            • Vl-rangelist-subst
            • Vl-portlist-subst
            • Vl-stmt-subst
            • Vl-maybe-delayoreventcontrol-subst
            • Vl-repeateventcontrol-subst
            • Vl-maybe-packeddimension-subst
            • Vl-delayoreventcontrol-subst
            • Vl-packeddimension-subst
            • Vl-namedparamvalue-subst
            • Vl-module-subst
            • Vl-maybe-paramvalue-subst
            • Vl-paramvalue-subst
            • Vl-paramtype-subst
            • Vl-modinst-subst
            • Vl-maybe-gatedelay-subst
            • Vl-maybe-datatype-subst
            • Vl-interfaceport-subst
            • Vl-gateinst-subst
            • Vl-fundecl-subst
            • Vl-eventcontrol-subst
            • Vl-enumbasetype-subst
            • Vl-delaycontrol-subst
            • Vl-vardecl-subst
            • Vl-regularport-subst
            • Vl-portdecl-subst
            • Vl-plainarg-subst
            • Vl-paramdecl-subst
            • Vl-paramargs-subst
            • Vl-namedarg-subst
            • Vl-maybe-range-subst
            • Vl-gatedelay-subst
            • Vl-enumitem-subst
            • Vl-assign-subst
            • Vl-arguments-subst
            • Vl-range-subst
            • Vl-maybe-expr-subst
            • Vl-initial-subst
            • Vl-evatom-subst
            • Vl-always-subst
            • Vl-port-subst
            • Vl-sigma-count
            • Vl-sigma
          • Allexprs
          • Hid-tools
          • Vl-consteval
          • Range-tools
          • Lvalexprs
          • Hierarchy
          • Finding-by-name
          • Expr-tools
          • Expr-slicing
          • Stripping-functions
          • Stmt-tools
          • Modnamespace
          • Vl-parse-expr-from-str
          • Welltyped
          • Reordering-by-name
          • Flat-warnings
          • Genblob
          • Expr-building
          • Datatype-tools
          • Syscalls
          • Relocate
          • Expr-cleaning
          • Namemangle
          • Caremask
          • Port-tools
          • Lvalues
        • Server
        • Kit
        • Printer
        • Esim-vl
        • Well-formedness
      • Sv
      • Fgl
      • Vwsim
      • Vl
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Math
    • Testing-utilities
  • Mlib

Substitution

Substitution into Verilog constructs

We implement routines to substitute values for identifiers throughout Verilog constructs such as expressions, assignments, and modules.

Our original use of substitution was in unparameterization, where we used substitution to replace parameters with their values throughout a module. Because of this, and since there are usually only a couple of parameters per module, we historically created ordinary alists and look up with hons-assoc-equal rather than hons-get. Since then we have found substitution to be more generally useful, and prefer to use fast alists.

Subtopics

Vl-packeddimensionlist-subst
(vl-packeddimensionlist-subst x sigma) maps vl-packeddimension-subst across a list.
Vl-namedparamvaluelist-subst
(vl-namedparamvaluelist-subst x sigma) maps vl-namedparamvalue-subst across a list.
Vl-paramvaluelist-subst
(vl-paramvaluelist-subst x sigma) maps vl-paramvalue-subst across a list.
Vl-paramdecllist-subst
(vl-paramdecllist-subst x sigma) maps vl-paramdecl-subst across a list.
Vl-portdecllist-subst
(vl-portdecllist-subst x sigma) maps vl-portdecl-subst across a list.
Vl-plainarglist-subst
(vl-plainarglist-subst x sigma) maps vl-plainarg-subst across a list.
Vl-namedarglist-subst
(vl-namedarglist-subst x sigma) maps vl-namedarg-subst across a list.
Vl-gateinstlist-subst
(vl-gateinstlist-subst x sigma) maps vl-gateinst-subst across a list.
Vl-enumitemlist-subst
(vl-enumitemlist-subst x sigma) maps vl-enumitem-subst across a list.
Vl-vardecllist-subst
(vl-vardecllist-subst x sigma) maps vl-vardecl-subst across a list.
Vl-modinstlist-subst
(vl-modinstlist-subst x sigma) maps vl-modinst-subst across a list.
Vl-initiallist-subst
(vl-initiallist-subst x sigma) maps vl-initial-subst across a list.
Vl-fundecllist-subst
(vl-fundecllist-subst x sigma) maps vl-fundecl-subst across a list.
Vl-expr-subst
Substitute into a vl-expr-p.
Vl-modulelist-subst
(vl-modulelist-subst x sigma) maps vl-module-subst across a list.
Vl-evatomlist-subst
(vl-evatomlist-subst x sigma) maps vl-evatom-subst across a list.
Vl-assignlist-subst
(vl-assignlist-subst x sigma) maps vl-assign-subst across a list.
Vl-alwayslist-subst
(vl-alwayslist-subst x sigma) maps vl-always-subst across a list.
Vl-rangelist-subst
(vl-rangelist-subst x sigma) maps vl-range-subst across a list.
Vl-portlist-subst
(vl-portlist-subst x sigma) maps vl-port-subst across a list.
Vl-stmt-subst
Substitute into a vl-stmt-p
Vl-maybe-delayoreventcontrol-subst
Substitute into a vl-maybe-delayoreventcontrol-p.
Vl-repeateventcontrol-subst
Substitute into a vl-repeateventcontrol-p.
Vl-maybe-packeddimension-subst
Substitute into a vl-maybe-packeddimension-p.
Vl-delayoreventcontrol-subst
Substitute into a vl-delayoreventcontrol-p.
Vl-packeddimension-subst
Substitute into a vl-packeddimension-p.
Vl-namedparamvalue-subst
Substitute into a vl-namedparamvalue-p.
Vl-module-subst
Substitute into a vl-module-p.
Vl-maybe-paramvalue-subst
Substitute into a vl-maybe-paramvalue-p.
Vl-paramvalue-subst
Substitute into a vl-paramvalue-p.
Vl-paramtype-subst
Substitute into a vl-paramtype-p.
Vl-modinst-subst
Substitute into a vl-modinst-p.
Vl-maybe-gatedelay-subst
Substitute into a vl-maybe-gatedelay-p.
Vl-maybe-datatype-subst
Substitute into a vl-maybe-datatype-p.
Vl-interfaceport-subst
Substitute into a vl-interfaceport-p.
Vl-gateinst-subst
Substitute into a vl-gateinst-p.
Vl-fundecl-subst
Substitute into a vl-fundecl-p.
Vl-eventcontrol-subst
Substitute into a vl-eventcontrol-p.
Vl-enumbasetype-subst
Substitute into a vl-enumbasetype-p.
Vl-delaycontrol-subst
Substitute into a vl-delaycontrol-p.
Vl-vardecl-subst
Substitute into a vl-vardecl-p.
Vl-regularport-subst
Substitute into a vl-regularport-p.
Vl-portdecl-subst
Substitute into a vl-portdecl-p.
Vl-plainarg-subst
Substitute into a vl-plainarg-p.
Vl-paramdecl-subst
Substitute into a vl-paramdecl-p.
Vl-paramargs-subst
Substitute into a vl-paramargs-p.
Vl-namedarg-subst
Substitute into a vl-namedarg-p.
Vl-maybe-range-subst
Substitute into a vl-maybe-range-p.
Vl-gatedelay-subst
Substitute into a vl-gatedelay-p.
Vl-enumitem-subst
Substitute into a vl-enumitem-p.
Vl-assign-subst
Substitute into a vl-assign-p.
Vl-arguments-subst
Substitute into a vl-arguments-p.
Vl-range-subst
Substitute into a vl-range-p.
Vl-maybe-expr-subst
Substitute into a vl-maybe-expr-p.
Vl-initial-subst
Substitute into a vl-initial-p.
Vl-evatom-subst
Substitute into a vl-evatom-p.
Vl-always-subst
Substitute into a vl-always-p.
Vl-port-subst
Substitute into a vl-port-p.
Vl-sigma-count
Vl-sigma
An alist mapping strings to expressions, used in substitution.