• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
      • Fgl
      • Vwsim
      • Vl
        • Syntax
        • Loader
        • Warnings
        • Getting-started
        • Utilities
        • Printer
        • Kit
        • Mlib
        • Transforms
          • Unparameterization
          • Elaborate
          • Addnames
          • Annotate
            • Increment-elim
            • Make-implicit-wires
              • Shadowcheck
                • Vl-shadowcheck-genelement
                • Vl-shadowcheck-reference-name
                • Vl-shadowcheck-declare-name
                • Deltemps
                • Vl-shadowcheck-modelement
                • Vl-lexscope
                  • Vl-lexscope-entry
                  • Vl-lexscope-fix
                  • Vl-lexscope-equiv
                  • Vl-lexscope-find
                  • Make-vl-lexscope
                  • Vl-lexscope->wildpkgs
                  • Vl-lexscope->decls
                  • Change-vl-lexscope
                  • Vl-lexscope-p
                  • Vl-empty-lexscope
                • Vl-shadowcheck-reference-scopeexpr
                • Vl-shadowcheck-reference-names
                • Vl-shadowcheck-declare-names
                • Vl-shadowcheck-paramtype
                • Vl-shadowcheck-fun/task-loaditems
                • Vl-shadowcheck-fun/task-loaditem
                • Vl-shadowcheck-fundecl
                • Vl-shadowcheck-declare-typedefs
                • Vl-shadowcheck-blockitemlist
                • Vl-shadowcheck-portdecllist
                • Vl-shadowcheck-paramdecls
                • Vl-shadowcheck-dpiimports
                • Vl-shadowcheck-taskdecls
                • Vl-shadowcheck-taskdecl
                • Vl-shadowcheck-push-scope
                • Vl-shadowcheck-blockitem
                • Vl-shadowcheck-vardecls
                • Vl-shadowcheck-vardecl
                • Vl-shadowcheck-typedef
                • Vl-shadowcheck-portdecl
                • Vl-shadowcheck-paramdecl
                • Vl-shadowcheck-modport
                • Vl-shadowcheck-modinst
                • Vl-shadowcheck-imports
                • Vl-shadowcheck-import
                • Vl-shadowcheck-gateinst
                • Vl-shadowcheck-fundecls
                • Vl-shadowcheck-dpiimport
                • Vl-shadowcheck-ports
                • Vl-shadowcheck-port
                • Vl-shadowcheck-initial
                • Vl-shadowcheck-assign
                • Vl-shadowcheck-always
                • Vl-shadowcheck-final
                • Vl-shadowcheck-alias
                • Vl-shadowcheck-state
                • Vl-shadowcheck-module
                • Vl-shadowcheck-interface
                • Vl-shadowcheck-interfaces
                • Vl-shadowcheck-modules
                • Vl-packagemap-find-packages-for-name
                • Vl-shadowcheck-design
                • Vl-lexscopes
                • Vl-expr->maybe-subtype
                • Vl-shadowcheck-pop-scope
                • Nameclash
                • Vl-portdecl-or-blockitem
                • Vl-lexscope-decls
                • Vl-packagemap
                • Vl-portdecl-or-blockitem-list
              • 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-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
  • Shadowcheck

Vl-lexscope

Representation of a single partial lexical scope.

This is a product type introduced by defprod.

Fields
decls — vl-lexscope-decls
wildpkgs — vl-packagemap

Abstractly a lexscope is just a mapping from names to vl-lexscope-entry objects, i.e. a vl-lexscope-decls object. The decls field has this mapping, for names that are explicitly declared or imported explicitly from packages at the current scope. But for wildcard imports, we don't store imported symbols in the decls map. Instead, we keep an additional field wildpkgs mapping each wildcard-imported package name to the scopeitem-alist of the declarations of that package. Whenever we look up a name in a lexscope, we also look up the name in all of these package scopeitem-alists to collect the list of packages that the name is imported from (populating the wildpkgs field of the vl-lexscope-entry' object.

Subtopics

Vl-lexscope-entry
Information about a single name in a lexical scope.
Vl-lexscope-fix
Fixing function for vl-lexscope structures.
Vl-lexscope-equiv
Basic equivalence relation for vl-lexscope structures.
Vl-lexscope-find
Look up a name in a (single) lexical scope.
Make-vl-lexscope
Basic constructor macro for vl-lexscope structures.
Vl-lexscope->wildpkgs
Get the wildpkgs field from a vl-lexscope.
Vl-lexscope->decls
Get the decls field from a vl-lexscope.
Change-vl-lexscope
Modifying constructor for vl-lexscope structures.
Vl-lexscope-p
Recognizer for vl-lexscope structures.
Vl-empty-lexscope
Create a new, empty lexical scope.