• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • 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-replicate-orig-instnames1
          • 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
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Replicate-insts

Vl-replicate-orig-instnames

Generate the Verilog-style names of the original instances (e.g., names with square-bracketed indices).

Signature

(vl-replicate-orig-instnames instname instrange) → names

Arguments

instname — Guard (maybe-stringp instname).

instrange — Guard (vl-range-p instrange).

Returns

names — Verilog-style names in highest-first order, e.g., ("foo[5]" "foo[4]" "foo[3]").
    Type (string-listp names).

These names are just going to be attributes for the new instances, which allow you to relate the original Verilog with the simplified Verilog. The order must match vl-replicated-instnames.

Definitions and Theorems

Function: vl-replicate-orig-instnames

(defun vl-replicate-orig-instnames (instname instrange)
 (declare (xargs :guard (and (maybe-stringp instname)
                             (vl-range-p instrange))))
 (declare (xargs :guard (vl-range-resolved-p instrange)))
 (let ((__function__ 'vl-replicate-orig-instnames))
   (declare (ignorable __function__))
   (b*
    ((left (vl-resolved->val (vl-range->msb instrange)))
     (right (vl-resolved->val (vl-range->lsb instrange)))
     (low (min left right))
     (high (max left right))
     (instname (or instname "unnamed"))
     (low-to-high (vl-replicate-orig-instnames1 low high instname)))
    (if (>= left right)
        (reverse low-to-high)
      low-to-high))))

Theorem: string-listp-of-vl-replicate-orig-instnames

(defthm string-listp-of-vl-replicate-orig-instnames
  (b* ((names (vl-replicate-orig-instnames instname instrange)))
    (string-listp names))
  :rule-classes :rewrite)

Theorem: len-of-vl-replicate-orig-instnames

(defthm len-of-vl-replicate-orig-instnames
  (equal (len (vl-replicate-orig-instnames instname instrange))
         (vl-range-size instrange)))

Theorem: vl-replicate-orig-instnames-of-maybe-string-fix-instname

(defthm vl-replicate-orig-instnames-of-maybe-string-fix-instname
  (equal (vl-replicate-orig-instnames (maybe-string-fix instname)
                                      instrange)
         (vl-replicate-orig-instnames instname instrange)))

Theorem: vl-replicate-orig-instnames-maybe-string-equiv-congruence-on-instname

(defthm
 vl-replicate-orig-instnames-maybe-string-equiv-congruence-on-instname
 (implies
     (maybe-string-equiv instname instname-equiv)
     (equal (vl-replicate-orig-instnames instname instrange)
            (vl-replicate-orig-instnames instname-equiv instrange)))
 :rule-classes :congruence)

Theorem: vl-replicate-orig-instnames-of-vl-range-fix-instrange

(defthm vl-replicate-orig-instnames-of-vl-range-fix-instrange
 (equal
     (vl-replicate-orig-instnames instname (vl-range-fix instrange))
     (vl-replicate-orig-instnames instname instrange)))

Theorem: vl-replicate-orig-instnames-vl-range-equiv-congruence-on-instrange

(defthm
 vl-replicate-orig-instnames-vl-range-equiv-congruence-on-instrange
 (implies
     (vl-range-equiv instrange instrange-equiv)
     (equal (vl-replicate-orig-instnames instname instrange)
            (vl-replicate-orig-instnames instname instrange-equiv)))
 :rule-classes :congruence)

Subtopics

Vl-replicate-orig-instnames1