• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Vwsim
    • Fgl
    • Vl
      • Syntax
      • Loader
      • Warnings
      • Getting-started
      • Utilities
      • Printer
      • Kit
      • Mlib
      • Transforms
        • Unparameterization
        • Elaborate
        • Addnames
        • Annotate
          • Increment-elim
          • Make-implicit-wires
            • Shadowcheck
            • Implicit-wires-minutia
            • Implicit-wires-generate-scoping
            • Vl-genbase-make-implicit-wires
            • Vl-expr-names-for-implicit
            • Vl-make-implicit-wires-main
            • Vl-implicitst
              • Vl-implicitst-fix
              • Vl-implicitst-equiv
              • Vl-implicitst-p
              • Make-vl-implicitst
              • Vl-implicitst->wildpkgs
              • Vl-implicitst->portdecls
              • Change-vl-implicitst
              • Vl-implicitst->ss
              • Vl-implicitst->decls
            • Vl-make-port-implicit-wires
            • Vl-import-update-implicit
            • Vl-blockitemlist-update-implicit
            • Vl-blockitem-update-implicit
            • Vl-make-ordinary-implicit-wires
            • Vl-remove-declared-wires
            • Vl-implicitsts-restore-fast-alists
            • Vl-genblock-under-cond-make-implicit-wires
            • Vl-collect-exprs-for-implicit-wires-from-namedargs
            • Vl-genblock-make-implicit-wires
            • Vl-collect-exprs-for-implicit-wires-from-portargs
            • Vl-collect-exprs-for-implicit-wires-from-namedarg
            • Vl-gateinst-exprs-for-implicit-wires
            • Vl-modinst-exprs-for-implicit-wires
            • Vl-genelementlist-make-implicit-wires
            • Vl-packagemap-find-name
          • Basic-bind-elim
          • Argresolve
          • Basicsanity
          • Portdecl-sign
          • Enum-names
          • Port-resolve
          • Udp-elim
          • Vl-annotate-design
          • Vl-annotate-module
        • Clean-warnings
        • Eliminitial
        • Custom-transform-hooks
        • Problem-modules
    • 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 their declarations.

decls — 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. Also includes any items explicitly imported from packages.

wildpkgs — vl-packagemap

Fast alist binding the name of each wildcard-imported package to its corresponding scopeitem-alist

ss — vl-scopestack

Scopestack for lookup of global and package 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->wildpkgs

Get the wildpkgs field from a vl-implicitst.

Vl-implicitst->portdecls

Get the portdecls 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.

Vl-implicitst->decls

Get the decls field from a vl-implicitst.