• 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
      • Lint
      • Mlib
        • Scopestack
        • Filtering-by-name
        • Vl-namefactory
        • Substitution
        • Allexprs
        • Hid-tools
        • Vl-consteval
        • Range-tools
        • Lvalexprs
        • Hierarchy
        • Finding-by-name
        • Expr-tools
        • Expr-slicing
        • Stripping-functions
        • Stmt-tools
        • Modnamespace
        • Vl-parse-expr-from-str
        • Welltyped
        • Reordering-by-name
        • Flat-warnings
        • Genblob
        • Expr-building
        • Datatype-tools
        • Syscalls
        • Relocate
        • Expr-cleaning
        • Namemangle
          • Vl-namemangle-vardecls
          • Vl-namemangle-gateinsts
          • Vl-namemangle-modinsts
        • Caremask
        • Port-tools
        • Lvalues
      • Server
      • Kit
      • Printer
      • Esim-vl
      • Well-formedness
    • Sv
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Namemangle

Vl-namemangle-gateinsts

Safely rename gate instances, preferring names of the form prefix_{current-name}.

Signature

(vl-namemangle-gateinsts prefix gateinsts nf) 
  → 
(mv new-gateinsts new-nf)

Arguments

prefix — Guard (stringp prefix).

gateinsts — Guard (vl-gateinstlist-p gateinsts).

nf — Guard (vl-namefactory-p nf).

Returns

new-gateinsts — Type (vl-gateinstlist-p new-gateinsts).

new-nf — Type (vl-namefactory-p new-nf).

Definitions and Theorems

Function: vl-namemangle-gateinsts

(defun vl-namemangle-gateinsts (prefix gateinsts nf)
  (declare (xargs :guard (and (stringp prefix)
                              (vl-gateinstlist-p gateinsts)
                              (vl-namefactory-p nf))))
  (let ((__function__ 'vl-namemangle-gateinsts))
    (declare (ignorable __function__))
    (b* (((when (atom gateinsts))
          (mv nil (vl-namefactory-fix nf)))
         (instname1 (or (vl-gateinst->name (car gateinsts))
                        "g"))
         (want1 (cat prefix "_" instname1))
         ((mv fresh1 nf)
          (vl-namefactory-plain-name want1 nf))
         (inst1 (change-vl-gateinst (car gateinsts)
                                    :name fresh1))
         ((mv insts2 nf)
          (vl-namemangle-gateinsts prefix (cdr gateinsts)
                                   nf)))
      (mv (cons inst1 insts2) nf))))

Theorem: vl-gateinstlist-p-of-vl-namemangle-gateinsts.new-gateinsts

(defthm vl-gateinstlist-p-of-vl-namemangle-gateinsts.new-gateinsts
  (b* (((mv ?new-gateinsts ?new-nf)
        (vl-namemangle-gateinsts prefix gateinsts nf)))
    (vl-gateinstlist-p new-gateinsts))
  :rule-classes :rewrite)

Theorem: vl-namefactory-p-of-vl-namemangle-gateinsts.new-nf

(defthm vl-namefactory-p-of-vl-namemangle-gateinsts.new-nf
  (b* (((mv ?new-gateinsts ?new-nf)
        (vl-namemangle-gateinsts prefix gateinsts nf)))
    (vl-namefactory-p new-nf))
  :rule-classes :rewrite)

Theorem: vl-namemangle-gateinsts-mvtypes-0

(defthm vl-namemangle-gateinsts-mvtypes-0
 (true-listp (mv-nth 0
                     (vl-namemangle-gateinsts prefix gateinsts nf)))
 :rule-classes :type-prescription)

Theorem: len-of-vl-namemangle-gateinsts

(defthm len-of-vl-namemangle-gateinsts
  (b* (((mv new-gateinsts ?new-nf)
        (vl-namemangle-gateinsts loc gateinsts nf)))
    (equal (len new-gateinsts)
           (len gateinsts))))

Theorem: vl-namemangle-gateinsts-of-str-fix-prefix

(defthm vl-namemangle-gateinsts-of-str-fix-prefix
  (equal (vl-namemangle-gateinsts (str-fix prefix)
                                  gateinsts nf)
         (vl-namemangle-gateinsts prefix gateinsts nf)))

Theorem: vl-namemangle-gateinsts-streqv-congruence-on-prefix

(defthm vl-namemangle-gateinsts-streqv-congruence-on-prefix
  (implies
       (streqv prefix prefix-equiv)
       (equal (vl-namemangle-gateinsts prefix gateinsts nf)
              (vl-namemangle-gateinsts prefix-equiv gateinsts nf)))
  :rule-classes :congruence)

Theorem: vl-namemangle-gateinsts-of-vl-gateinstlist-fix-gateinsts

(defthm vl-namemangle-gateinsts-of-vl-gateinstlist-fix-gateinsts
 (equal
     (vl-namemangle-gateinsts prefix (vl-gateinstlist-fix gateinsts)
                              nf)
     (vl-namemangle-gateinsts prefix gateinsts nf)))

Theorem: vl-namemangle-gateinsts-vl-gateinstlist-equiv-congruence-on-gateinsts

(defthm
 vl-namemangle-gateinsts-vl-gateinstlist-equiv-congruence-on-gateinsts
 (implies
      (vl-gateinstlist-equiv gateinsts gateinsts-equiv)
      (equal (vl-namemangle-gateinsts prefix gateinsts nf)
             (vl-namemangle-gateinsts prefix gateinsts-equiv nf)))
 :rule-classes :congruence)

Theorem: vl-namemangle-gateinsts-of-vl-namefactory-fix-nf

(defthm vl-namemangle-gateinsts-of-vl-namefactory-fix-nf
  (equal (vl-namemangle-gateinsts prefix
                                  gateinsts (vl-namefactory-fix nf))
         (vl-namemangle-gateinsts prefix gateinsts nf)))

Theorem: vl-namemangle-gateinsts-vl-namefactory-equiv-congruence-on-nf

(defthm
      vl-namemangle-gateinsts-vl-namefactory-equiv-congruence-on-nf
  (implies
       (vl-namefactory-equiv nf nf-equiv)
       (equal (vl-namemangle-gateinsts prefix gateinsts nf)
              (vl-namemangle-gateinsts prefix gateinsts nf-equiv)))
  :rule-classes :congruence)