		Search-engine friendly clone of the ACL2 documentation.

Mlib

Vl-namefactory

Produces fresh names for a module.

This is a product type introduced by defprod.

Fields

mod — vl-maybe-module
namedb — vl-namedb

Additional Requirements

The following invariant is enforced on the fields:

(vl-namefactory-namedb-okp mod namedb)

A name factory allows you to easily and efficiently generate good, fresh names that are not being used elsewhere in a Verilog module. They combine a name database (which is a general mechanism for generating fresh names; see vl-namedb-p for details) with a Verilog module in order to avoid computing the module's namespace until a name is actually needed. This optimization often saves a lot of consing.

Using Name Factories

Typically, given some module mod, the user begins by constructing a name factory using (vl-starting-namefactory mod). Note that it is quite cheap to construct a name factory in this way; all expense is delayed until the first use of the factory. It is also possible to create a name factory without a module using vl-empty-namefactory, which is occasionally useful when generating new modules.

Once constructed, name factories must be used in a single-threaded discipline. That is, the functions for generating names actually return (mv fresh-name factory-prime), and to ensure that a sequence of generated names are unique, one must always use the most recently returned factory to generate subsequent names.

Two functions are provided for generating names:

(vl-namefactory-indexed-name prefix nf) 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-namefactory-plain-name name nf) 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-namefactory-indexed-name.

We use these functions for different purposes. We think that vl-namefactory-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-namefactory-plain-name should be used for splitting up instance names or in any other cases where a reliable name is desired.

Because name factories make use of fast alists, they should be destroyed with (vl-free-namefactory nf) when you are done using them.

Freshness Guarantee

To establish that name factories generate only fresh names, we introduce the function (vl-namefactory-allnames nf). This function returns a list of all names that the name factory currently considers to be in use. We prove:

The allnames of the empty name factory is empty.
Every name in the vl-module->modnamespace of mod is among the allnames of the initial name factory produced by (vl-starting-namefactory mod).
The fresh-names returned by vl-namefactory-indexed-name or vl-namefactory-plain-name are not members of the allnames of the input factory.
The allnames of the resulting factory-prime include exactly the allnames of the input factory, along with the generated fresh-name.

Together, these theorems ensure that, when properly used, the name factory will only give you fresh names.

Motivation and History

Name generation is a surprisingly important and difficult problem. It needs to be very efficient: we have sometimes found that tens of thousands of fresh names are needed, e.g., in split. Toward this goal, our original approach was as follows:

Our generated names always looked like _gen_1, _gen_2, etc.
When the first name was needed, a transform would examine the module's namespace for the largest n such that _gen_n was already in use. The name _gen_{n+1} would then be used as the first new name.
Subsequently, any number of fresh names could then be generated by simply increasing the index. That is, the second name fresh name would be _gen_{n+2}, the third _gen_{n+3}, and so on.

This scheme was highly efficient because the module's namespace only needed to be consulted when generating the first wire's name. This meant that for large modules, generating thousands of names was not very expensive. It also meant that if no fresh names were needed, then the module's namespace was never even computed.

But a problem with this scheme is that the generated names are not very good or predictable. This was particularly problematic when instance arrays like:

basic_flop data [(width - 1):0] (q, ph1, d);

would be transformed into something like:

basic_flop _gen_19 (q[0], ph1, d[0]);
basic_flop _gen_18 (q[1], ph1, d[1]);
basic_flop _gen_17 (q[2], ph1, d[2]);

that is, here the instance name data has been entirely lost and replaced with a bunch of unrelated, stupid names that might easily change when the module is translated in the future.

Name factories basically extend this scheme to allow much better names to be generated, while still being quite efficient.

Implementation

A name factory has two fields:

mod, the module that we are generating names for, or nil if there is no such module (e.g., for empty name factories).
namedb is an ordinary vl-namedb-p that we use to generate fresh names.

The invariant we maintain is that either the namedb is empty, or every name in the vl-module->modnamespace of mod must be bound in it.

Subtopics

Vl-namefactory-p: Recognizer for vl-namefactory structures.
Vl-namefactory-fix: Fixing function for vl-namefactory structures.
Vl-namefactory-equiv: Basic equivalence relation for vl-namefactory structures.
Make-vl-namefactory: Basic constructor macro for vl-namefactory structures.
Vl-namefactory->namedb: Get the namedb field from a vl-namefactory.
Vl-namefactory->mod: Get the mod field from a vl-namefactory.
Change-vl-namefactory: Modifying constructor for vl-namefactory structures.