		Search-engine friendly clone of the ACL2 documentation.

Gate-elim

Vl-gateinst-gate-elim

Try to convert a single gate into one of VL's primitive modules.

Signature
(vl-gateinst-gate-elim x primalist warnings) → (mv warnings gateinsts modinsts addmods)
Arguments: x — Guard (vl-gateinst-p x).; primalist — Mapping from gate types to primitive modules.
Guard (vl-primalist-p primalist).; warnings — Guard (vl-warninglist-p warnings).
Returns: warnings — Type (vl-warninglist-p warnings).; gateinsts — Type (vl-gateinstlist-p gateinsts), given (force (vl-gateinst-p x)).; modinsts — Type (vl-modinstlist-p modinsts), given (force (vl-gateinst-p x)).; addmods — Type (vl-modulelist-p addmods), given (force (vl-gateinst-p x)).

We try to convert the gate instance x into an instance of the corresponding primitive VL module. We return new lists of gateinsts and modinsts that should collectively replace this gate instance. The idea is that the replacement gateinsts/modinsts should be equivalent to the gate being eliminated.

We may fail to eliminate x for several reasons, for instance:

it has more than the usual number of arguments (higher arity gates can simplified by gatesplit,
it is an array of gates (these can be split up by replicate-insts),
it has blank arguments (these can be handled by blankargs), or
its arguments are not one-bit expressions, since these sometimes have odd semantics in Cadence (see for instance the comments in vl-make-gates-for-buf/not, which is part of the gatesplit transform.)

In case of such a failure, we add non-fatal warnings to explain what happened and leave the gate unchanged.

Definitions and Theorems

Function: vl-gateinst-gate-elim

(defun vl-gateinst-gate-elim (x primalist warnings)
 (declare (xargs :guard (and (vl-gateinst-p x)
                             (vl-primalist-p primalist)
                             (vl-warninglist-p warnings))))
 (let ((__function__ 'vl-gateinst-gate-elim))
  (declare (ignorable __function__))
  (b*
   (((vl-gateinst x) x)
    (target (cdr (hons-assoc-equal x.type primalist)))
    (exprs (vl-plainarglist->exprs x.args))
    ((unless target)
     (mv
      (warn
       :type :vl-gate-elim-fail
       :msg
       "~a0: gates of type ~x1 are not supported by ~
                        gate-elim; leaving this gate unchanged."
       :args (list x x.type))
      (list x)
      nil nil))
    (target (vl-module-fix target))
    (ports (vl-module->ports target))
    ((unless (and (not x.range)
                  (not (vl-collect-interface-ports ports))
                  (same-lengthp x.args ports)
                  (not (member nil exprs))
                  (all-equalp 1 (vl-exprlist->finalwidths exprs))))
     (mv
      (warn
       :type :vl-gate-elim-fail
       :msg
       "~a0: gates with ~s1 are not supported by gate-elim; ~
                        leaving this gate unchanged."
       :args (list x
                   (cond (x.range "arrays")
                         ((not (same-lengthp x.args ports))
                          "extra arguments")
                         ((member nil exprs) "blank arguments")
                         (t "wide arguments"))))
      (list x)
      nil nil))
    (args (vl-add-portnames-to-plainargs x.args ports))
    (modinst
     (make-vl-modinst :instname x.name
                      :modname (vl-module->name target)
                      :portargs (make-vl-arguments-plain :args args)
                      :paramargs (make-vl-paramargs-plain :args nil)
                      :loc x.loc)))
   (mv (ok)
       nil (list modinst)
       (list target)))))

Theorem: vl-warninglist-p-of-vl-gateinst-gate-elim.warnings

(defthm vl-warninglist-p-of-vl-gateinst-gate-elim.warnings
  (b* (((mv ?warnings ?gateinsts ?modinsts ?addmods)
        (vl-gateinst-gate-elim x primalist warnings)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: vl-gateinstlist-p-of-vl-gateinst-gate-elim.gateinsts

(defthm vl-gateinstlist-p-of-vl-gateinst-gate-elim.gateinsts
  (implies (force (vl-gateinst-p x))
           (b* (((mv ?warnings ?gateinsts ?modinsts ?addmods)
                 (vl-gateinst-gate-elim x primalist warnings)))
             (vl-gateinstlist-p gateinsts)))
  :rule-classes :rewrite)

Theorem: vl-modinstlist-p-of-vl-gateinst-gate-elim.modinsts

(defthm vl-modinstlist-p-of-vl-gateinst-gate-elim.modinsts
  (implies (force (vl-gateinst-p x))
           (b* (((mv ?warnings ?gateinsts ?modinsts ?addmods)
                 (vl-gateinst-gate-elim x primalist warnings)))
             (vl-modinstlist-p modinsts)))
  :rule-classes :rewrite)

Theorem: vl-modulelist-p-of-vl-gateinst-gate-elim.addmods

(defthm vl-modulelist-p-of-vl-gateinst-gate-elim.addmods
  (implies (force (vl-gateinst-p x))
           (b* (((mv ?warnings ?gateinsts ?modinsts ?addmods)
                 (vl-gateinst-gate-elim x primalist warnings)))
             (vl-modulelist-p addmods)))
  :rule-classes :rewrite)

Theorem: vl-gateinst-gate-elim-mvtypes-1

(defthm vl-gateinst-gate-elim-mvtypes-1
  (true-listp (mv-nth 1
                      (vl-gateinst-gate-elim x primalist warnings)))
  :rule-classes :type-prescription)

Theorem: vl-gateinst-gate-elim-mvtypes-2

(defthm vl-gateinst-gate-elim-mvtypes-2
  (true-listp (mv-nth 2
                      (vl-gateinst-gate-elim x primalist warnings)))
  :rule-classes :type-prescription)

Theorem: vl-gateinst-gate-elim-mvtypes-3

(defthm vl-gateinst-gate-elim-mvtypes-3
  (true-listp (mv-nth 3
                      (vl-gateinst-gate-elim x primalist warnings)))
  :rule-classes :type-prescription)