Moddb
A database object that provides a unique numbering of all the wires in
a module hierarchy.
A moddb is a stobj that provides a fast method of enumerating wires
and a compact, high-performance mapping between these indices and their
names/declarations. It is used in svex-compilation to avoid more memory
hungry methods of mapping hierarchical wire names to values.
A moddb is a nested stobj structure defined as follows:
Definition: moddb
(defstobj moddb
(moddb->nmods1 :type (integer 0 *)
:initially 0)
(moddb->mods :type (array elab-mod (0))
:resizable t)
(moddb->modname-idxes :type (hash-table equal)))
where:
- moddb->nmods contains the number of modules in the database.
- moddb->mods is an array of elab-mod structures, which we
describe below, of which moddb->nmods are valid.
- moddb->modname-idxes is a hash table mapping module names to indices.
Together, moddb->mods and moddb->modname-idxes constitute a
two-way mapping between module names and module indices. It is a requirement
of a well-formed moddb that both of the following hold:
(implies (and (natp i) (< i (moddb->nmods moddb)))
(equal (moddb->modname-idxes-get
(elab-mod->name (moddb->modsi i moddb))
moddb)
i))
(implies (moddb->modname-idxes-get name moddb)
(equal (elab-mod->name
(moddb->modsi
(moddb->modname-idxes-get name moddb)
moddb))
name))
The moddb->mods field is an array of elab-mod stobjs. Thus, a
moddb is a nested stobj -- see ACL2::nested-stobjs. An elab-mod is an
abstract stobj; more detailed documentation of its accessors/updaters is in
elab-mod. Generally speaking, an elab-mod has a name, an array of
wires, and an array of submodule instances, as well as a count of the total
number of wires/instances in itself its instances. For each submodule
instance, it also has a wire offset and an instance offset, which say where
that submodule instance falls in the module-wide ordering of wires and
instances.
Usage
To create a moddb, users should always use module->db to put the
dependencies of some module in a modalist into the database. Any other
updates to a moddb require careful consideration of well-formedness
invariants.
Subtopics
- Moddb.lisp
- Elab-mod
- Part of a moddb representing a single module.
- 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.
- Moddb-wireidx->path/decl
- Convert a wire index to a path relative to the module it's in, and additionally
return the wire declaation.
- Moddb-path->wireidx
- Convert a wire path relative to a module into a wire index.
- Moddb-address->wireidx
- Convert a wire address into a wire index, given the scope from which
the address is relative.
- Moddb-address->wiredecl
- Given a wire address, find the corresponding wire declaration.
- Moddb-wireidx->path
- Convert a wire index to a path relative to the module it's in.
- 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.
