		Search-engine friendly clone of the ACL2 documentation.

Always-top

Vl-always-convert-reg

Convert a register into a wire.

Signature
(vl-always-convert-reg x) → netdecl
Arguments: x — Guard (vl-vardecl-p x).
Returns: netdecl — Type (vl-vardecl-p netdecl).

When we replace always blocks with explicit instances, we have to convert the register declaration into an ordinary net declaration.

We expect that this function should only ever be called on registers that have passed vl-always-check-reg, so we cause a hard error if the register has array dimensions.

Definitions and Theorems

Function: vl-always-convert-reg

(defun vl-always-convert-reg (x)
 (declare (xargs :guard (vl-vardecl-p x)))
 (let ((__function__ 'vl-always-convert-reg))
  (declare (ignorable __function__))
  (b*
   (((vl-vardecl x) x)
    ((unless (vl-simplereg-p x))
     (raise
      "Expected all variables to convert to be simple regs and not arrays.")
     (vl-vardecl-fix x))
    (range (vl-simplereg->range x))
    (new-type (make-vl-coretype :name :vl-logic
                                :signedp (vl-simplereg->signedp x)
                                :pdims (and range (list range)))))
   (change-vl-vardecl x
                      :type new-type
                      :nettype :vl-wire
                      :atts (acons (hons-copy "VL_CONVERTED_REG")
                                   nil x.atts)))))

Theorem: vl-vardecl-p-of-vl-always-convert-reg

(defthm vl-vardecl-p-of-vl-always-convert-reg
  (b* ((netdecl (vl-always-convert-reg x)))
    (vl-vardecl-p netdecl))
  :rule-classes :rewrite)

Theorem: vl-always-convert-reg-of-vl-vardecl-fix-x

(defthm vl-always-convert-reg-of-vl-vardecl-fix-x
  (equal (vl-always-convert-reg (vl-vardecl-fix x))
         (vl-always-convert-reg x)))

Theorem: vl-always-convert-reg-vl-vardecl-equiv-congruence-on-x

(defthm vl-always-convert-reg-vl-vardecl-equiv-congruence-on-x
  (implies (vl-vardecl-equiv x x-equiv)
           (equal (vl-always-convert-reg x)
                  (vl-always-convert-reg x-equiv)))
  :rule-classes :congruence)