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

    Vl-remove-declared-wires

    Filter names to remove wires that are already declared. We remove the names of any port declarations, ordinary declarations, global names, and imported names.

    Signature
    (vl-remove-declared-wires names st) → implicit
    Arguments
    names — Guard (string-listp names).
    st — Guard (vl-implicitst-p st).
    Returns
    implicit — Subset of names that don't have declarations already, e.g., names that we don't want to add local declarations for.
        Type (string-listp implicit).

    Definitions and Theorems

    Function: vl-remove-declared-wires

    (defun vl-remove-declared-wires (names st)
      (declare (xargs :guard (and (string-listp names)
                                  (vl-implicitst-p st))))
      (let ((__function__ 'vl-remove-declared-wires))
        (declare (ignorable __function__))
        (b* (((when (atom names)) nil)
             ((vl-implicitst st))
             (name1 (string-fix (car names)))
             ((when (or (hons-get name1 st.decls)
                        (hons-get name1 st.portdecls)
                        (hons-get name1 st.imports)
                        (vl-scopestack-find-item name1 st.ss)))
              (vl-remove-declared-wires (cdr names)
                                        st)))
          (cons name1
                (vl-remove-declared-wires (cdr names)
                                          st)))))

    Theorem: string-listp-of-vl-remove-declared-wires

    (defthm string-listp-of-vl-remove-declared-wires
      (b* ((implicit (vl-remove-declared-wires names st)))
        (string-listp implicit))
      :rule-classes :rewrite)

    Theorem: vl-remove-declared-wires-of-string-list-fix-names

    (defthm vl-remove-declared-wires-of-string-list-fix-names
      (equal (vl-remove-declared-wires (string-list-fix names)
                                       st)
             (vl-remove-declared-wires names st)))

    Theorem: vl-remove-declared-wires-string-list-equiv-congruence-on-names

    (defthm
         vl-remove-declared-wires-string-list-equiv-congruence-on-names
      (implies (str::string-list-equiv names names-equiv)
               (equal (vl-remove-declared-wires names st)
                      (vl-remove-declared-wires names-equiv st)))
      :rule-classes :congruence)

    Theorem: vl-remove-declared-wires-of-vl-implicitst-fix-st

    (defthm vl-remove-declared-wires-of-vl-implicitst-fix-st
      (equal (vl-remove-declared-wires names (vl-implicitst-fix st))
             (vl-remove-declared-wires names st)))

    Theorem: vl-remove-declared-wires-vl-implicitst-equiv-congruence-on-st

    (defthm
          vl-remove-declared-wires-vl-implicitst-equiv-congruence-on-st
      (implies (vl-implicitst-equiv st st-equiv)
               (equal (vl-remove-declared-wires names st)
                      (vl-remove-declared-wires names st-equiv)))
      :rule-classes :congruence)