• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
      • Svex-stvs
      • Svex-fixpoint-decomposition-methodology
      • Sv-versus-esim
      • Svex-decomp
      • Svex-compose-dfs
      • Moddb
        • Moddb.lisp
        • Elab-mod
        • Moddb-path->wireidx/decl
        • Moddb-wireidx->path/decl
        • Moddb-path->wireidx
        • Moddb-address->wireidx
        • Moddb-address->wiredecl
        • Moddb-wireidx->path
        • Modscope-okp
      • Svex-compilation
      • Svmods
      • Svstmt
      • Sv-tutorial
      • Expressions
      • Symbolic-test-vector
      • Vl-to-svex
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Testing-utilities
  • Math

• Moddb

Moddb-address->wireidx

Convert a wire address into a wire index, given the scope from which the address is relative.

Signature

(moddb-address->wireidx addr scope moddb) → idx

Arguments

addr — Guard (address-p addr).

scope — Guard (modscope-p scope).

moddb — Guard (moddb-ok moddb).

Returns

idx — Type (iff (natp idx) idx).

Definitions and Theorems

Function: moddb-address->wireidx

(defun moddb-address->wireidx (addr scope moddb)
 (declare (xargs :stobjs (moddb)))
 (declare (xargs :guard (and (address-p addr)
                             (modscope-p scope)
                             (moddb-ok moddb))))
 (declare (xargs :guard (modscope-okp scope moddb)))
 (let ((__function__ 'moddb-address->wireidx))
  (declare (ignorable __function__))
  (b*
   (((address addr))
    ((modscope scope1)
     (if (eq addr.scope :root)
         (modscope->top scope)
       (modscope->nth addr.scope scope)))
    (local-idx (moddb-path->wireidx addr.path scope1.modidx moddb)))
   (and local-idx
        (+ local-idx scope1.wireoffset)))))

Theorem: return-type-of-moddb-address->wireidx

(defthm return-type-of-moddb-address->wireidx
  (b* ((idx (moddb-address->wireidx addr scope moddb)))
    (iff (natp idx) idx))
  :rule-classes :rewrite)

Theorem: moddb-address->wireidx-bound

(defthm moddb-address->wireidx-bound
 (let ((res (moddb-address->wireidx addr scope moddb)))
  (implies
   (and (moddb-ok moddb)
        (modscope-okp scope moddb)
        res)
   (< res
      (moddb-mod-totalwires (modscope->modidx (modscope->top scope))
                            moddb))))
 :rule-classes :linear)

Theorem: moddb-address->wireidx-of-address-fix-addr

(defthm moddb-address->wireidx-of-address-fix-addr
  (equal (moddb-address->wireidx (address-fix addr)
                                 scope moddb)
         (moddb-address->wireidx addr scope moddb)))

Theorem: moddb-address->wireidx-address-equiv-congruence-on-addr

(defthm moddb-address->wireidx-address-equiv-congruence-on-addr
  (implies (address-equiv addr addr-equiv)
           (equal (moddb-address->wireidx addr scope moddb)
                  (moddb-address->wireidx addr-equiv scope moddb)))
  :rule-classes :congruence)

Theorem: moddb-address->wireidx-of-modscope-fix-scope

(defthm moddb-address->wireidx-of-modscope-fix-scope
  (equal (moddb-address->wireidx addr (modscope-fix scope)
                                 moddb)
         (moddb-address->wireidx addr scope moddb)))

Theorem: moddb-address->wireidx-modscope-equiv-congruence-on-scope

(defthm moddb-address->wireidx-modscope-equiv-congruence-on-scope
  (implies (modscope-equiv scope scope-equiv)
           (equal (moddb-address->wireidx addr scope moddb)
                  (moddb-address->wireidx addr scope-equiv moddb)))
  :rule-classes :congruence)

Theorem: moddb-address->wireidx-of-moddb-fix-moddb

(defthm moddb-address->wireidx-of-moddb-fix-moddb
  (equal (moddb-address->wireidx addr scope (moddb-fix moddb))
         (moddb-address->wireidx addr scope moddb)))

Theorem: moddb-address->wireidx-moddb-equiv-congruence-on-moddb

(defthm moddb-address->wireidx-moddb-equiv-congruence-on-moddb
  (implies (moddb-equiv moddb moddb-equiv)
           (equal (moddb-address->wireidx addr scope moddb)
                  (moddb-address->wireidx addr scope moddb-equiv)))
  :rule-classes :congruence)