Name-database
A general utility for generating fresh names.
A name database allows you to easily and efficiently
generate good, fresh names that are not being used elsewhere.
Name databases are a general-purpose mechanism that has nothing to do with
Verilog. This was not always true; historically name databases were originally
part of a larger vl-namefactory structure that had a deep understanding of
Verilog modules, but that mechanism no longer exists.
Using Name Databases
Typically, the user begins by constructing a name database using
(vl-starting-namedb names), where names are just a list of the
names (strings) that are "in use."
Once constructed, name databases must be used in a single-threaded
discipline. That is, the functions for generating names actually return (mv
fresh-name db-prime), and to ensure that a sequence of generated names are
unique, one must always use the most recently returned database to generate
subsequent names.
Two functions are provided for generating names:
(vl-namedb-indexed-name prefix db) produces a name that looks like
prefix_n, where n is the smallest positive natural number n such
that the name prefix_n is not in use.
(vl-namedb-plain-name name db) attempts to return name verbatim.
When this is not possible, a name of the form name_n, a note will be
printed to standard output and instead we will produce a name with
vl-namedb-indexed-name.
We use these functions for different purposes. We think that vl-namedb-indexed-name should be used for "throwaway" names that don't need
to be reliable or understandable, such as the names of temporary wires to be
generated for split-up expressions. Meanwhile, vl-namedb-plain-name
should be used for splitting up instance names or in any other cases where a
reliable name is desired.
Because name databases make use of fast alists, they should be destroyed
with (vl-free-namedb nf) when you are done using them.
Freshness Guarantee
To establish that name databases generate only fresh names, we introduce the
function (vl-namedb-allnames db). This function returns a list of all
names that the name database currently considers to be in use. We prove:
- Every name in names is among the allnames of the initial name
database produced by (vl-starting-namedb names).
- The fresh-names returned by vl-namedb-indexed-name or vl-namedb-plain-name are not members of the allnames of the input
database.
- The allnames of the resulting db-prime include exactly the
allnames of the input db, along with the generated
fresh-name.
Together, these theorems ensure that, when properly used, the name database
will only give you fresh names.
Subtopics
- Vl-namedb
- Name database structure.
- Vl-namedb-plain-name
- Safely try to generate a particular name.
- Vl-namedb-pset-fix
- Vl-namedb-plain-names
- Generate a list of fresh names.
- Vl-namedb-indexed-name
- (vl-namedb-indexed-name prefix db) constructs a fresh name that looks
like prefix_n for some natural number n.
- Vl-namedb-pmap-fix
- Vl-unlike-any-prefix-p
- (vl-unlike-any-prefix-p name prefixes) determines whether for all p in
prefixes, (vl-pgenstr-p p name) is false.
- Vl-namedb-pmap-okp
- Vl-namedb-allnames
- (vl-namedb-p x) returns a list of all names that are
considered to be used by the name db.
- Vl-starting-namedb
- (vl-starting-namedb names) creates a name database that regards
names as already in use.
- Vl-pgenstr-highest
- (vl-pgenstr-highest prefix names) returns the largest n such that
"prefix_n" occurs in names.
- Vl-namedb-pset-okp
- Vl-pgenstr-p
- (vl-pgenstr-p prefix str) recognizes strings of the form
"prefix_n".
- Vl-pgenstr->val
- (vl-pgenstr->val prefix str) retrieves n from the string str,
which must have the form "prefix_n"; we return n as a natural
number.
- Vl-free-namedb
- (vl-free-namedb db) frees the fast alists associated with a name
db and returns nil.
- Vl-namedb-plain-name-quiet
- Same as vl-namedb-plain-name, but doesn't print messages when
names aren't available.
- Vl-pgenstr-highest-of-alist-keys
- Fusion of vl-pgenstr-highest and alist-keys, for efficiency.
- Vl-pgenstr
- (vl-pgenstr prefix n) creates the string "prefix_n".
- Vl-empty-namedb
- (vl-empty-namedb) creates an empty name db.
- Vl-namedb-nameset
- An alist mapping stringp to true-p.
- Vl-unlike-any-prefix-p-of-alist-keys
- Vl-namedb-prefixmap
- An alist mapping stringp to natp.
