		Search-engine friendly clone of the ACL2 documentation.

Moddb

Moddb.lisp

Subtopics

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: Push an instantiation onto a modscope, given by the instance index within the current module.
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: A module context within a moddb.
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: Given some modscope, pop out n frames.
Moddb-basics-ok
Svex->absindexed-memo-ok
Svex-named->indexed-memo-ok
Svarlist-idxaddr-okp: (svarlist-idxaddr-okp x bound) recognizes lists where every element satisfies svar-idxaddr-okp.
Elab-modlist-normp
Wirelist-remove-name
Modscope->top: Given some modscope, pop all the way out to the top level.
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: Flatten an SV module into a list of assignments and aliases.
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: A list of path-p objects.
Module->db: Copy the wire hierarchy of an SV module into a moddb.
Elab-modlist: A list of elab-mod$ap objects.
Elab-modinst-list: A list of elab-modinst$cp objects.
Nrec-list-mods
Moddb->nmods
Nrec-list
Nrec