Produce a list of two-input
(vl-make-gates-for-and/or/xor outs lhses rhses type name loc atts nf warnings) → (mv warnings new-gateinsts nf)
We generate the replacement gates for a multi-input
OUTS: (temp1 temp2 ... tempN-2 Out) LHSES: (i1 temp1 temp2 ... tempN-2) RHSES: (i2 i3 .... iN-1 iN)
We march down the three main input-lists, zipping them together into new gate instances. The new gateinsts we return are intended to replace the original gate.
Function:
(defun vl-make-gates-for-and/or/xor (outs lhses rhses type name loc atts nf warnings) (declare (xargs :guard (and (vl-plainarglist-p outs) (vl-plainarglist-p lhses) (vl-plainarglist-p rhses) (member type '(:vl-and :vl-or :vl-xor)) (stringp name) (vl-location-p loc) (vl-atts-p atts) (vl-namefactory-p nf) (vl-warninglist-p warnings)))) (declare (xargs :guard (and (same-lengthp outs lhses) (same-lengthp outs rhses)))) (let ((__function__ 'vl-make-gates-for-and/or/xor)) (declare (ignorable __function__)) (b* (((when (atom outs)) (mv (ok) nil nf)) (warnings (let ((expr (vl-plainarg->expr (car outs)))) (if (and expr (equal (vl-expr->finalwidth expr) 1)) (ok) (fatal :type :vl-bad-gate :msg "~a0: output terminal expression has width ~x1, but ~ should have width 1. The expression is ~a2." :args (list loc (and expr (vl-expr->finalwidth expr)) expr))))) (warnings (let ((expr (vl-plainarg->expr (car lhses)))) (if (and expr (equal (vl-expr->finalwidth expr) 1)) (ok) (fatal :type :vl-bad-gate :msg "~a0: input terminal expression has width ~x1, but ~ should have width 1. The expression is ~a2." :args (list loc (and expr (vl-expr->finalwidth expr)) expr))))) (warnings (let ((expr (vl-plainarg->expr (car rhses)))) (if (and expr (equal (vl-expr->finalwidth expr) 1)) (ok) (fatal :type :vl-bad-gate :msg "~a0: input terminal expression has width ~x1 but ~ should have width 1. The expression is ~a2." :args (list loc (and expr (vl-expr->finalwidth expr)) expr))))) ((mv new-name nf) (vl-namefactory-indexed-name name nf)) (gate1 (make-vl-gateinst :name new-name :type type :args (list (car outs) (car lhses) (car rhses)) :range nil :atts atts :loc loc)) ((mv warnings rest nf) (vl-make-gates-for-and/or/xor (cdr outs) (cdr lhses) (cdr rhses) type name loc atts nf warnings))) (mv warnings (cons gate1 rest) nf))))
Theorem:
(defthm vl-warninglist-p-of-vl-make-gates-for-and/or/xor.warnings (b* (((mv ?warnings ?new-gateinsts ?nf) (vl-make-gates-for-and/or/xor outs lhses rhses type name loc atts nf warnings))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-gateinstlist-p-of-vl-make-gates-for-and/or/xor.new-gateinsts (implies (and (force (vl-plainarglist-p outs)) (force (vl-plainarglist-p lhses)) (force (vl-plainarglist-p rhses)) (force ((lambda (acl2::x acl2::l) (return-last 'acl2::mbe1-raw (acl2::member-eql-exec acl2::x acl2::l) (return-last 'progn (acl2::member-eql-exec$guard-check acl2::x acl2::l) (member-equal acl2::x acl2::l)))) type '(:vl-and :vl-or :vl-xor))) (force (stringp name)) (force (vl-location-p loc)) (force (vl-atts-p atts)) (force (vl-namefactory-p nf)) (force (vl-warninglist-p warnings)) (force (same-lengthp outs lhses)) (force (same-lengthp outs rhses))) (b* (((mv ?warnings ?new-gateinsts ?nf) (vl-make-gates-for-and/or/xor outs lhses rhses type name loc atts nf warnings))) (vl-gateinstlist-p new-gateinsts))) :rule-classes :rewrite)
Theorem:
(defthm vl-namefactory-p-of-vl-make-gates-for-and/or/xor.nf (implies (and (force (vl-plainarglist-p outs)) (force (vl-plainarglist-p lhses)) (force (vl-plainarglist-p rhses)) (force ((lambda (acl2::x acl2::l) (return-last 'acl2::mbe1-raw (acl2::member-eql-exec acl2::x acl2::l) (return-last 'progn (acl2::member-eql-exec$guard-check acl2::x acl2::l) (member-equal acl2::x acl2::l)))) type '(:vl-and :vl-or :vl-xor))) (force (stringp name)) (force (vl-location-p loc)) (force (vl-atts-p atts)) (force (vl-namefactory-p nf)) (force (vl-warninglist-p warnings)) (force (same-lengthp outs lhses)) (force (same-lengthp outs rhses))) (b* (((mv ?warnings ?new-gateinsts ?nf) (vl-make-gates-for-and/or/xor outs lhses rhses type name loc atts nf warnings))) (vl-namefactory-p nf))) :rule-classes :rewrite)
Theorem:
(defthm vl-make-gates-for-and/or/xor-mvtypes-1 (true-listp (mv-nth 1 (vl-make-gates-for-and/or/xor outs lhses rhses type name loc atts nf warnings))) :rule-classes :type-prescription)