• 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)