Compute the vl-emodwire-ps for a variable declaration, in MSB-first order.
(vl-vardecl-msb-emodwires x warnings) → (mv successp warnings emodwires)
Function:
(defun vl-vardecl-msb-emodwires (x warnings) (declare (xargs :guard (and (vl-vardecl-p x) (vl-warninglist-p warnings)))) (let ((__function__ 'vl-vardecl-msb-emodwires)) (declare (ignorable __function__)) (b* (((vl-vardecl x) x) ((unless (vl-simplevar-p x)) (mv nil (fatal :type :vl-bad-vardecl :msg "~a0 is not yet supported: we only handle simple ~ wires and reg/logic variables with at most a single ~ range." :args (list x)) nil)) (range (vl-simplevar->range x)) ((unless (vl-maybe-range-resolved-p range)) (mv nil (fatal :type :vl-bad-vardecl :msg "~a0 has unresolved range ~a1." :args (list x range)) nil)) ((unless range) (mv t (ok) (list (vl-plain-wire-name x.name)))) (msb (vl-resolved->val (vl-range->msb range))) (lsb (vl-resolved->val (vl-range->lsb range))) (|w[msb:lsb]| (vl-emodwires-from-msb-to-lsb x.name msb lsb))) (mv t (ok) |w[msb:lsb]|))))
Theorem:
(defthm booleanp-of-vl-vardecl-msb-emodwires.successp (b* (((mv ?successp ?warnings ?emodwires) (vl-vardecl-msb-emodwires x warnings))) (booleanp successp)) :rule-classes :type-prescription)
Theorem:
(defthm vl-warninglist-p-of-vl-vardecl-msb-emodwires.warnings (b* (((mv ?successp ?warnings ?emodwires) (vl-vardecl-msb-emodwires x warnings))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-emodwirelist-p-of-vl-vardecl-msb-emodwires.emodwires (b* (((mv ?successp ?warnings ?emodwires) (vl-vardecl-msb-emodwires x warnings))) (vl-emodwirelist-p emodwires)) :rule-classes :rewrite)
Theorem:
(defthm true-listp-of-vl-vardecl-msb-emodwires (true-listp (mv-nth 2 (vl-vardecl-msb-emodwires x warnings))) :rule-classes :type-prescription)
Theorem:
(defthm basenames-of-vl-vardecl-msb-emodwires (implies (vl-vardecl-p x) (let ((wires (mv-nth 2 (vl-vardecl-msb-emodwires x warnings)))) (equal (vl-emodwirelist->basenames wires) (replicate (len wires) (vl-vardecl->name x))))))
Theorem:
(defthm unique-indicies-of-vl-vardecl-msb-emodwires (no-duplicatesp-equal (vl-emodwirelist->indices (mv-nth 2 (vl-vardecl-msb-emodwires x warnings)))))