• 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
                • Vl-shadowcheck-genelement
                • Vl-shadowcheck-reference-name
                • Vl-shadowcheck-declare-name
                • Deltemps
                • Vl-shadowcheck-modelement
                • Vl-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-state-p
                  • Vl-shadowcheck-state-fix
                  • Vl-shadowcheck-state-equiv
                  • Make-vl-shadowcheck-state
                  • Vl-shadowcheck-state->lexscopes
                  • Vl-shadowcheck-state->design
                  • Vl-shadowcheck-state->ss
                  • Change-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-shadowcheck-state

This is a product type introduced by defprod.

Fields
lexscopes — vl-lexscopes
Lexical scopes, current up to this point.
ss — vl-scopestack
Proper scopestack with all implicit variables already added to it, and updated with whatever scopes we've descended through pushed onto it.
design — vl-design
Original design.

Subtopics

Vl-shadowcheck-state-p
Recognizer for vl-shadowcheck-state structures.
Vl-shadowcheck-state-fix
Fixing function for vl-shadowcheck-state structures.
Vl-shadowcheck-state-equiv
Basic equivalence relation for vl-shadowcheck-state structures.
Make-vl-shadowcheck-state
Basic constructor macro for vl-shadowcheck-state structures.
Vl-shadowcheck-state->lexscopes
Get the lexscopes field from a vl-shadowcheck-state.
Vl-shadowcheck-state->design
Get the design field from a vl-shadowcheck-state.
Vl-shadowcheck-state->ss
Get the ss field from a vl-shadowcheck-state.
Change-vl-shadowcheck-state
Modifying constructor for vl-shadowcheck-state structures.