Make a list of basic binary gate instances, e.g., AND, OR, XOR, NAND, NOR, or XNOR gates.
(vl-make-binary-gateinstlist type outs as bs &key atts (loc '*vl-fakeloc*)) → insts
Function:
(defun vl-make-binary-gateinstlist-fn (type outs as bs atts loc) (declare (xargs :guard (and (vl-gatetype-p type) (vl-exprlist-p outs) (vl-exprlist-p as) (vl-exprlist-p bs) (vl-atts-p atts) (vl-location-p loc)))) (declare (xargs :guard (and (member-eq type (list :vl-and :vl-nand :vl-nor :vl-or :vl-xor :vl-xnor)) (same-lengthp outs as) (same-lengthp outs bs)))) (let ((__function__ 'vl-make-binary-gateinstlist)) (declare (ignorable __function__)) (if (atom outs) nil (cons (vl-make-binary-gateinst type (car outs) (car as) (car bs) :atts atts :loc loc) (vl-make-binary-gateinstlist type (cdr outs) (cdr as) (cdr bs) :atts atts :loc loc)))))
Theorem:
(defthm vl-gateinstlist-p-of-vl-make-binary-gateinstlist (b* ((insts (vl-make-binary-gateinstlist-fn type outs as bs atts loc))) (vl-gateinstlist-p insts)) :rule-classes :rewrite)
Theorem:
(defthm len-of-vl-make-binary-gateinstlist (equal (len (vl-make-binary-gateinstlist type outs as bs :atts atts :loc loc)) (len outs)))
Theorem:
(defthm vl-make-binary-gateinstlist-fn-of-vl-gatetype-fix-type (equal (vl-make-binary-gateinstlist-fn (vl-gatetype-fix type) outs as bs atts loc) (vl-make-binary-gateinstlist-fn type outs as bs atts loc)))
Theorem:
(defthm vl-make-binary-gateinstlist-fn-vl-gatetype-equiv-congruence-on-type (implies (vl-gatetype-equiv type type-equiv) (equal (vl-make-binary-gateinstlist-fn type outs as bs atts loc) (vl-make-binary-gateinstlist-fn type-equiv outs as bs atts loc))) :rule-classes :congruence)
Theorem:
(defthm vl-make-binary-gateinstlist-fn-of-vl-exprlist-fix-outs (equal (vl-make-binary-gateinstlist-fn type (vl-exprlist-fix outs) as bs atts loc) (vl-make-binary-gateinstlist-fn type outs as bs atts loc)))
Theorem:
(defthm vl-make-binary-gateinstlist-fn-vl-exprlist-equiv-congruence-on-outs (implies (vl-exprlist-equiv outs outs-equiv) (equal (vl-make-binary-gateinstlist-fn type outs as bs atts loc) (vl-make-binary-gateinstlist-fn type outs-equiv as bs atts loc))) :rule-classes :congruence)
Theorem:
(defthm vl-make-binary-gateinstlist-fn-of-vl-exprlist-fix-as (equal (vl-make-binary-gateinstlist-fn type outs (vl-exprlist-fix as) bs atts loc) (vl-make-binary-gateinstlist-fn type outs as bs atts loc)))
Theorem:
(defthm vl-make-binary-gateinstlist-fn-vl-exprlist-equiv-congruence-on-as (implies (vl-exprlist-equiv as as-equiv) (equal (vl-make-binary-gateinstlist-fn type outs as bs atts loc) (vl-make-binary-gateinstlist-fn type outs as-equiv bs atts loc))) :rule-classes :congruence)
Theorem:
(defthm vl-make-binary-gateinstlist-fn-of-vl-exprlist-fix-bs (equal (vl-make-binary-gateinstlist-fn type outs as (vl-exprlist-fix bs) atts loc) (vl-make-binary-gateinstlist-fn type outs as bs atts loc)))
Theorem:
(defthm vl-make-binary-gateinstlist-fn-vl-exprlist-equiv-congruence-on-bs (implies (vl-exprlist-equiv bs bs-equiv) (equal (vl-make-binary-gateinstlist-fn type outs as bs atts loc) (vl-make-binary-gateinstlist-fn type outs as bs-equiv atts loc))) :rule-classes :congruence)
Theorem:
(defthm vl-make-binary-gateinstlist-fn-of-vl-atts-fix-atts (equal (vl-make-binary-gateinstlist-fn type outs as bs (vl-atts-fix atts) loc) (vl-make-binary-gateinstlist-fn type outs as bs atts loc)))
Theorem:
(defthm vl-make-binary-gateinstlist-fn-vl-atts-equiv-congruence-on-atts (implies (vl-atts-equiv atts atts-equiv) (equal (vl-make-binary-gateinstlist-fn type outs as bs atts loc) (vl-make-binary-gateinstlist-fn type outs as bs atts-equiv loc))) :rule-classes :congruence)
Theorem:
(defthm vl-make-binary-gateinstlist-fn-of-vl-location-fix-loc (equal (vl-make-binary-gateinstlist-fn type outs as bs atts (vl-location-fix loc)) (vl-make-binary-gateinstlist-fn type outs as bs atts loc)))
Theorem:
(defthm vl-make-binary-gateinstlist-fn-vl-location-equiv-congruence-on-loc (implies (vl-location-equiv loc loc-equiv) (equal (vl-make-binary-gateinstlist-fn type outs as bs atts loc) (vl-make-binary-gateinstlist-fn type outs as bs atts loc-equiv))) :rule-classes :congruence)