		Search-engine friendly clone of the ACL2 documentation.

Gatesplit

Vl-gatesplit-buf/not

Split up a multi-output buf or not gate, if necessary.

Signature
(vl-gatesplit-buf/not x nf warnings) → (mv warnings new-gateinsts nf)
Arguments: x — Guard (vl-gateinst-p x).; nf — Guard (vl-namefactory-p nf).; warnings — Guard (vl-warninglist-p warnings).
Returns: warnings — Type (vl-warninglist-p warnings).; new-gateinsts — Type (vl-gateinstlist-p new-gateinsts), given the guard.; nf — Type (vl-namefactory-p nf), given the guard.

From Section 7.3, buf and not gates have one input (the last terminal) and one or more outputs (all other terminals). We split up multi-output versions of these gates into many single-output versions, e.g.,

not(o1, o2, ..., on, i);
  -->
not(o1, i);
not(o2, i);
  ...
not(on, i);

We verified this with Cadence, in xf-gatesplit.v.

Signature: (vl-gatesplit-buf/not x nf warnings) returns (mv warnings' new-gateinsts nf').

x is an instance of a buf or not gate.
nf is a vl-namefactory-p for generating fresh names.

The new-gateinsts we return should be used to replace x in the module.

Definitions and Theorems

Function: vl-gatesplit-buf/not

(defun vl-gatesplit-buf/not (x nf warnings)
 (declare (xargs :guard (and (vl-gateinst-p x)
                             (vl-namefactory-p nf)
                             (vl-warninglist-p warnings))))
 (declare (xargs :guard (member (vl-gateinst->type x)
                                '(:vl-not :vl-buf))))
 (let ((__function__ 'vl-gatesplit-buf/not))
  (declare (ignorable __function__))
  (b*
   ((args (list-fix (vl-gateinst->args x)))
    (nargs (length args))
    ((when (< nargs 2))
     (mv (fatal :type :vl-bad-gate
                :msg "~a0: gate illegally has ~x1 argument(s)."
                :args (list x nargs))
         (list x)
         nf))
    (input (car (last args)))
    (outputs (butlast args 1))
    (in-expr (vl-plainarg->expr input))
    ((when (not (and in-expr
                     (equal (vl-expr->finalwidth in-expr)
                            1))))
     (mv
      (fatal
       :type :vl-bad-gate
       :msg
       "~a0: input terminal has width ~x1, but we only ~
                         support 1-bit inputs."
       :args (list x
                   (and in-expr (vl-expr->finalwidth in-expr))))
      (list x)
      nf))
    ((when (eql nargs 2))
     (mv (ok) (list x) nf)))
   (vl-make-gates-for-buf/not input outputs x nf warnings))))

Theorem: vl-warninglist-p-of-vl-gatesplit-buf/not.warnings

(defthm vl-warninglist-p-of-vl-gatesplit-buf/not.warnings
  (b* (((mv ?warnings ?new-gateinsts ?nf)
        (vl-gatesplit-buf/not x nf warnings)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: vl-gateinstlist-p-of-vl-gatesplit-buf/not.new-gateinsts

(defthm vl-gateinstlist-p-of-vl-gatesplit-buf/not.new-gateinsts
 (implies
  (and
   (force (vl-gateinst-p x))
   (force (vl-namefactory-p nf))
   (force (vl-warninglist-p warnings))
   (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))))
     (vl-gateinst->type$inline x)
     '(:vl-not :vl-buf))))
  (b* (((mv ?warnings ?new-gateinsts ?nf)
        (vl-gatesplit-buf/not x nf warnings)))
    (vl-gateinstlist-p new-gateinsts)))
 :rule-classes :rewrite)

Theorem: vl-namefactory-p-of-vl-gatesplit-buf/not.nf

(defthm vl-namefactory-p-of-vl-gatesplit-buf/not.nf
 (implies
  (and
   (force (vl-gateinst-p x))
   (force (vl-namefactory-p nf))
   (force (vl-warninglist-p warnings))
   (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))))
     (vl-gateinst->type$inline x)
     '(:vl-not :vl-buf))))
  (b* (((mv ?warnings ?new-gateinsts ?nf)
        (vl-gatesplit-buf/not x nf warnings)))
    (vl-namefactory-p nf)))
 :rule-classes :rewrite)

Theorem: vl-gatesplit-buf/not-mvtypes-1

(defthm vl-gatesplit-buf/not-mvtypes-1
  (true-listp (mv-nth 1 (vl-gatesplit-buf/not x nf warnings)))
  :rule-classes :type-prescription)

Subtopics

Vl-make-gates-for-buf/not: Produce a list of buf or not gates.