• 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-shadowcheck-reference-name
                • Vl-shadowcheck-aux
                • Vl-shadowcheck-reference-names
                • Vl-shadowcheck-declare-names
                • Vl-shadowcheck-declare-name
                • Vl-shadowcheck-fundecl
                • Vl-shadowcheck-declare-typedefs
                • Vl-shadowcheck-blockitemlist
                • Vl-shadowcheck-taskdecl
                • Vl-shadowcheck-portdecllist
                • Vl-shadowcheck-paramdecls
                • Vl-shadowcheck-taskdecls
                • Vl-shadowcheck-paramdecl
                • Vl-shadowcheck-gateinst
                • Vl-shadowcheck-vardecls
                • Vl-shadowcheck-vardecl
                • Vl-shadowcheck-portdecl
                • Vl-shadowcheck-modinst
                • Vl-shadowcheck-imports
                • Vl-shadowcheck-import
                • Vl-shadowcheck-fundecls
                • Vl-shadowcheck-blockitem
                • Vl-shadowcheck-ports
                • Vl-shadowcheck-port
                • Vl-shadowcheck-initial
                • Vl-shadowcheck-assign
                • Vl-shadowcheck-always
                • Vl-shadowcheck-alias
                • Vl-shadowcheck-state
                • Vl-shadowcheck-module
                • Vl-shadowcheck-modules
                • Vl-shadowcheck-push-scope
                • Vl-lexscopes
                • Vl-shadowcheck-design
                • Vl-shadowcheck-pop-scope
                • Vl-lexscope
              • Vl-stmt-check-undeclared
              • Vl-make-implicit-wires-main
              • Vl-fundecl-check-undeclared
              • Vl-warn-about-undeclared-wires
              • Vl-implicitst
              • 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

Shadowcheck

Sanity check to prevent tricky kinds of global name shadowing.

In some Verilog tools, top-level and imported declarations can sometimes be shadowed by local declarations for only part of a module. For instance,

parameter foo = 1;

module m ();
  logic [3:0] a = foo;     // references the global foo
  parameter foo = 2;
  logic [3:0] b = foo;     // references the local foo
endmodule

Throughout VL we generally abstract away from the parse order and expect to be able to traverse scopes in a simple set-like way. This approach makes supporting this kind of lexical shadowing a challenge. To avoid any problems due to this kind of shadowing, we implement a special check to prohibit globals from being used before they are locally declared.

This checking depends on the parse order. It occurs as part of the make-implicit-wires transform. Note that we do this checking after we have already introduced implicit wires, so we can assume that implicit wires have explicit declarations.

Subtopics

Vl-shadowcheck-reference-name
Vl-shadowcheck-aux
Main function for checking for name shadowing.
Vl-shadowcheck-reference-names
Vl-shadowcheck-declare-names
Vl-shadowcheck-declare-name
Vl-shadowcheck-fundecl
Vl-shadowcheck-declare-typedefs
Vl-shadowcheck-blockitemlist
Vl-shadowcheck-taskdecl
Vl-shadowcheck-portdecllist
Vl-shadowcheck-paramdecls
Vl-shadowcheck-taskdecls
Vl-shadowcheck-paramdecl
Vl-shadowcheck-gateinst
Vl-shadowcheck-vardecls
Vl-shadowcheck-vardecl
Vl-shadowcheck-portdecl
Vl-shadowcheck-modinst
Vl-shadowcheck-imports
Vl-shadowcheck-import
Vl-shadowcheck-fundecls
Vl-shadowcheck-blockitem
Vl-shadowcheck-ports
Vl-shadowcheck-port
Vl-shadowcheck-initial
Vl-shadowcheck-assign
Vl-shadowcheck-always
Vl-shadowcheck-alias
Vl-shadowcheck-state
Vl-shadowcheck-module
Vl-shadowcheck-modules
Vl-shadowcheck-push-scope
Vl-lexscopes
A stack of lexical scopes.
Vl-shadowcheck-design
Vl-shadowcheck-pop-scope
Vl-lexscope
Representation of a single, partial, lexical scope.