Make a list of unary (buf or not) gate instances.
(vl-make-unary-gateinstlist type outs ins &key atts (loc '*vl-fakeloc*)) → insts
Function:
(defun vl-make-unary-gateinstlist-fn (type outs ins atts loc) (declare (xargs :guard (and (vl-gatetype-p type) (vl-exprlist-p outs) (vl-exprlist-p ins) (vl-atts-p atts) (vl-location-p loc)))) (declare (xargs :guard (and (member type (list :vl-buf :vl-not)) (same-lengthp outs ins)))) (let ((__function__ 'vl-make-unary-gateinstlist)) (declare (ignorable __function__)) (if (atom outs) nil (cons (vl-make-unary-gateinst type (car outs) (car ins) :atts atts :loc loc) (vl-make-unary-gateinstlist type (cdr outs) (cdr ins) :atts atts :loc loc)))))
Theorem:
(defthm vl-gateinstlist-p-of-vl-make-unary-gateinstlist (b* ((insts (vl-make-unary-gateinstlist-fn type outs ins atts loc))) (vl-gateinstlist-p insts)) :rule-classes :rewrite)
Theorem:
(defthm vl-make-unary-gateinstlist-fn-of-vl-gatetype-fix-type (equal (vl-make-unary-gateinstlist-fn (vl-gatetype-fix type) outs ins atts loc) (vl-make-unary-gateinstlist-fn type outs ins atts loc)))
Theorem:
(defthm vl-make-unary-gateinstlist-fn-vl-gatetype-equiv-congruence-on-type (implies (vl-gatetype-equiv type type-equiv) (equal (vl-make-unary-gateinstlist-fn type outs ins atts loc) (vl-make-unary-gateinstlist-fn type-equiv outs ins atts loc))) :rule-classes :congruence)
Theorem:
(defthm vl-make-unary-gateinstlist-fn-of-vl-exprlist-fix-outs (equal (vl-make-unary-gateinstlist-fn type (vl-exprlist-fix outs) ins atts loc) (vl-make-unary-gateinstlist-fn type outs ins atts loc)))
Theorem:
(defthm vl-make-unary-gateinstlist-fn-vl-exprlist-equiv-congruence-on-outs (implies (vl-exprlist-equiv outs outs-equiv) (equal (vl-make-unary-gateinstlist-fn type outs ins atts loc) (vl-make-unary-gateinstlist-fn type outs-equiv ins atts loc))) :rule-classes :congruence)
Theorem:
(defthm vl-make-unary-gateinstlist-fn-of-vl-exprlist-fix-ins (equal (vl-make-unary-gateinstlist-fn type outs (vl-exprlist-fix ins) atts loc) (vl-make-unary-gateinstlist-fn type outs ins atts loc)))
Theorem:
(defthm vl-make-unary-gateinstlist-fn-vl-exprlist-equiv-congruence-on-ins (implies (vl-exprlist-equiv ins ins-equiv) (equal (vl-make-unary-gateinstlist-fn type outs ins atts loc) (vl-make-unary-gateinstlist-fn type outs ins-equiv atts loc))) :rule-classes :congruence)
Theorem:
(defthm vl-make-unary-gateinstlist-fn-of-vl-atts-fix-atts (equal (vl-make-unary-gateinstlist-fn type outs ins (vl-atts-fix atts) loc) (vl-make-unary-gateinstlist-fn type outs ins atts loc)))
Theorem:
(defthm vl-make-unary-gateinstlist-fn-vl-atts-equiv-congruence-on-atts (implies (vl-atts-equiv atts atts-equiv) (equal (vl-make-unary-gateinstlist-fn type outs ins atts loc) (vl-make-unary-gateinstlist-fn type outs ins atts-equiv loc))) :rule-classes :congruence)
Theorem:
(defthm vl-make-unary-gateinstlist-fn-of-vl-location-fix-loc (equal (vl-make-unary-gateinstlist-fn type outs ins atts (vl-location-fix loc)) (vl-make-unary-gateinstlist-fn type outs ins atts loc)))
Theorem:
(defthm vl-make-unary-gateinstlist-fn-vl-location-equiv-congruence-on-loc (implies (vl-location-equiv loc loc-equiv) (equal (vl-make-unary-gateinstlist-fn type outs ins atts loc) (vl-make-unary-gateinstlist-fn type outs ins atts loc-equiv))) :rule-classes :congruence)