• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
      • Warnings
      • Primitives
      • Use-set
      • Syntax
      • Getting-started
      • Utilities
      • Loader
      • Transforms
        • Expression-sizing
        • Occform
        • Oprewrite
        • Expand-functions
        • Delayredux
        • Unparameterization
        • Caseelim
        • Split
        • Selresolve
        • Weirdint-elim
        • Vl-delta
        • Replicate-insts
          • Vl-replicated-instnames
          • Vl-modulelist-replicate
          • Argument-partitioning
          • Vl-replicate-gateinst
          • Vl-replicate-gateinstlist
          • Vl-module-port-widths
          • Vl-replicate-modinst
          • Vl-replicate-arguments
          • Vl-replicate-orig-instnames
          • Vl-assemble-modinsts
          • Vl-module-replicate
          • Vl-replicate-modinstlist
          • Vl-modinst-origname/idx
          • Vl-modinst-origname
          • Vl-gateinst-origname/idx
          • Vl-gateinst-origname
          • Vl-gateinst-origidx
          • Vl-modinst-origidx
          • Vl-design-replicate
          • Vl-some-modinst-array-p
          • Vl-some-gateinst-array-p
        • Rangeresolve
        • Propagate
        • Clean-selects
        • Clean-params
        • Blankargs
        • Inline-mods
        • Expr-simp
        • Trunc
        • Always-top
        • Gatesplit
        • Gate-elim
        • Expression-optimization
        • Elim-supplies
        • Wildelim
        • Drop-blankports
        • Clean-warnings
        • Addinstnames
        • Custom-transform-hooks
        • Annotate
        • Latchcode
        • Elim-unused-vars
        • Problem-modules
      • Lint
      • Mlib
      • Server
      • Kit
      • Printer
      • Esim-vl
      • Well-formedness
    • Sv
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• 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)