• 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
          • Vl-modulelist-elim-supplies
          • Vl-collect-supplies
          • Vl-module-elim-supplies
          • Vl-design-elim-supplies
        • Wildelim
        • Drop-blankports
        • Clean-warnings
        • Addinstnames
        • Custom-transform-hooks
        • Annotate
        • 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

• Elim-supplies

Vl-collect-supplies

Signature

(vl-collect-supplies x portdecls palist warnings) 
  → 
(mv warnings vardecls supply0s supply1s)

Arguments

x — Guard (vl-vardecllist-p x).

portdecls — Guard (vl-portdecllist-p portdecls).

palist — Guard (equal palist (vl-make-portdecl-alist portdecls)).

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

Returns

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

vardecls — The non-supply netdecls, which should be kept.
    Type (vl-vardecllist-p vardecls).

supply0s — Names of supply0 wires.
    Type (string-listp supply0s).

supply1s — Names of supply1 wires.
    Type (string-listp supply1s).

Definitions and Theorems

Function: vl-collect-supplies

(defun vl-collect-supplies (x portdecls palist warnings)
 (declare
    (xargs :guard (and (vl-vardecllist-p x)
                       (vl-portdecllist-p portdecls)
                       (vl-warninglist-p warnings)
                       (equal palist
                              (vl-make-portdecl-alist portdecls)))))
 (let ((__function__ 'vl-collect-supplies))
   (declare (ignorable __function__))
   (b*
    (((when (atom x)) (mv (ok) nil nil nil))
     ((mv warnings
          rest-decls rest-supply0 rest-supply1)
      (vl-collect-supplies (cdr x)
                           portdecls palist warnings))
     ((vl-vardecl x1)
      (vl-vardecl-fix (car x)))
     ((unless (member x1.nettype '(:vl-supply0 :vl-supply1)))
      (mv (ok)
          (cons x1 rest-decls)
          rest-supply0 rest-supply1))
     ((unless (eq (vl-datatype-kind x1.type)
                  :vl-coretype))
      (mv (fatal :type :vl-bad-supply
                 :msg "~a0: bad wire declared as a supply"
                 :args (list x1))
          (cons x1 rest-decls)
          rest-supply0 rest-supply1))
     ((vl-coretype x1.type))
     ((when (or (consp x1.type.pdims)
                (consp x1.type.udims)))
      (mv (fatal :type :vl-bad-supply
                 :msg "~a0: we do not support supplies with ranges."
                 :args (list x1))
          (cons x1 rest-decls)
          rest-supply0 rest-supply1))
     (portdecl (vl-fast-find-portdecl x1.name portdecls palist))
     ((unless portdecl)
      (mv warnings rest-decls
          (if (eq x1.nettype :vl-supply0)
              (cons x1.name rest-supply0)
            rest-supply0)
          (if (eq x1.nettype :vl-supply1)
              (cons x1.name rest-supply1)
            rest-supply1)))
     ((unless (eq (vl-portdecl->dir portdecl)
                  :vl-input))
      (mv (fatal :type :vl-bad-supply
                 :msg "~a0: we do not support supplies as ports."
                 :args (list x1))
          (cons x1 rest-decls)
          rest-supply0 rest-supply1))
     (new-atts (cons (if (eq x1.nettype :vl-supply0)
                         (cons "VL_SUPPLY_0" nil)
                       (cons "VL_SUPPLY_1" nil))
                     x1.atts))
     (new-x1 (change-vl-vardecl x1
                                :nettype :vl-wire
                                :atts new-atts)))
    (mv (ok)
        (cons new-x1 rest-decls)
        rest-supply0 rest-supply1))))

Theorem: vl-warninglist-p-of-vl-collect-supplies.warnings

(defthm vl-warninglist-p-of-vl-collect-supplies.warnings
  (b* (((mv ?warnings ?vardecls ?supply0s ?supply1s)
        (vl-collect-supplies x portdecls palist warnings)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: vl-vardecllist-p-of-vl-collect-supplies.vardecls

(defthm vl-vardecllist-p-of-vl-collect-supplies.vardecls
  (b* (((mv ?warnings ?vardecls ?supply0s ?supply1s)
        (vl-collect-supplies x portdecls palist warnings)))
    (vl-vardecllist-p vardecls))
  :rule-classes :rewrite)

Theorem: string-listp-of-vl-collect-supplies.supply0s

(defthm string-listp-of-vl-collect-supplies.supply0s
  (b* (((mv ?warnings ?vardecls ?supply0s ?supply1s)
        (vl-collect-supplies x portdecls palist warnings)))
    (string-listp supply0s))
  :rule-classes :rewrite)

Theorem: string-listp-of-vl-collect-supplies.supply1s

(defthm string-listp-of-vl-collect-supplies.supply1s
  (b* (((mv ?warnings ?vardecls ?supply0s ?supply1s)
        (vl-collect-supplies x portdecls palist warnings)))
    (string-listp supply1s))
  :rule-classes :rewrite)

Theorem: vl-collect-supplies-mvtypes-1

(defthm vl-collect-supplies-mvtypes-1
  (true-listp
       (mv-nth 1
               (vl-collect-supplies x portdecls palist warnings)))
  :rule-classes :type-prescription)

Theorem: vl-collect-supplies-mvtypes-2

(defthm vl-collect-supplies-mvtypes-2
  (true-listp
       (mv-nth 2
               (vl-collect-supplies x portdecls palist warnings)))
  :rule-classes :type-prescription)

Theorem: vl-collect-supplies-mvtypes-3

(defthm vl-collect-supplies-mvtypes-3
  (true-listp
       (mv-nth 3
               (vl-collect-supplies x portdecls palist warnings)))
  :rule-classes :type-prescription)

Theorem: vl-collect-supplies-of-vl-vardecllist-fix-x

(defthm vl-collect-supplies-of-vl-vardecllist-fix-x
  (equal (vl-collect-supplies (vl-vardecllist-fix x)
                              portdecls palist warnings)
         (vl-collect-supplies x portdecls palist warnings)))

Theorem: vl-collect-supplies-vl-vardecllist-equiv-congruence-on-x

(defthm vl-collect-supplies-vl-vardecllist-equiv-congruence-on-x
 (implies
    (vl-vardecllist-equiv x x-equiv)
    (equal (vl-collect-supplies x portdecls palist warnings)
           (vl-collect-supplies x-equiv portdecls palist warnings)))
 :rule-classes :congruence)

Theorem: vl-collect-supplies-of-vl-portdecllist-fix-portdecls

(defthm vl-collect-supplies-of-vl-portdecllist-fix-portdecls
  (equal (vl-collect-supplies x (vl-portdecllist-fix portdecls)
                              palist warnings)
         (vl-collect-supplies x portdecls palist warnings)))

Theorem: vl-collect-supplies-vl-portdecllist-equiv-congruence-on-portdecls

(defthm
  vl-collect-supplies-vl-portdecllist-equiv-congruence-on-portdecls
 (implies
    (vl-portdecllist-equiv portdecls portdecls-equiv)
    (equal (vl-collect-supplies x portdecls palist warnings)
           (vl-collect-supplies x portdecls-equiv palist warnings)))
 :rule-classes :congruence)

Theorem: vl-collect-supplies-of-vl-warninglist-fix-warnings

(defthm vl-collect-supplies-of-vl-warninglist-fix-warnings
  (equal (vl-collect-supplies x portdecls
                              palist (vl-warninglist-fix warnings))
         (vl-collect-supplies x portdecls palist warnings)))

Theorem: vl-collect-supplies-vl-warninglist-equiv-congruence-on-warnings

(defthm
    vl-collect-supplies-vl-warninglist-equiv-congruence-on-warnings
 (implies
    (vl-warninglist-equiv warnings warnings-equiv)
    (equal (vl-collect-supplies x portdecls palist warnings)
           (vl-collect-supplies x portdecls palist warnings-equiv)))
 :rule-classes :congruence)