A Semi-Canonical form for Sequential AIGs

In numerous EDA flows, time-consuming computations are repeatedly applied to sequential circuits. This motivates developing methods to determine what circuits have been processed already by a tool. This paper proposes an algorithm for semi-canonical labeling of nodes in a sequential AIG, allowing problems or sub-problems solved by an EDA tool to be cached with their computed results. This can speed up the tool when applied to designs with isomorphic components or design suites exhibiting substantial structural similarity.

Proposed Method for Semi-Canonical Labeling of Sequential AIGs

In sequential and-inverter-graphs (AIGs) there frequently exist many instances of the same logic sub-circuit but with different inputs. Many synthesis and verification packages spend significant time analyzing logic, and the presence of identical sub-circuits results in duplication of effort. Alternatively, if a synthesis or verification package is invoked on a design and then again on a minimally changed version of the same design, many of the logic sub-circuits remain unchanged between runs. Time spent re-analyzing these sub-circuits results in a duplication of effort. The method proposed in this paper for semi-canonical labeling of sequential AIGs, detects the majority of isomorphic sub-circuits. Intermediate results computed on these sub-circuits can be cached and applied across every instance of the sub-circuit, leading to dramatic improvements in runtimes of synthesis or verification.

A sequential AIG represents a sequential circuit as a directed labeled graph consisting of two-input AND nodes, primary inputs, primary outputs, and flip-flop nodes. The edges are labeled with 1 denoting inversion or 0 otherwise. Labeling of nodes and AND gate fanins can be arbitrary. The idea of the method is to use this freedom, to re-label the nodes based on their transitive fanin and fanout graph structures, and thereby create a semi-canonical form for the given sequential AIG. Thus a new labeling is derived and each node's fanins are listed in numerical order of their labels. We want the semi-canonical structure to be as precise as reasonably possible. For example, given two isomorphic AIGs, we want their newly labeled representations to be identical. If this always happens, the labeling is canonical. While it is not efficient to make relabeling exactly precise in this sense, we want it to be highly precise in that it rarely fails to identify two isomorphic AIGs. We call this labeling semi-canonical.

Three applications of this idea are as follows.

1. It can detect structurally isomorphic primary outputs (POs) of a multi-output sequential AIG. This is done by taking each output＊s cone and mapping it into its semi-canonical form. If the forms of the two outputs, are identical, then the outputs are isomorphic.
2. In verification, where each output represents a property to be proved, if two outputs are isomorphic then it is only necessary to solve one. If an inductive invariant (or a counter-example) is computed to witness a proof (or a failure) of one property, it can be readily remapped to be a witness for the other. Thus when verifying a set of outputs, only one representative of each isomorphic class need be considered, reducing the number of proof obligations.
3. It can be used to cache synthesis or verification results that have been computed previously on an AIG. When an AIG is to be processed, it is cast into its semi-canonical form and stored in a cache along with the computed result. Given a new AIG, we compute its semi-canonical form and check if it is cached. If already cached, we return the saved result. Otherwise, we solve the problem and cache the semi-canonical form and the result.

The method finds a re-labeling of the node IDs using the AIG structure. This is done by computing signatures for each node, based the node's transitive fanin cone in the sequential AIG. Unique labels are assigned to a node that has a unique signature. For nodes with non-unique signatures, "tie-breaking" is done by assigning one such node an unused label and then node signatures are updated based on this. The key for this semi-canonicalization is a) to define the signature of a node in such a way that it is very precise, and b) to compute and update signatures efficiently.

To summarize, the contributions of this paper are:

• An algorithm for structural semi-canonical labeling for sequential AIGs is given. The method of re-labeling can be adapted easily to other forms of graphs.
• Analysis of public and industrial benchmarks confirms that a) re-labeling can be computed efficiently, and b) many benchmarks contain a large number of isomorphic primary output cones.