		Search-engine friendly clone of the ACL2 documentation.

Always-top

Vl-always-convert-regport

Convert a reg portdecl into a wire portdecl.

Signature
(vl-always-convert-regport x) → new-x
Arguments: x — Guard (vl-portdecl-p x).
Returns: new-x — Type (vl-portdecl-p new-x).

Definitions and Theorems

Function: vl-always-convert-regport

(defun vl-always-convert-regport (x)
 (declare (xargs :guard (vl-portdecl-p x)))
 (let ((__function__ 'vl-always-convert-regport))
   (declare (ignorable __function__))
   (b* (((vl-portdecl x) (vl-portdecl-fix x))
        ((unless (and (eq (vl-datatype-kind x.type)
                          :vl-coretype)
                      (member (vl-coretype->name x.type)
                              '(:vl-reg :vl-logic))))
         (raise "Not actually a portdecl reg?  ~x0" x)
         x)
        (dims (vl-coretype->pdims x.type))
        ((unless (and (atom (vl-coretype->udims x.type))
                      (or (atom dims)
                          (and (atom (cdr dims))
                               (vl-range-p (car dims))))))
         (raise "Multi-dimensional array on portdecl reg? ~x0"
                x)
         x))
     (change-vl-portdecl x
                         :type (change-vl-coretype x.type
                                                   :name :vl-logic)
                         :nettype :vl-wire
                         :atts (acons (hons-copy "VL_CONVERTED_REG")
                                      nil x.atts)))))

Theorem: vl-portdecl-p-of-vl-always-convert-regport

(defthm vl-portdecl-p-of-vl-always-convert-regport
  (b* ((new-x (vl-always-convert-regport x)))
    (vl-portdecl-p new-x))
  :rule-classes :rewrite)

Theorem: vl-always-convert-regport-of-vl-portdecl-fix-x

(defthm vl-always-convert-regport-of-vl-portdecl-fix-x
  (equal (vl-always-convert-regport (vl-portdecl-fix x))
         (vl-always-convert-regport x)))

Theorem: vl-always-convert-regport-vl-portdecl-equiv-congruence-on-x

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