• 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

Modscope-okp

Checks whether a modscope is well-formed, in that the module indices make sense and each nested module's wire/instance indices are completely contained within those of the outer module.

Signature

(modscope-okp x moddb) → *

Arguments

x — Guard (modscope-p x).

moddb — Guard (moddb-ok moddb).

Definitions and Theorems

Function: modscope-okp

(defun
 modscope-okp (x moddb)
 (declare (xargs :stobjs (moddb)))
 (declare (xargs :guard (and (modscope-p x) (moddb-ok moddb))))
 (let
    ((__function__ 'modscope-okp))
    (declare (ignorable __function__))
    (modscope-case
         x
         :top (< x.modidx (moddb->nmods moddb))
         :nested
         (b* (((unless (< x.modidx (moddb->nmods moddb)))
               nil)
              ((unless (modscope-okp x.upper moddb))
               nil)
              ((modscope f2) x.upper)
              (f2-totalwires (moddb-mod-totalwires f2.modidx moddb))
              (f2-totalinsts (moddb-mod-totalinsts f2.modidx moddb))
              (f1-totalwires (moddb-mod-totalwires x.modidx moddb))
              (f1-totalinsts (moddb-mod-totalinsts x.modidx moddb)))
             (and (<= f2.wireoffset x.wireoffset)
                  (<= (+ f1-totalwires x.wireoffset)
                      (+ f2-totalwires f2.wireoffset))
                  (<= f2.instoffset x.instoffset)
                  (<= (+ f1-totalinsts x.instoffset)
                      (+ f2-totalinsts f2.instoffset)))))))

Theorem: modscope-okp-implies-top-modidx-in-bounds

(defthm modscope-okp-implies-top-modidx-in-bounds
        (implies (modscope-okp x moddb)
                 (and (< (modscope->modidx x)
                         (nth *moddb->nmods* moddb))
                      (< (modscope->modidx x)
                         (nfix (nth *moddb->nmods* moddb)))))
        :rule-classes (:rewrite :linear))

Theorem: modscope-okp-of-modscope-fix-x

(defthm modscope-okp-of-modscope-fix-x
        (equal (modscope-okp (modscope-fix x) moddb)
               (modscope-okp x moddb)))

Theorem: modscope-okp-modscope-equiv-congruence-on-x

(defthm modscope-okp-modscope-equiv-congruence-on-x
        (implies (modscope-equiv x x-equiv)
                 (equal (modscope-okp x moddb)
                        (modscope-okp x-equiv moddb)))
        :rule-classes :congruence)

Theorem: modscope-okp-of-moddb-fix-moddb

(defthm modscope-okp-of-moddb-fix-moddb
        (equal (modscope-okp x (moddb-fix moddb))
               (modscope-okp x moddb)))

Theorem: modscope-okp-moddb-equiv-congruence-on-moddb

(defthm modscope-okp-moddb-equiv-congruence-on-moddb
        (implies (moddb-equiv moddb moddb-equiv)
                 (equal (modscope-okp x moddb)
                        (modscope-okp x moddb-equiv)))
        :rule-classes :congruence)