• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • 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
              • 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
    • Make-implicit-wires

    Vl-genblock-under-cond-make-implicit-wires

    Only for genblocks that are found in conditional contexts, i.e., the then/else branches of if statements, or the bodies of case statements. (Scoping is tricky here).

    Signature
    (vl-genblock-under-cond-make-implicit-wires x st warnings) 
      → 
    (mv warnings st new-x)
    Arguments
    x — Guard (vl-genblock-p x).
    st — Guard (vl-implicitst-p st).
    warnings — Guard (vl-warninglist-p warnings).
    Returns
    warnings — Type (vl-warninglist-p warnings).
    st — Type (vl-implicitst-p st).
    new-x — Updated version of the block, extended with declarations for any implicit wires as necessary.
        Type (vl-genblock-p new-x).

    This is slightly tricky because of the condnest case. For background see SystemVerilog-2012 Section 27.5 and see vl-genblock.

    We are careful here not to introduce new scopes when we go into condnest ifs. Note though that the only places we could introduce implicit wires are always in the leaves of the IF structure, and the leaves always have a block.