|
|
|---|
|
|
|
|---|
The process of computing a canonical form for each wire in the module hierarchy.
Alias normalization takes as input a list of pairs of lhs objects and computes a canonical form for each wire mentioned. The inputs must be in indexed-variable form; that is, each variable name must be a unique natural number (this allows us to use arrays to look up variable properties).
The normalization algorithm is similar to a disjoint sets union-find algorithm. Initially, every wire is mapped to itself. For each alias pair, we canonicalize the two LHS objects according to our current mapping. That is, for each wire range in the LHS, we look up the current mapping of the wire, truncate it to the relevant range, and recursively canonicalize that, stopping on ranges that are mapped to themselves. (In order that this process terminates, it is an invariant that every subrange of every wire is mapped to a range of a wire whose index is less than or equal to the index of that wire; and if mapped to itself, then to either a lower range of bits or just to itself.)
Then, when we have normalized the two LHSes, we break this pairing down into
pairs of single wire ranges. For example, if our two normalized LHSes are
(a[5:4], c[8:7]), (b[7:6], c[6:5]), (b[5:3], d[9:7]).
For each of these range pairs, unless the two elements are the same, we set the canonical version of one to the other, chosen so that the ordering invariant is maintained.
To finish processing the current alias pair, we again recursively canonicalize the original pair of LHS objects. However, now, whenever we find the canonical version of a wire range, we replace the mapping for that wire range with the canonical version found. As in the union-find algorithm, this is a performance optimization to minimize the number of steps necessary in future searches.
Once all alias pairs are processed like this, we finish by doing a linear sweep over all entries in the table, replacing every wire range by its canonical representation.
We haven't proved the algorithm correct. Here are some thoughts on the topic.
The correctness statement is something like the following.
If v and w are each a bit selected from some wire, then
During the main loop of the algorithm (i.e. between processing alias pairs),
this property holds of the alias pairs processed so far, if we regard
Base case: we haven't processed any alias pairs yet; by the initial setting
of the mapping,
Inductive case: Suppose the property holds before adding an alias pair, and show it holds after adding it.
Backward direction: Show that if a path exists from v to w, then the canonical forms are equal.
Lemma: If
So if the path exists without our new alias pair, then by I.H. the canonical forms are equal before, so they are equal after as well. So we only need to consider the case where the path uses our new alias pair. Basically, it suffices to show that as we process the alias pair, we equalize the canonical forms of corresponding bits. So since each link in the path is corresponding bits of a pair, they have equal canonical representations.
Forward direction: If there is no path, then the canonical forms differ. To prove this, we assume the canonical forms are the same and produce a path. We only need to consider v, w whose canonical forms are newly equal: if they were equal before then there was a path before by IH, and that same path works now. The only operation that equalizes new pairs is that we set a canonical range to the corresponding canonical range of the other LHS.
Lemma: Setting a canonical range to another range only affects the canonical form of bits whose canonical form was in that range.
Bits whose canonical form was in the changed range (by IH) have a path to corresponding bits of that range. The part of the original LHS that mapped to that range also has such a path. Concatenate these two, step over the current alias to some bit whose canonical form already was the new canonical form in question -- so then concatenate on that bit's path to w. Got that?