• 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-wireidx->path/decl

Convert a wire index to a path relative to the module it's in, and additionally return the wire declaation.

Signature

(moddb-wireidx->path/decl wireidx modidx moddb) 
  → 
(mv path wire)

Arguments

wireidx — Guard (natp wireidx).

modidx — Guard (natp modidx).

moddb — Guard (moddb-ok moddb).

Returns

path — Type (path-p path).

wire — Type (wire-p wire).

Definitions and Theorems

Function: moddb-wireidx->path/decl

(defun
 moddb-wireidx->path/decl
 (wireidx modidx moddb)
 (declare (xargs :stobjs (moddb)))
 (declare (xargs :guard (and (natp wireidx)
                             (natp modidx)
                             (moddb-ok moddb))))
 (declare
      (xargs :guard (and (< modidx (moddb->nmods moddb))
                         (< wireidx
                            (moddb-mod-totalwires modidx moddb)))))
 (let ((__function__ 'moddb-wireidx->path/decl))
      (declare (ignorable __function__))
      (b* ((wireidx (lnfix wireidx))
           (modidx (lnfix modidx))
           ((unless (mbt (< modidx (moddb->nmods moddb))))
            (mv (path-fix nil) (wire-fix nil)))
           ((stobj-get donep wire/name nextmod nextwire)
            ((elab-mod (moddb->modsi modidx moddb)))
            (b* (((unless (mbt (< wireidx
                                  (elab-mod->totalwires elab-mod))))
                  (mv t (wire-fix nil) nil nil))
                 ((when (< wireidx (elab-mod-nwires elab-mod)))
                  (mv t (elab-mod-wiretablei wireidx elab-mod)
                      nil nil))
                 (inst (elab-mod-wire-find-inst wireidx elab-mod))
                 (name (elab-mod->instname inst elab-mod))
                 (nextmod (elab-mod->inst-modidx inst elab-mod))
                 (offset (elab-mod->inst-wireoffset inst elab-mod))
                 (nextwire (- wireidx offset)))
                (mv nil name nextmod nextwire)))
           ((when donep)
            (mv (make-path-wire :name (wire->name wire/name))
                wire/name))
           ((unless (mbt (< nextmod modidx)))
            (mv (path-fix nil) (wire-fix nil)))
           ((mv subpath wire)
            (moddb-wireidx->path/decl nextwire nextmod moddb)))
          (mv (make-path-scope :subpath subpath
                               :namespace wire/name)
              wire))))

Theorem: path-p-of-moddb-wireidx->path/decl.path

(defthm path-p-of-moddb-wireidx->path/decl.path
        (b* (((mv ?path ?wire)
              (moddb-wireidx->path/decl wireidx modidx moddb)))
            (path-p path))
        :rule-classes :rewrite)

Theorem: wire-p-of-moddb-wireidx->path/decl.wire

(defthm wire-p-of-moddb-wireidx->path/decl.wire
        (b* (((mv ?path ?wire)
              (moddb-wireidx->path/decl wireidx modidx moddb)))
            (wire-p wire))
        :rule-classes :rewrite)

Theorem: moddb-wireidx->path/decl-of-nfix-wireidx

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

Theorem: moddb-wireidx->path/decl-nat-equiv-congruence-on-wireidx

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

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

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

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

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

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

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

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

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