Produce a list of
(vl-make-gates-for-buf/not in outs x nf warnings) → (mv new-warnings new-gateinsts nf)
We produce a list of gateinsts of the appropriate type, one to
drive each output in
Function:
(defun vl-make-gates-for-buf/not (in outs x nf warnings) (declare (xargs :guard (and (vl-plainarg-p in) (vl-plainarglist-p outs) (vl-gateinst-p x) (vl-namefactory-p nf) (vl-warninglist-p warnings)))) (let ((__function__ 'vl-make-gates-for-buf/not)) (declare (ignorable __function__)) (b* (((when (atom outs)) (mv (ok) nil nf)) (warnings (if (not (vl-gateinst->range x)) (ok) (fatal :type :vl-bad-gate :msg "~a0: expected all instance arrays to have been ~ eliminated, but found a range. Did you forget to run ~ the replicate-insts transform?" :args (list x)))) (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 has width ~x1 but we only ~ support 1-bit outputs. The expression for the bad ~ terminal is ~a2." :args (list x (and expr (vl-expr->finalwidth expr)) expr))))) (origname-s (or (vl-gateinst->name x) "unnamed")) (origname-atom (make-vl-atom :guts (vl-string origname-s))) (atts (cons (cons "VL_GATESPLIT" origname-atom) (vl-gateinst->atts x))) ((mv new-name nf) (vl-namefactory-indexed-name origname-s nf)) (inst1 (make-vl-gateinst :name new-name :type (vl-gateinst->type x) :args (list (car outs) in) :loc (vl-gateinst->loc x) :atts atts)) ((mv warnings rest nf) (vl-make-gates-for-buf/not in (cdr outs) x nf warnings))) (mv (ok) (cons inst1 rest) nf))))
Theorem:
(defthm vl-warninglist-p-of-vl-make-gates-for-buf/not.new-warnings (b* (((mv ?new-warnings ?new-gateinsts ?nf) (vl-make-gates-for-buf/not in outs x nf warnings))) (vl-warninglist-p new-warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-gateinstlist-p-of-vl-make-gates-for-buf/not.new-gateinsts (implies (and (force (vl-plainarg-p in)) (force (vl-plainarglist-p outs)) (force (vl-gateinst-p x)) (force (vl-namefactory-p nf)) (force (vl-warninglist-p warnings))) (b* (((mv ?new-warnings ?new-gateinsts ?nf) (vl-make-gates-for-buf/not in outs x nf warnings))) (vl-gateinstlist-p new-gateinsts))) :rule-classes :rewrite)
Theorem:
(defthm vl-namefactory-p-of-vl-make-gates-for-buf/not.nf (implies (and (force (vl-plainarg-p in)) (force (vl-plainarglist-p outs)) (force (vl-gateinst-p x)) (force (vl-namefactory-p nf)) (force (vl-warninglist-p warnings))) (b* (((mv ?new-warnings ?new-gateinsts ?nf) (vl-make-gates-for-buf/not in outs x nf warnings))) (vl-namefactory-p nf))) :rule-classes :rewrite)
Theorem:
(defthm vl-make-gates-for-buf/not-mvtypes-1 (true-listp (mv-nth 1 (vl-make-gates-for-buf/not in outs x nf warnings))) :rule-classes :type-prescription)