• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
      • Svex-stvs
      • Svex-decomposition-methodology
      • Sv-versus-esim
      • Svex-decomp
      • Svex-compose-dfs
      • Svex-compilation
      • Moddb
        • Moddb.lisp
          • Moddb-add-modinst-to-last
          • Moddb-add-module1
          • Moddb-norm
          • Elab-modlist-norm
          • Moddb-ok
          • Elab-modinsts-rem-dups
          • Moddb-add-modinst
          • Elab-mod-initialize-aliases
          • Modinstlist-add-modinsts
          • Moddb-mod-ok
          • Wirelist-rem-dups
          • Moddb-norm-p
          • Elab-mod$a-fix
          • Moddb-mod-order-ok
          • Moddb-mod-insts-ok
          • Elab-mod-wire-find-inst-aux
          • Svex-alist->absindexed
          • Modscope-push-frame
          • Moddb-modinst-ok
          • Lhspairs->absindexed
          • Moddb-mod-inst-wireoffset
          • Moddb-find-bad-modinst-order
          • Constraintlist->absindexed
          • Wirelist-remove-names
          • Moddb-mod-inst-instoffset
          • Lhspairs-named->indexed
          • Elab-modinst-fix
          • Moddb-mod-totalwires
          • Svar-map->absindexed
          • Moddb-modinst-order-ok
          • Moddb-mod-totalinsts
          • Moddb-find-bad-modinst
          • Modscope
          • Constraintlist-named->indexed
          • Assigns->absindexed
          • Moddb-indices-ok
          • Lhs->absindexed
          • Svar-map-named->indexed
          • Module-named->indexed
          • Moddb-find-bad-index
          • Assigns-named->indexed
          • Svar-named->indexed
          • Lhs-named->indexed
          • Elab-mod$c-add-wire
          • Moddb-modname-get-index
          • Moddb-maybe-grow
          • Lhspairs-named->indexed-aux-nrev
          • Elab-modinst-list-names
          • Elab-mod-wire-find-inst
          • Svar->absindexed
          • Moddb-path->wiredecl
          • Modalist-named->indexed
          • Lhspairs->absindexed-nrev
          • Elab-mod$ap
          • Elab-modinst-remove-names
          • Moddb-wireidx->paths
          • Moddb-mods-ok
          • Moddb-find-bad-mod
          • Elab-mod$c-add-inst
          • Elab-mod$c-modinsts-ok
          • Elab-modinst-remove-name
          • Modscope->nth
          • Moddb-basics-ok
          • Svex->absindexed-memo-ok
          • Svex-named->indexed-memo-ok
          • Svarlist-idxaddr-okp
          • Elab-modlist-normp
          • Wirelist-remove-name
          • Modscope->top
          • Moddb-fix
          • Elab-mod$a-add-inst
          • Elab-mod-wiresearch-smartpivot
          • Elab-mod$c-wires-ok
          • Update-elab-mod$a->totalwires
          • Update-elab-mod$a->totalinsts
          • Update-elab-mod$a->orig-mod
          • Update-elab-mod$a->name
          • Moddb-modinst-order-badguy
          • Elab-mod$a-add-wire
          • Elab-mod$a-wiretablei
          • Elab-mod-wiresearch-pivot
          • Elab-mod-wireoffset
          • Elab-mod-instoffset
          • Svar-idxaddr-okp
          • Paths-add-scope
          • Moddb-modinst-badguy
          • Moddb-mod-nwires
          • Moddb-mod-ninsts
          • Modalist-all-idxaddr-okp
          • Elab-mod$a->instname
          • Elab-mods->names
          • Elab-modinst$c-copy
          • Elab-mod$a->inst-wireoffset
          • Elab-mod$a->inst-instoffset
          • Moddb-elab-mod-stats
          • Moddb-contains-modnames
          • Elab-mod$c-inst-abstraction
          • Elab-mod$a->inst-modidx
          • Elab-mod$a-wirename->idx
          • Elab-mod$a-instname->idx
          • Elab-mod-add-wires
          • Modscope-top-bound
          • Modscope-local-bound
          • Constraintlist-add-scope
          • Moddb-modidx-get-name
          • Moddb-add-module
          • Elab-mod-wiresearch-dumbpivot
          • Update-moddb->nmods
          • Elab-mod$c->inst-wireoffset
          • Elab-mod$c->inst-modidx
          • Elab-mod$c->inst-instoffset
          • Elab-mod$c-wire-abstraction
          • Moddb-clear
          • Elab-mod$c->instname
          • Svex-mod->flatten
          • Names->paths
          • Modscope->wireoffset
          • Modscope->instoffset
          • Moddb-mod-badguy
          • Elab-modinsts-nodups-p
          • Wirelist-nodups-p
          • Nat-list-max
          • Modscope->modidx
          • Elab-mod-wiresearch-next-smartp
          • Elab-mod$a->totalwires
          • Elab-mod$a->totalinsts
          • Elab-mod$a->orig-mod
          • Elab-mod$a->name
          • Elab-mod$a-nwires
          • Elab-mod$a-ninsts
          • Elab-modinst$c-fix
          • Elab-mod-fix
          • Create-elab-mod$a
          • Pathlist
          • Module->db
          • Elab-modlist
          • Elab-modinst-list
          • Nrec-list-mods
          • Moddb->nmods
          • Nrec-list
          • Nrec
        • Elab-mod
        • Moddb-path->wireidx/decl
        • Moddb-wireidx->path/decl
        • Moddb-path->wireidx
        • Moddb-address->wireidx
        • Moddb-address->wiredecl
        • Moddb-wireidx->path
        • Modscope-okp
      • Svmods
      • Svstmt
      • Sv-tutorial
      • Expressions
      • Symbolic-test-vector
      • Vl-to-svex
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Moddb.lisp

Moddb-add-module1

Signature

(moddb-add-module1 elab-mod moddb) → (mv elab-mod1 moddb1)

Definitions and Theorems

Function: moddb-add-module1

(defun moddb-add-module1 (elab-mod moddb)
 (declare (xargs :stobjs (elab-mod moddb)))
 (declare
   (xargs
        :guard
        (and (moddb-basics-ok moddb)
             (< (moddb->nmods moddb)
                (moddb->mods-length moddb))
             (not (moddb-modname-get-index (elab-mod->name elab-mod)
                                           moddb)))))
 (let ((__function__ 'moddb-add-module1))
  (declare (ignorable __function__))
  (b*
   ((moddb (moddb-fix moddb))
    (elab-mod (elab-mod-fix elab-mod))
    ((unless
        (mbt (not (moddb-modname-get-index (elab-mod->name elab-mod)
                                           moddb))))
     (mv elab-mod moddb))
    (idx (lnfix (moddb->nmods moddb)))
    (moddb (update-moddb->nmods (+ 1 idx) moddb))
    (moddb (moddb->modname-idxes-put (elab-mod->name elab-mod)
                                     idx moddb)))
   (stobj-let ((new-elab-mod (moddb->modsi idx moddb)))
              (new-elab-mod elab-mod)
              (swap-elab-mods new-elab-mod elab-mod)
              (mv elab-mod moddb)))))

Theorem: moddb-add-module1-of-elab-mod$a-fix-elab-mod

(defthm moddb-add-module1-of-elab-mod$a-fix-elab-mod
  (equal (moddb-add-module1 (elab-mod$a-fix elab-mod)
                            moddb)
         (moddb-add-module1 elab-mod moddb)))

Theorem: moddb-add-module1-elab-mod$a-equiv-congruence-on-elab-mod

(defthm moddb-add-module1-elab-mod$a-equiv-congruence-on-elab-mod
  (implies (elab-mod$a-equiv elab-mod elab-mod-equiv)
           (equal (moddb-add-module1 elab-mod moddb)
                  (moddb-add-module1 elab-mod-equiv moddb)))
  :rule-classes :congruence)

Theorem: moddb-add-module1-of-moddb-fix-moddb

(defthm moddb-add-module1-of-moddb-fix-moddb
  (equal (moddb-add-module1 elab-mod (moddb-fix moddb))
         (moddb-add-module1 elab-mod moddb)))

Theorem: moddb-add-module1-moddb-equiv-congruence-on-moddb

(defthm moddb-add-module1-moddb-equiv-congruence-on-moddb
  (implies (moddb-equiv moddb moddb-equiv)
           (equal (moddb-add-module1 elab-mod moddb)
                  (moddb-add-module1 elab-mod moddb-equiv)))
  :rule-classes :congruence)

Theorem: mv-nth-of-moddb-norm-moddb-under-moddb-norm-equiv

(defthm acl2::mv-nth-of-moddb-norm-moddb-under-moddb-norm-equiv
  (moddb-norm-equiv
       (mv-nth 1
               (moddb-add-module1 elab-mod (moddb-norm moddb)))
       (mv-nth 1 (moddb-add-module1 elab-mod moddb))))

Theorem: mv-nth-moddb-norm-equiv-congruence-on-moddb-under-moddb-norm-equiv

(defthm
 acl2::mv-nth-moddb-norm-equiv-congruence-on-moddb-under-moddb-norm-equiv
 (implies
      (moddb-norm-equiv moddb acl2::moddb-equiv)
      (moddb-norm-equiv
           (mv-nth 1 (moddb-add-module1 elab-mod moddb))
           (mv-nth 1
                   (moddb-add-module1 elab-mod acl2::moddb-equiv))))
 :rule-classes :congruence)

Theorem: take-of-n+1-update-nth

(defthm take-of-n+1-update-nth
  (equal (take (+ 1 (nfix n)) (update-nth n v x))
         (append (take n x) (list v))))

Theorem: moddb-add-module1-under-moddb-norm-equiv

(defthm moddb-add-module1-under-moddb-norm-equiv
 (moddb-norm-equiv (mv-nth 1 (moddb-add-module1 elab-mod moddb))
                   (if (moddb-modname-get-index (g :name elab-mod)
                                                moddb)
                       moddb
                     (list (+ 1 (nfix (nth *moddb->nmods* moddb)))
                           (append (take (nth *moddb->nmods* moddb)
                                         (nth *moddb->modsi* moddb))
                                   (list elab-mod))))))

Theorem: moddb-basics-ok-of-moddb-add-module1

(defthm moddb-basics-ok-of-moddb-add-module1
 (implies
   (and (moddb-basics-ok moddb)
        (< (nfix (moddb->nmods moddb))
           (moddb->mods-length moddb)))
   (moddb-basics-ok (mv-nth 1 (moddb-add-module1 elab-mod moddb)))))

Theorem: moddb-mod-inst-wireoffset-of-update-nmods

(defthm moddb-mod-inst-wireoffset-of-update-nmods
  (implies (and (< (nfix modidx)
                   (nfix (nth *moddb->nmods* moddb)))
                (<= (nfix (nth *moddb->nmods* moddb))
                    (nfix newnmods)))
           (equal (moddb-mod-inst-wireoffset
                       inst modidx
                       (update-nth *moddb->nmods* newnmods moddb))
                  (moddb-mod-inst-wireoffset inst modidx moddb))))

Theorem: moddb-mod-inst-wireoffset-of-update-mod

(defthm moddb-mod-inst-wireoffset-of-update-mod
  (implies (< (nfix modidx) (nfix updidx))
           (equal (moddb-mod-inst-wireoffset
                       inst modidx
                       (update-nth *moddb->modsi*
                                   (update-nth updidx newmod mods)
                                   moddb))
                  (moddb-mod-inst-wireoffset
                       inst modidx
                       (update-nth *moddb->modsi* mods moddb)))))

Theorem: moddb-mod-inst-wireoffset-of-update-table

(defthm moddb-mod-inst-wireoffset-of-update-table
  (equal (moddb-mod-inst-wireoffset
              inst modidx
              (update-nth *moddb->modname-idxes-get* tab moddb))
         (moddb-mod-inst-wireoffset inst modidx moddb)))

Theorem: moddb-mod-inst-instoffset-of-update-nmods

(defthm moddb-mod-inst-instoffset-of-update-nmods
  (implies (and (< (nfix modidx)
                   (nfix (nth *moddb->nmods* moddb)))
                (<= (nfix (nth *moddb->nmods* moddb))
                    (nfix newnmods)))
           (equal (moddb-mod-inst-instoffset
                       inst modidx
                       (update-nth *moddb->nmods* newnmods moddb))
                  (moddb-mod-inst-instoffset inst modidx moddb))))

Theorem: moddb-mod-inst-instoffset-of-update-mod

(defthm moddb-mod-inst-instoffset-of-update-mod
  (implies (< (nfix modidx) (nfix updidx))
           (equal (moddb-mod-inst-instoffset
                       inst modidx
                       (update-nth *moddb->modsi*
                                   (update-nth updidx newmod mods)
                                   moddb))
                  (moddb-mod-inst-instoffset
                       inst modidx
                       (update-nth *moddb->modsi* mods moddb)))))

Theorem: moddb-mod-inst-instoffset-of-update-table

(defthm moddb-mod-inst-instoffset-of-update-table
  (equal (moddb-mod-inst-instoffset
              inst modidx
              (update-nth *moddb->modname-idxes-get* tab moddb))
         (moddb-mod-inst-instoffset inst modidx moddb)))

Theorem: moddb-mods-ok-of-moddb-add-module1-empty

(defthm moddb-mods-ok-of-moddb-add-module1-empty
 (implies
     (and (moddb-mods-ok moddb)
          (equal 0 (elab-mod$a-ninsts elab-mod))
          (equal (elab-mod$a-nwires elab-mod)
                 (nfix (g :totalwires elab-mod)))
          (zp (g :totalinsts elab-mod)))
     (moddb-mods-ok (mv-nth 1 (moddb-add-module1 elab-mod moddb)))))

Theorem: elab-mods->names-of-append

(defthm elab-mods->names-of-append
  (equal (elab-mods->names (append a b))
         (append (elab-mods->names a)
                 (elab-mods->names b))))

Theorem: index-of-append

(defthm index-of-append
  (equal (index-of k (append a b))
         (or (index-of k a)
             (let ((bind (index-of k b)))
               (and bind (+ (len a) bind))))))

Theorem: index-of-cons

(defthm index-of-cons
  (equal (index-of k (cons a b))
         (if (equal k a)
             0
           (let ((bind (index-of k b)))
             (and bind (+ 1 bind))))))

Theorem: moddb-modname-get-index-of-moddb-add-module1

(defthm moddb-modname-get-index-of-moddb-add-module1
  (equal (moddb-modname-get-index
              name
              (mv-nth 1 (moddb-add-module1 elab-mod moddb)))
         (or (moddb-modname-get-index name moddb)
             (and (equal (modname-fix name)
                         (modname-fix (g :name elab-mod)))
                  (nfix (nth *moddb->nmods* moddb))))))

Theorem: nmods-of-moddb-add-module1

(defthm nmods-of-moddb-add-module1
 (implies (not (moddb-modname-get-index (g :name elab-mod)
                                        moddb))
          (equal (nth *moddb->nmods*
                      (mv-nth 1 (moddb-add-module1 elab-mod moddb)))
                 (+ 1 (nfix (moddb->nmods moddb))))))