Elab-mod
Part of a moddb representing a single module.
Note: This is partly implementation-level documentation for moddb.
Specifically, none of the updater functions listed here should be used in the
context of operating on a moddb -- rather, a moddb should be built from a modalist using one or more calls of module->db, and treated as
read-only thereafter. It is fine to use the (read-only) accessor
functions.
An elab-mod is an abstract stobj whose logical story is that it is a
record (accessed using g/s -- see ACL2::misc/records)
containing the following fields:
- name -- the name of the module, a modname-p object
- totalwires -- the total number of wires in the module and all its
instances, a natural
- totalinsts -- the total number of instances in the module and all
its instances, a natural
- orig-mod -- the module that this was generated from
- wires -- the list of wires local to the module
- insts -- the list of modinsts local to the module.
The executable accessors/updaters of these (except for wires and insts; see
below) are named, e.g., elab-mod->name/update-elab-mod->name.
The wires and insts fields are special in that they cannot be accessed
directly in execution; in fact, they are not actually lists, but arrays. They
are also backed by hash tables so that wire or instance indices may be looked
up by wire/instance name. (Well-formedness enforced by the abstract stobj
representation makes this mapping invertible.) The following accessors are
used to access information about the wires/instances:
- (elab-mod-nwires elab-mod) -- the number of local wires
- (elab-mod-wiretablei wire-idx elab-mod) -- the nth wire
- (elab-mod-wirename->idx name elab-mod) -- the index for the named
wire
- (elab-mod-add-wire wire elab-mod) -- add a wire to the table
- (elab-mod-ninsts elab-mod) -- the number of local module
instances
- (elab-mod->instname inst-idx elab-mod) -- the instname of the nth
module instance
- (elab-mod->inst-modidx inst-idx elab-mod) -- the index of the module
instantiated by the nth instance
- (elab-mod->inst-wireoffset inst-idx elab-mod) -- the total number of
wires in the module up until this instance -- i.e. the number of local wires
plus the sum of the totalwires of the modules of lower-numbered instances
- (elab-mod->inst-instoffset inst-idx elab-mod) -- the total number of
instances in the module up until this instance -- i.e., inst-idx plus the sum
of the totalinsts of the modules of lower-numbered instances
- (elab-mod-instname->idx name elab-mod) -- the index for the named
instance
- (elab-mod-add-inst elab-modinst$c elab-mod) -- copy an elab-modinst$c
stobj into the elab-mod as a new instance.
All of the above functions execute in constant time, even though several of
their logical definitions are linear in the number of wires/insts.
A wire or instance cannot be removed once added. There isn't even any way
to clear out the wires or instances; just start over with a new elab-mod.
