		Search-engine friendly clone of the ACL2 documentation.

Argresolve

Vl-gateinst-dirassign

Arity-checks a gate instance and annotates its arguments with their directions.

Signature
(vl-gateinst-dirassign x warnings) → (mv warnings new-x)
Arguments: x — Guard (vl-gateinst-p x).; warnings — Guard (vl-warninglist-p warnings).
Returns: warnings — Type (vl-warninglist-p warnings).; new-x — Semantically equivalent to x.
Type (vl-gateinst-p new-x).

If x is a well-formed gate instance, then no fatal warnings will be added and every argument of x-prime will be given the correct :dir annotation, following the rules in Chapter 7 of the Verilog-2005 specification.

If x is a not well-formed (i.e., it has an improper arity), then it will be returned unchanged and a fatal warning will be added.

We also check for blank arguments in gates during this function. BOZO this is convenient but isn't necessarily a very sensible place to do this.

Definitions and Theorems

Function: vl-gateinst-dirassign

(defun vl-gateinst-dirassign (x warnings)
 (declare (xargs :guard (and (vl-gateinst-p x)
                             (vl-warninglist-p warnings))))
 (let ((__function__ 'vl-gateinst-dirassign))
  (declare (ignorable __function__))
  (b*
   ((x (vl-gateinst-fix x))
    ((vl-gateinst x) x)
    (nargs (len x.args))
    (warnings
     (if (vl-plainarglist-blankfree-p x.args)
         (ok)
      (warn
       :type :vl-warn-blank-gateargs
       :msg
       "~a0 has \"blank\" arguments; we treat these as ~
                      unconnected wires, but other tools like Cadence's ~
                      Verilog-XL simulator do not seem to support this."
       :args (list x))))
    ((mv warnings args-prime)
     (case
      x.type
      ((:vl-and :vl-nand
                :vl-nor :vl-or
                :vl-xor :vl-xnor)
       (if (< nargs 2)
           (mv (fatal :type :vl-bad-gate
                      :msg "~a0 has ~s1."
                      :args (list x
                                  (if (= nargs 1)
                                      "only one argument"
                                    "no arguments")))
               x.args)
        (mv
         (ok)
         (cons
             (change-vl-plainarg (car x.args)
                                 :dir :vl-output)
             (vl-plainarglist-assign-dir :vl-input (cdr x.args))))))
      ((:vl-buf :vl-not)
       (if (< nargs 2)
           (mv (fatal :type :vl-bad-gate
                      :msg "~a0 has ~s1."
                      :args (list x
                                  (if (= nargs 1)
                                      "only one argument"
                                    "no arguments")))
               x.args)
         (mv (ok)
             (vl-plainarglist-assign-last-dir
                  :vl-input
                  (vl-plainarglist-assign-dir :vl-output x.args)))))
      ((:vl-bufif0 :vl-bufif1
                   :vl-notif0 :vl-notif1
                   :vl-nmos :vl-pmos
                   :vl-rnmos :vl-rpmos)
       (if
        (/= nargs 3)
        (mv
         (fatal
          :type :vl-bad-gate
          :msg
          "~a0 has ~x1 argument~s2, but must have ~
                                exactly 3 arguments."
          :args (list x nargs (if (= nargs 1) "s" "")))
         x.args)
        (mv
         (ok)
         (cons
             (change-vl-plainarg (car x.args)
                                 :dir :vl-output)
             (vl-plainarglist-assign-dir :vl-input (cdr x.args))))))
      ((:vl-tranif1 :vl-tranif0
                    :vl-rtranif1 :vl-rtranif0)
       (if
        (/= nargs 3)
        (mv
         (fatal
          :type :vl-bad-gate
          :msg
          "~a0 has ~x1 argument~s2, but must have ~
                                exactly 3 arguments."
          :args (list x nargs (if (= nargs 1) "s" "")))
         x.args)
        (mv (ok)
            (list (change-vl-plainarg (first x.args)
                                      :dir :vl-inout)
                  (change-vl-plainarg (second x.args)
                                      :dir :vl-inout)
                  (change-vl-plainarg (third x.args)
                                      :dir :vl-input)))))
      ((:vl-tran :vl-rtran)
       (if
        (/= nargs 2)
        (mv
         (fatal
          :type :vl-bad-gate
          :msg
          "~a0 has ~x1 argument~s2, but must have ~
                                exactly 2 arguments."
          :args (list x nargs (if (= nargs 1) "s" "")))
         x.args)
        (mv (ok)
            (list (change-vl-plainarg (first x.args)
                                      :dir :vl-inout)
                  (change-vl-plainarg (second x.args)
                                      :dir :vl-inout)))))
      ((:vl-cmos :vl-rcmos)
       (if
        (/= nargs 4)
        (mv
         (fatal
          :type :vl-bad-gate
          :msg
          "~a0 has ~x1 argument~s2, but must have ~
                                exactly 4 arguments."
          :args (list x nargs (if (= nargs 1) "s" "")))
         x.args)
        (mv (ok)
            (list (change-vl-plainarg (first x.args)
                                      :dir :vl-output)
                  (change-vl-plainarg (second x.args)
                                      :dir :vl-input)
                  (change-vl-plainarg (third x.args)
                                      :dir :vl-input)
                  (change-vl-plainarg (fourth x.args)
                                      :dir :vl-input)))))
      ((:vl-pullup :vl-pulldown)
       (mv (ok)
           (vl-plainarglist-assign-dir :vl-output x.args)))
      (otherwise (progn$ (impossible)
                         (mv (ok) x.args)))))
    (x-prime (change-vl-gateinst x
                                 :args args-prime)))
   (mv (ok) x-prime))))

Theorem: vl-warninglist-p-of-vl-gateinst-dirassign.warnings

(defthm vl-warninglist-p-of-vl-gateinst-dirassign.warnings
  (b* (((mv ?warnings ?new-x)
        (vl-gateinst-dirassign x warnings)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: vl-gateinst-p-of-vl-gateinst-dirassign.new-x

(defthm vl-gateinst-p-of-vl-gateinst-dirassign.new-x
  (b* (((mv ?warnings ?new-x)
        (vl-gateinst-dirassign x warnings)))
    (vl-gateinst-p new-x))
  :rule-classes :rewrite)

Theorem: vl-gateinst-dirassign-of-vl-gateinst-fix-x

(defthm vl-gateinst-dirassign-of-vl-gateinst-fix-x
  (equal (vl-gateinst-dirassign (vl-gateinst-fix x)
                                warnings)
         (vl-gateinst-dirassign x warnings)))

Theorem: vl-gateinst-dirassign-vl-gateinst-equiv-congruence-on-x

(defthm vl-gateinst-dirassign-vl-gateinst-equiv-congruence-on-x
  (implies (vl-gateinst-equiv x x-equiv)
           (equal (vl-gateinst-dirassign x warnings)
                  (vl-gateinst-dirassign x-equiv warnings)))
  :rule-classes :congruence)

Theorem: vl-gateinst-dirassign-of-vl-warninglist-fix-warnings

(defthm vl-gateinst-dirassign-of-vl-warninglist-fix-warnings
  (equal (vl-gateinst-dirassign x (vl-warninglist-fix warnings))
         (vl-gateinst-dirassign x warnings)))

Theorem: vl-gateinst-dirassign-vl-warninglist-equiv-congruence-on-warnings

(defthm
  vl-gateinst-dirassign-vl-warninglist-equiv-congruence-on-warnings
  (implies (vl-warninglist-equiv warnings warnings-equiv)
           (equal (vl-gateinst-dirassign x warnings)
                  (vl-gateinst-dirassign x warnings-equiv)))
  :rule-classes :congruence)

Subtopics

Vl-plainarglist-assign-last-dir: Assign DIR to the last argument in the list X, leave the other arguments unchanged.
Vl-plainarglist-assign-dir: Assign DIR to every argument in the list X.