• 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
            • 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-make-implicit-wires-main

Top level routine for adding implicit wires to a module's load items.

Signature

(vl-make-implicit-wires-main loaditems ifports ss warnings) 
  → 
(mv newitems warnings)

Arguments

loaditems — Module elements in parse order.
    Guard (vl-genelementlist-p loaditems).

ifports — Interface ports for the module (we implicitly declare them first).
    Guard (vl-interfaceportlist-p ifports).

ss — Partial scopestack with info for superior scopes.
    Guard (vl-scopestack-p ss).

warnings — Ordinary warnings accumulator.
    Guard (vl-warninglist-p warnings).

Returns

newitems — Extended loaditems with implicit wires added.
    Type (vl-genelementlist-p newitems).

warnings — Possibly extended warnings.
    Type (vl-warninglist-p warnings).

Definitions and Theorems

Function: vl-make-implicit-wires-main

(defun vl-make-implicit-wires-main (loaditems ifports ss warnings)
 (declare (xargs :guard (and (vl-genelementlist-p loaditems)
                             (vl-interfaceportlist-p ifports)
                             (vl-scopestack-p ss)
                             (vl-warninglist-p warnings))))
 (let ((__function__ 'vl-make-implicit-wires-main))
   (declare (ignorable __function__))
   (b*
     ((ifports (vl-interfaceportlist-fix ifports))
      (decls (make-fast-alist (pairlis$ (vl-portlist->names ifports)
                                        (list-fix ifports))))
      (st (make-vl-implicitst :decls decls
                              :portdecls nil
                              :wildpkgs nil
                              :ss ss))
      (newitems nil)
      (impitems nil)
      ((mv warnings st newitems impitems)
       (vl-genelementlist-make-implicit-wires
            loaditems
            st newitems impitems warnings))
      (newitems (append newitems
                        (vl-modelementlist->genelements impitems)))
      ((vl-implicitst st))
      (newitems (vl-make-port-implicit-wires newitems st.decls nil))
      (- (fast-alist-free st.portdecls))
      (- (fast-alist-free st.decls)))
     (mv newitems warnings))))

Theorem: vl-genelementlist-p-of-vl-make-implicit-wires-main.newitems

(defthm vl-genelementlist-p-of-vl-make-implicit-wires-main.newitems
 (b* (((mv ?newitems ?warnings)
       (vl-make-implicit-wires-main loaditems ifports ss warnings)))
   (vl-genelementlist-p newitems))
 :rule-classes :rewrite)

Theorem: vl-warninglist-p-of-vl-make-implicit-wires-main.warnings

(defthm vl-warninglist-p-of-vl-make-implicit-wires-main.warnings
 (b* (((mv ?newitems ?warnings)
       (vl-make-implicit-wires-main loaditems ifports ss warnings)))
   (vl-warninglist-p warnings))
 :rule-classes :rewrite)

Theorem: vl-make-implicit-wires-main-of-vl-genelementlist-fix-loaditems

(defthm
     vl-make-implicit-wires-main-of-vl-genelementlist-fix-loaditems
 (equal
      (vl-make-implicit-wires-main (vl-genelementlist-fix loaditems)
                                   ifports ss warnings)
      (vl-make-implicit-wires-main loaditems ifports ss warnings)))

Theorem: vl-make-implicit-wires-main-vl-genelementlist-equiv-congruence-on-loaditems

(defthm
 vl-make-implicit-wires-main-vl-genelementlist-equiv-congruence-on-loaditems
 (implies
  (vl-genelementlist-equiv loaditems loaditems-equiv)
  (equal (vl-make-implicit-wires-main loaditems ifports ss warnings)
         (vl-make-implicit-wires-main
              loaditems-equiv ifports ss warnings)))
 :rule-classes :congruence)

Theorem: vl-make-implicit-wires-main-of-vl-interfaceportlist-fix-ifports

(defthm
    vl-make-implicit-wires-main-of-vl-interfaceportlist-fix-ifports
 (equal
     (vl-make-implicit-wires-main loaditems
                                  (vl-interfaceportlist-fix ifports)
                                  ss warnings)
     (vl-make-implicit-wires-main loaditems ifports ss warnings)))

Theorem: vl-make-implicit-wires-main-vl-interfaceportlist-equiv-congruence-on-ifports

(defthm
 vl-make-implicit-wires-main-vl-interfaceportlist-equiv-congruence-on-ifports
 (implies
  (vl-interfaceportlist-equiv ifports ifports-equiv)
  (equal (vl-make-implicit-wires-main loaditems ifports ss warnings)
         (vl-make-implicit-wires-main
              loaditems ifports-equiv ss warnings)))
 :rule-classes :congruence)

Theorem: vl-make-implicit-wires-main-of-vl-scopestack-fix-ss

(defthm vl-make-implicit-wires-main-of-vl-scopestack-fix-ss
  (equal
       (vl-make-implicit-wires-main
            loaditems ifports (vl-scopestack-fix ss)
            warnings)
       (vl-make-implicit-wires-main loaditems ifports ss warnings)))

Theorem: vl-make-implicit-wires-main-vl-scopestack-equiv-congruence-on-ss

(defthm
   vl-make-implicit-wires-main-vl-scopestack-equiv-congruence-on-ss
 (implies
  (vl-scopestack-equiv ss ss-equiv)
  (equal (vl-make-implicit-wires-main loaditems ifports ss warnings)
         (vl-make-implicit-wires-main
              loaditems ifports ss-equiv warnings)))
 :rule-classes :congruence)

Theorem: vl-make-implicit-wires-main-of-vl-warninglist-fix-warnings

(defthm vl-make-implicit-wires-main-of-vl-warninglist-fix-warnings
 (equal
      (vl-make-implicit-wires-main loaditems ifports
                                   ss (vl-warninglist-fix warnings))
      (vl-make-implicit-wires-main loaditems ifports ss warnings)))

Theorem: vl-make-implicit-wires-main-vl-warninglist-equiv-congruence-on-warnings

(defthm
 vl-make-implicit-wires-main-vl-warninglist-equiv-congruence-on-warnings
 (implies
  (vl-warninglist-equiv warnings warnings-equiv)
  (equal (vl-make-implicit-wires-main loaditems ifports ss warnings)
         (vl-make-implicit-wires-main
              loaditems ifports ss warnings-equiv)))
 :rule-classes :congruence)