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

Convert a wire path relative to a module into a wire index and get its wire structure. The path may have one extra numeric component which is checked to see if it is a valid bitselect and returned as a separate value.

Signature

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

Arguments

path — Guard (path-p path).

modidx — Guard (natp modidx).

moddb — Guard (moddb-ok moddb).

Returns

wire — Type (implies (not errmsg) (wire-p wire)).

idx — Type (implies (not errmsg) (natp idx)).

bitsel — Type (maybe-natp bitsel).

Definitions and Theorems

Function: moddb-path->wireidx/decl

(defun moddb-path->wireidx/decl (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/decl))
  (declare (ignorable __function__))
  (path-case
   path :wire
   (b* (((stobj-get err idx wire)
         ((elab-mod (moddb->modsi modidx moddb)))
         (b* ((idx (elab-mod-wirename->idx path.name elab-mod))
              ((unless idx)
               (mv (msg "In module ~x0: Missing: ~s1"
                        (elab-mod->name elab-mod)
                        path.name)
                   nil nil))
              (wire (elab-mod-wiretablei idx elab-mod)))
           (mv nil idx wire)))
        ((when err) (mv err nil nil nil)))
     (mv nil wire idx nil))
   :scope
   (b*
    ((bit (path-case path.subpath
                     :wire (and (natp path.subpath.name)
                                path.subpath.name)
                     :scope nil))
     ((stobj-get wireidx wire offset submod modname err)
      ((elab-mod (moddb->modsi modidx moddb)))
      (b*
       ((wireidx
             (and bit
                  (elab-mod-wirename->idx path.namespace elab-mod)))
        (instidx (elab-mod-instname->idx path.namespace elab-mod))
        (modname (elab-mod->name elab-mod))
        ((unless (or instidx wireidx))
         (mv nil nil nil nil modname
             (msg "missing: ~s0" path.namespace))))
       (mv wireidx
           (and wireidx
                (elab-mod-wiretablei wireidx elab-mod))
           (and instidx
                (elab-mod->inst-wireoffset instidx elab-mod))
           (and instidx
                (elab-mod->inst-modidx instidx elab-mod))
           modname nil)))
     ((when err)
      (mv (msg "In module ~x0: ~@1" modname err)
          nil nil nil))
     ((mv err submod-wire rest-index bitsel)
      (if submod
          (moddb-path->wireidx/decl path.subpath submod moddb)
        (mv (msg "In module ~x0: missing submod: ~s1"
                 modname path.namespace)
            nil nil nil)))
     ((unless err)
      (mv nil submod-wire (+ offset rest-index)
          bitsel))
     ((unless wire) (mv err nil nil nil))
     ((wire wire))
     (in-bounds (and (>= bit wire.low-idx)
                     (< bit (+ wire.low-idx wire.width))))
     ((unless in-bounds)
      (mv (msg "In module ~x0: bitselect out of bounds: ~x1"
               modname bit)
          nil nil nil)))
    (mv nil wire wireidx bit)))))

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

(defthm return-type-of-moddb-path->wireidx/decl.wire
  (b* (((mv ?errmsg ?wire ?idx ?bitsel)
        (moddb-path->wireidx/decl path modidx moddb)))
    (implies (not errmsg) (wire-p wire)))
  :rule-classes :rewrite)

Theorem: return-type-of-moddb-path->wireidx/decl.idx

(defthm return-type-of-moddb-path->wireidx/decl.idx
  (b* (((mv ?errmsg ?wire ?idx ?bitsel)
        (moddb-path->wireidx/decl path modidx moddb)))
    (implies (not errmsg) (natp idx)))
  :rule-classes :type-prescription)

Theorem: maybe-natp-of-moddb-path->wireidx/decl.bitsel

(defthm maybe-natp-of-moddb-path->wireidx/decl.bitsel
  (b* (((mv ?errmsg ?wire ?idx ?bitsel)
        (moddb-path->wireidx/decl path modidx moddb)))
    (maybe-natp bitsel))
  :rule-classes :type-prescription)

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

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

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

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

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

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

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

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

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

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

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

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

Theorem: moddb-path->wireidx/decl-bound

(defthm moddb-path->wireidx/decl-bound
  (b* (((mv ?errmsg ?wire ?idx ?bitsel)
        (moddb-path->wireidx/decl path modidx moddb)))
    (implies (and (moddb-ok moddb)
                  (< (nfix modidx)
                     (nfix (nth *moddb->nmods* moddb)))
                  (not errmsg))
             (< idx
                (moddb-mod-totalwires modidx moddb))))
  :rule-classes :linear)