		Search-engine friendly clone of the ACL2 documentation.

Vl-gatesplit-buf/not

Vl-make-gates-for-buf/not

Produce a list of buf or not gates.

Signature
(vl-make-gates-for-buf/not in outs x nf warnings) → (mv new-warnings new-gateinsts nf)
Arguments: in — Input terminal to a multi-output buf/not gate.
Guard (vl-plainarg-p in).; outs — Output terminals for the gate.
Guard (vl-plainarglist-p outs).; x — The gate itself, used for good error messages, and also to identify which kind of gate we are working with, its location, etc.
Guard (vl-gateinst-p x).; nf — For generating fresh names.
Guard (vl-namefactory-p nf).; warnings — Ordinary warnings accumulator.
Guard (vl-warninglist-p warnings).
Returns: new-warnings — Type (vl-warninglist-p new-warnings).; new-gateinsts — New gate instances that individually drive the outs.
Type (vl-gateinstlist-p new-gateinsts), given the guard.; nf — Type (vl-namefactory-p nf), given the guard.

We produce a list of gateinsts of the appropriate type, one to drive each output in outs with in.

Definitions and Theorems

Function: vl-make-gates-for-buf/not

(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: vl-warninglist-p-of-vl-make-gates-for-buf/not.new-warnings

(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: vl-gateinstlist-p-of-vl-make-gates-for-buf/not.new-gateinsts

(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: vl-namefactory-p-of-vl-make-gates-for-buf/not.nf

(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: vl-make-gates-for-buf/not-mvtypes-1

(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)