• 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
          • Expression-sizing
          • Occform
          • Oprewrite
          • Expand-functions
          • Delayredux
          • Unparameterization
          • Caseelim
          • Split
          • Selresolve
          • Weirdint-elim
          • Vl-delta
          • Replicate-insts
          • Rangeresolve
          • Propagate
          • Clean-selects
          • Clean-params
          • Blankargs
          • Inline-mods
          • Expr-simp
          • Trunc
          • Always-top
          • Gatesplit
          • Gate-elim
          • Expression-optimization
          • Elim-supplies
          • Wildelim
          • Drop-blankports
          • Clean-warnings
          • Addinstnames
          • Custom-transform-hooks
          • Annotate
            • Make-implicit-wires
              • Vl-modulelist-make-implicit-wires
              • Vl-make-implicit-wires-aux
              • Shadowcheck
              • Vl-stmt-check-undeclared
              • Vl-make-implicit-wires-main
              • Vl-fundecl-check-undeclared
              • Vl-warn-about-undeclared-wires
              • Vl-implicitst
                • Vl-implicitst-fix
                • Vl-implicitst-equiv
                • Vl-implicitst-p
                • Make-vl-implicitst
                • Vl-implicitst->portdecls
                • Vl-implicitst->imports
                • Vl-implicitst->decls
                • Change-vl-implicitst
                • Vl-implicitst->ss
              • Vl-blockitem-check-undeclared
              • Vl-taskdecl-check-undeclared
              • Vl-modinst-exprs-for-implicit-wires
              • Vl-blockitemlist-check-undeclared
              • Vl-import-check-undeclared
              • Vl-make-ordinary-implicit-wires
              • Vl-gateinst-exprs-for-implicit-wires
              • Vl-remove-declared-wires
              • Vl-make-port-implicit-wires
              • Vl-module-make-implicit-wires
              • Vl-vardecl-exprs-for-implicit-wires
              • Vl-design-make-implicit-wires
            • Resolve-indexing
            • Origexprs
            • Argresolve
            • Portdecl-sign
            • Designwires
            • Udp-elim
            • Vl-annotate-design
          • Latchcode
          • Elim-unused-vars
          • Problem-modules
        • Lint
        • Mlib
        • Server
        • Kit
        • Printer
        • Esim-vl
        • Well-formedness
      • Sv
      • Fgl
      • Vwsim
      • Vl
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Math
    • Testing-utilities
  • Make-implicit-wires

Vl-implicitst

State for the make-implicit-wires transform.

This is a product type introduced by defprod.

Fields
portdecls — vl-portdecl-alist
Fast alist binding names of declared port names to anything.
decls — ACL2::any-p
Fast alist binding names of declared non-port names to anything. These names can be the names of wires, instances, functions, etc., that are in the local scope, for instance.
imports — ACL2::any-p
Fast alist binding imported names to anything.
ss — vl-scopestack
Scopestack for lookup of global names. Note that this scopestack doesn't typically contain the current module we're looking at, because it isn't really a complete module until we add the implicit wires to it.

Subtopics

Vl-implicitst-fix
Fixing function for vl-implicitst structures.
Vl-implicitst-equiv
Basic equivalence relation for vl-implicitst structures.
Vl-implicitst-p
Recognizer for vl-implicitst structures.
Make-vl-implicitst
Basic constructor macro for vl-implicitst structures.
Vl-implicitst->portdecls
Get the portdecls field from a vl-implicitst.
Vl-implicitst->imports
Get the imports field from a vl-implicitst.
Vl-implicitst->decls
Get the decls field from a vl-implicitst.
Change-vl-implicitst
Modifying constructor for vl-implicitst structures.
Vl-implicitst->ss
Get the ss field from a vl-implicitst.