• 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
        • Rangeresolve
        • Propagate
        • Clean-selects
        • Clean-params
        • Blankargs
        • Inline-mods
        • Expr-simp
        • Trunc
        • Always-top
          • Edgesynth
          • Stmtrewrite
          • Cblock
          • Vl-always-convert-regports
          • Vl-always-convert-regs
          • Stmttemps
          • Edgesplit
          • Vl-always-check-reg
          • Vl-convert-regs
          • Latchsynth
          • Vl-always-check-regs
          • Vl-match-always-at-some-edges
          • Unelse
          • Vl-always-convert-reg
          • Vl-design-always-backend
          • Vl-stmt-guts
          • Vl-always-convert-regport
          • Vl-always-scary-regs
          • Eliminitial
          • Ifmerge
          • Vl-edge-control-p
          • Elimalways
        • 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

• Always-top

Vl-convert-regs

Signature

(vl-convert-regs cvtregs vardecls portdecls) 
  → 
(mv new-vardecls new-portdecls)

Arguments

cvtregs — Guard (string-listp cvtregs).

vardecls — Guard (vl-vardecllist-p vardecls).

portdecls — Guard (vl-portdecllist-p portdecls).

Returns

new-vardecls — Type (vl-vardecllist-p new-vardecls).

new-portdecls — Type (vl-portdecllist-p new-portdecls).

Definitions and Theorems

Function: vl-convert-regs

(defun vl-convert-regs (cvtregs vardecls portdecls)
 (declare (xargs :guard (and (string-listp cvtregs)
                             (vl-vardecllist-p vardecls)
                             (vl-portdecllist-p portdecls))))
 (let ((__function__ 'vl-convert-regs))
   (declare (ignorable __function__))
   (b*
    ((cvtregs (string-list-fix cvtregs))
     (vardecls (vl-vardecllist-fix vardecls))
     (portdecls (vl-portdecllist-fix portdecls))
     (non-regs
          (difference (mergesort cvtregs)
                      (mergesort (vl-vardecllist->names vardecls))))
     ((when non-regs)
      (raise "Trying to convert non-registers: ~x0.~%"
             non-regs)
      (mv vardecls portdecls))
     ((mv vardecls-to-convert
          vardecls-to-leave-alone)
      (vl-filter-vardecls cvtregs vardecls))
     ((mv portdecls-to-convert
          portdecls-to-leave-alone)
      (vl-filter-portdecls cvtregs portdecls))
     (converted-vardecls
          (vl-always-convert-regs vardecls-to-convert))
     (converted-portdecls
          (vl-always-convert-regports portdecls-to-convert)))
    (mv (append converted-vardecls
                vardecls-to-leave-alone)
        (append converted-portdecls
                portdecls-to-leave-alone)))))

Theorem: vl-vardecllist-p-of-vl-convert-regs.new-vardecls

(defthm vl-vardecllist-p-of-vl-convert-regs.new-vardecls
  (b* (((mv ?new-vardecls ?new-portdecls)
        (vl-convert-regs cvtregs vardecls portdecls)))
    (vl-vardecllist-p new-vardecls))
  :rule-classes :rewrite)

Theorem: vl-portdecllist-p-of-vl-convert-regs.new-portdecls

(defthm vl-portdecllist-p-of-vl-convert-regs.new-portdecls
  (b* (((mv ?new-vardecls ?new-portdecls)
        (vl-convert-regs cvtregs vardecls portdecls)))
    (vl-portdecllist-p new-portdecls))
  :rule-classes :rewrite)

Theorem: vl-convert-regs-of-string-list-fix-cvtregs

(defthm vl-convert-regs-of-string-list-fix-cvtregs
  (equal (vl-convert-regs (string-list-fix cvtregs)
                          vardecls portdecls)
         (vl-convert-regs cvtregs vardecls portdecls)))

Theorem: vl-convert-regs-string-list-equiv-congruence-on-cvtregs

(defthm vl-convert-regs-string-list-equiv-congruence-on-cvtregs
  (implies
       (str::string-list-equiv cvtregs cvtregs-equiv)
       (equal (vl-convert-regs cvtregs vardecls portdecls)
              (vl-convert-regs cvtregs-equiv vardecls portdecls)))
  :rule-classes :congruence)

Theorem: vl-convert-regs-of-vl-vardecllist-fix-vardecls

(defthm vl-convert-regs-of-vl-vardecllist-fix-vardecls
  (equal (vl-convert-regs cvtregs (vl-vardecllist-fix vardecls)
                          portdecls)
         (vl-convert-regs cvtregs vardecls portdecls)))

Theorem: vl-convert-regs-vl-vardecllist-equiv-congruence-on-vardecls

(defthm vl-convert-regs-vl-vardecllist-equiv-congruence-on-vardecls
  (implies
       (vl-vardecllist-equiv vardecls vardecls-equiv)
       (equal (vl-convert-regs cvtregs vardecls portdecls)
              (vl-convert-regs cvtregs vardecls-equiv portdecls)))
  :rule-classes :congruence)

Theorem: vl-convert-regs-of-vl-portdecllist-fix-portdecls

(defthm vl-convert-regs-of-vl-portdecllist-fix-portdecls
  (equal (vl-convert-regs cvtregs vardecls
                          (vl-portdecllist-fix portdecls))
         (vl-convert-regs cvtregs vardecls portdecls)))

Theorem: vl-convert-regs-vl-portdecllist-equiv-congruence-on-portdecls

(defthm
      vl-convert-regs-vl-portdecllist-equiv-congruence-on-portdecls
  (implies
       (vl-portdecllist-equiv portdecls portdecls-equiv)
       (equal (vl-convert-regs cvtregs vardecls portdecls)
              (vl-convert-regs cvtregs vardecls portdecls-equiv)))
  :rule-classes :congruence)