• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • 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
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Testing-utilities
  • Math

• Moddb

Moddb-path->wireidx

Convert a wire path relative to a module into a wire index.

Signature

(moddb-path->wireidx path modidx moddb) → idx

Arguments

path — Guard (path-p path).

modidx — Guard (natp modidx).

moddb — Guard (moddb-ok moddb).

Returns

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

Definitions and Theorems

Function: moddb-path->wireidx

(defun
  moddb-path->wireidx (path modidx moddb)
  (declare (xargs :stobjs (moddb)))
  (declare (xargs :guard (and (path-p path)
                              (natp modidx)
                              (moddb-ok moddb))))
  (declare (xargs :guard (< modidx (moddb->nmods moddb))))
  (let ((__function__ 'moddb-path->wireidx))
       (declare (ignorable __function__))
       (b* (((mv err & idx bitsel)
             (moddb-path->wireidx/decl path modidx moddb))
            ((when err)
             (b* (((stobj-get name)
                   ((elab-mod (moddb->modsi modidx moddb)))
                   (elab-mod->name elab-mod)))
                 (cw "Error looking up ~x1: ~@0~%from module: ~x2~%"
                     err path name)))
            ((when bitsel)
             (cw "Didn't expect a bit select: ~x0"
                 path)))
           idx)))

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

(defthm return-type-of-moddb-path->wireidx
        (b* ((idx (moddb-path->wireidx path modidx moddb)))
            (iff (natp idx) idx))
        :rule-classes :rewrite)

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

(defthm moddb-path->wireidx-of-path-fix-path
        (equal (moddb-path->wireidx (path-fix path)
                                    modidx moddb)
               (moddb-path->wireidx path modidx moddb)))

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

(defthm
     moddb-path->wireidx-path-equiv-congruence-on-path
     (implies (path-equiv path path-equiv)
              (equal (moddb-path->wireidx path modidx moddb)
                     (moddb-path->wireidx path-equiv modidx moddb)))
     :rule-classes :congruence)

Theorem: moddb-path->wireidx-of-nfix-modidx

(defthm moddb-path->wireidx-of-nfix-modidx
        (equal (moddb-path->wireidx path (nfix modidx)
                                    moddb)
               (moddb-path->wireidx path modidx moddb)))

Theorem: moddb-path->wireidx-nat-equiv-congruence-on-modidx

(defthm
     moddb-path->wireidx-nat-equiv-congruence-on-modidx
     (implies (nat-equiv modidx modidx-equiv)
              (equal (moddb-path->wireidx path modidx moddb)
                     (moddb-path->wireidx path modidx-equiv moddb)))
     :rule-classes :congruence)

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

(defthm moddb-path->wireidx-of-moddb-fix-moddb
        (equal (moddb-path->wireidx path modidx (moddb-fix moddb))
               (moddb-path->wireidx path modidx moddb)))

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

(defthm
     moddb-path->wireidx-moddb-equiv-congruence-on-moddb
     (implies (moddb-equiv moddb moddb-equiv)
              (equal (moddb-path->wireidx path modidx moddb)
                     (moddb-path->wireidx path modidx moddb-equiv)))
     :rule-classes :congruence)

Theorem: moddb-path->wireidx-type

(defthm moddb-path->wireidx-type
        (b* ((?idx (moddb-path->wireidx path modidx moddb)))
            (or (not idx) (natp idx)))
        :rule-classes :type-prescription)

Theorem: moddb-path->wireidx-bound

(defthm moddb-path->wireidx-bound
        (b* ((?idx (moddb-path->wireidx path modidx moddb)))
            (implies (and (moddb-ok moddb)
                          (< (nfix modidx)
                             (nfix (nth *moddb->nmods* moddb)))
                          idx)
                     (< idx
                        (moddb-mod-totalwires modidx moddb))))
        :rule-classes :linear)