		Search-engine friendly clone of the ACL2 documentation.

Replicate-insts

Vl-module-port-widths

Determine the widths of a module's ports.

Signature
(vl-module-port-widths ports inst warnings) → (mv successp warnings port-widths)
Arguments: ports — The module's ports.
Guard (vl-portlist-p ports).; inst — The module instance we're trying to replicate; serves merely as a context for warnings.
Guard (vl-modinst-p inst).; warnings — Ordinary warnings accumulator.
Guard (vl-warninglist-p warnings).
Returns: successp — Type (booleanp successp).; warnings — Type (vl-warninglist-p warnings).; port-widths — Type (implies successp (and (pos-listp port-widths) (equal (len port-widths) (len ports)))) .

We fail and cause fatal errors if any port is blank or does not have a positive width.

Definitions and Theorems

Function: vl-module-port-widths

(defun vl-module-port-widths (ports inst warnings)
 (declare (xargs :guard (and (vl-portlist-p ports)
                             (vl-modinst-p inst)
                             (vl-warninglist-p warnings))))
 (let ((__function__ 'vl-module-port-widths))
  (declare (ignorable __function__))
  (b*
   ((ports (vl-portlist-fix ports))
    (warnings (vl-warninglist-fix warnings))
    (inst (vl-modinst-fix inst))
    ((when (atom ports))
     (mv t warnings nil))
    (port1 (vl-port-fix (car ports)))
    ((when (eq (tag port1) :vl-interfaceport))
     (mv
        nil
        (fatal :type :vl-replicate-fail
               :msg "~a0: bozo need to implement interface ports.~%"
               :args (list inst))
        nil))
    (expr1 (vl-regularport->expr port1))
    (width1 (and expr1 (vl-expr->finalwidth expr1)))
    ((unless (posp width1))
     (mv
      nil
      (fatal
        :type :vl-replicate-fail
        :msg "~a0: width of ~a1 is ~x2; expected a positive number."
        :args (list inst port1
                    (and expr1 (vl-expr->finalwidth expr1))))
      nil))
    ((mv successp warnings cdr-sizes)
     (vl-module-port-widths (cdr ports)
                            inst warnings))
    ((unless successp)
     (mv nil warnings nil)))
   (mv t warnings (cons width1 cdr-sizes)))))

Theorem: booleanp-of-vl-module-port-widths.successp

(defthm booleanp-of-vl-module-port-widths.successp
  (b* (((mv ?successp ?warnings ?port-widths)
        (vl-module-port-widths ports inst warnings)))
    (booleanp successp))
  :rule-classes :type-prescription)

Theorem: vl-warninglist-p-of-vl-module-port-widths.warnings

(defthm vl-warninglist-p-of-vl-module-port-widths.warnings
  (b* (((mv ?successp ?warnings ?port-widths)
        (vl-module-port-widths ports inst warnings)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-module-port-widths.port-widths

(defthm return-type-of-vl-module-port-widths.port-widths
  (b* (((mv ?successp ?warnings ?port-widths)
        (vl-module-port-widths ports inst warnings)))
    (implies successp
             (and (pos-listp port-widths)
                  (equal (len port-widths) (len ports)))))
  :rule-classes :rewrite)

Theorem: vl-module-port-widths-of-vl-portlist-fix-ports

(defthm vl-module-port-widths-of-vl-portlist-fix-ports
  (equal (vl-module-port-widths (vl-portlist-fix ports)
                                inst warnings)
         (vl-module-port-widths ports inst warnings)))

Theorem: vl-module-port-widths-vl-portlist-equiv-congruence-on-ports

(defthm vl-module-port-widths-vl-portlist-equiv-congruence-on-ports
 (implies (vl-portlist-equiv ports ports-equiv)
          (equal (vl-module-port-widths ports inst warnings)
                 (vl-module-port-widths ports-equiv inst warnings)))
 :rule-classes :congruence)

Theorem: vl-module-port-widths-of-vl-modinst-fix-inst

(defthm vl-module-port-widths-of-vl-modinst-fix-inst
  (equal (vl-module-port-widths ports (vl-modinst-fix inst)
                                warnings)
         (vl-module-port-widths ports inst warnings)))

Theorem: vl-module-port-widths-vl-modinst-equiv-congruence-on-inst

(defthm vl-module-port-widths-vl-modinst-equiv-congruence-on-inst
 (implies (vl-modinst-equiv inst inst-equiv)
          (equal (vl-module-port-widths ports inst warnings)
                 (vl-module-port-widths ports inst-equiv warnings)))
 :rule-classes :congruence)

Theorem: vl-module-port-widths-of-vl-warninglist-fix-warnings

(defthm vl-module-port-widths-of-vl-warninglist-fix-warnings
  (equal (vl-module-port-widths ports
                                inst (vl-warninglist-fix warnings))
         (vl-module-port-widths ports inst warnings)))

Theorem: vl-module-port-widths-vl-warninglist-equiv-congruence-on-warnings

(defthm
  vl-module-port-widths-vl-warninglist-equiv-congruence-on-warnings
 (implies (vl-warninglist-equiv warnings warnings-equiv)
          (equal (vl-module-port-widths ports inst warnings)
                 (vl-module-port-widths ports inst warnings-equiv)))
 :rule-classes :congruence)