Reparameterization, also known as range preserving logic synthesis, replaces a logic cone by another logic cone, which has fewer inputs while producing the same output combinations as the original cone. It is expected that a smaller circuit leads to a shorter verification time. This paper describes an approach to reparameterization, which is faster but not as general as the previous work. The new procedure is particularly well-suited for circuits derived by localization abstraction.
The use of reparameterization as a circuit transformation in the verification flow was pioneered by Baumgartner et. al. in [1]. In their work, new positions for the primary inputs (PIs) are determined by finding a minimum cut between the current PI positions and the next-state variables (flop inputs). BDDs are then used to compute the range (or image) on the cut. Finally, a new logic cone with the same range (but fewer PIs), is synthesized from the BDDs and grafted onto the original design in place of the current logic cone. This is a very powerful transformation, but it has potential drawbacks: (i) the BDDs may blow up and exhaust the memory, (ii) the extracted circuit may be larger than the logic it replaces, and (iii) the runtime overhead may be too high.
In contrast, the proposed approach is based on greedy local transformations, capturing only a subset of optimization opportunities. However, memory consumption is modest, runtimes are very low, and the resulting design is always smaller, or of the same size, as the original design. It is shown experimentally that the proposed method leads to sizeble reductions when applied for circuits produced by localization abstraction [5]. The fast reparameterization algorithm is based on the following observation: if a node dominates1 a set of PIs, and those PIs are sufficient to force both a zero and a one at that node, regardless of the values given to the other PIs and state variables, then that node can be replaced by a new primary input, while the unused logic cone driving 1A node n dominates another node m iff every path from m to a primary output goes through node n. the original node can be removed. The old primary inputs dominated by the given node are also removed by this procedure.
Example. Suppose a design contains inputs x1, x2, and a gate Xor(x1, x2); and that furthermore, x1 has no other fanouts besides this Xor-gate. Then, no matter which value x2 takes, both a zero and a one can be forced at the output of the Xor by setting x1 appropriately, and thus the Xor-gate can, for verification purposes, be replaced by a primary input.
The proposed method to find similar situations starts by computing all dominators of the netlist graph, then for each candidate node dominating at least one PI the following quantification problem is solved: “for each assignment to the non-dominated gates, does there exist a pair of assignments to the dominated PIs that results in a zero and a one at the candidate node”. More formally, assuming that x represents non-dominated gates (“external inputs”) and yi represents dominated PIs (“internal inputs”), the following is always true for the node’s function φ:
∀x ∃y0, y1 . ¬φ(x, y0) ∧ φ(x, y1) Important features of this approach are: (i) It is circuit based, while early work on reparameterization was based on transition relations [4]. (ii) In its simplest form, the proposed restructuring replaces some internal nodes by new primary inputs and remove dangling logic. (iii) The analysis is completely combinational: no information on the reachable state-space is used. (iv) If the property was disproved after reparametrization, it is straight-forward to remap the resulting counterexample to depend on the original primary inputs. It is important to realize that by analyzing and applying reductions in topological order from PIs to POs, regions amenable to reparameterization are gradually reduced to contain fewer gates and PIs. By this process, the result of repeatedly applying local transformations can lead to a substantial global reduction. In the current implementation, the above formula is evaluated by exhaustive simulation of the logic cone rooted in the given node while the cone is limited to 8 inputs. Limiting the scope to cones with 8 inputs and simulating 256 bit patterns (or eight 32-bit words) seems to be enough to saturate the reduction achievable on the benchmarks where the method is applicable.
Some typical reductions are shown in Figure 1. The graphs should be understood as sub-circuits of a netlist being reparameterized. The exclamation marks denote “internal” PIs dominated by the top-node, and hence under our control; and the question marks denote gates with fanouts outside the displayed logic cone, for which no assumption on their values can be made. The full algorithm is described in Figure 2.
Counterexample reconstruction. There are several ways that a trace on the reduced netlist can be lifted to the original netlist. For instance, the removed logic between the new PIs and the old PIs can be stored in a separate netlist. The trace on the reduced netlist can then be pro− Compute dominators. For a DAG with bounded in-degree (such as an And-Inverter-Graph), this is a linear operation in the number of nodes (see Figure 3). − For each PI, add all its dominators to the set of “candidates”. − For each candidate c, in topological order from inputs to outputs: - Compute the set D of nodes dominated by c (Figure 4). - Denote the PIs in D “internal” inputs. - Denote any node outside D, but being a direct fanin of a node inside D, an “external” input (may be any gate type). - Simulate all possible assignments to the internal and external inputs. If for all external assignments there exists an internal assignment that gives a 0 at c, and another internal assignment that gives a 1 at c, then substitute c by a new primary input. Compute Dominators − Initialize all POs to dominate themselves − Traverse the netlist in reverse topological order (from POs to PIs), and mark the children of each node as being dominated by the same dominator as yourself unless the child has already been assigned a dominator − For already marked children, compute the “meet” of the two dominators, i.e. find the first common dominator. If there is no common dominator, mark the node as dominating itself.
Compute Dominated Area area = {w dom} count = [0, 0, . . ., 0] for w ∈ area: for v ∈ faninsOf (w ): count[v ]++ if count[v ] == num of fanouts[v ]: area = area ∪ {v } – init. set of gates to the dominator – count is a map “gate → integer” jected onto the original PIs by rerunning the simulation used to produce the reparameterized circuit, and for each candidate pick an assignment that gives the correct value. But even simpler, one can just put the original netlist into a SAT solver and assert the values from the trace onto the appropriate variables and call the SAT solver to complete the assignment. In practice, this seems to always work well. 3
The algorithm described in the previous section replaces internal nodes with inputs, and thus only removes logic. If we are prepared to forgo this admittedly nice property and occasionally add a bit of new logic, then nodes that are not completely controllable by their dominated inputs can still be reparameterized by the following method: for node with function φ(x, y), where x are external inputs and y are internal inputs, compute the following two functions: φ0(x) ≡ ∀y.¬φ(x, y) φ1(x) ≡ ∀y. φ(x, y) Using these two functions, φ can be resynthesized using a single input ynew by the expression:
¬φ0(x) ∧ (φ1(x) ∨ ynew) In other words, if two or more inputs are dominated by the node φ, a reduction in the number of inputs is guaranteed. Depending on the shape of the original logic, and how well new logic for φ0 and φ1 is synthesized, the number of logic gates may either increase or decrease. In our implementation, logic for φ0 and φ1 is created by the fast irredundant sum-of-product (“isop”) proposed by Shin-ichi Minato in [10]. We greedily apply this extended method for all nodes with two or more dominated PIs, even if it leads to a blow-up in logic size. To counter such cases, fast logic synthesis can be applied after the reparameterization. Obviously, there are many ways to refine this scheme. 4
Another possible improvement to the method is extending the reparameterization algorithm to work for multi-output cones. As an example, consider a two-output cone where the outputs can be forced to all four combinations {00, 01, 10, 11} by choosing appropriate values for dominated inputs. In such a case, the cone can be replaced by two free inputs. If some of the four combinations at the outputs are impossible under conditions expressed in terms of non-controllable signals, a logic cone can be constructed to characterize these conditions and reduce the number of PIs by adding logic similar to the case of a single-output cone. 5
As part of the experimental evaluation, all benchmarks from the single-property track of the Hardware Modelchecking Competition 2012 were considered. Localization abstraction [5] was applied with a timeout of one hour to each benchmark and the resulting models meeting the following criteria were kept: – At least half of the flops were removed by abstraction. – The abstraction was accurate (no spurious counterexamples). – At least one of the verification engines could prove the property within one hour.
The sizes of benchmarks selected in this way are listed in table Table 1. All those models were given to the reparameterization engine, both in weak mode and strong mode, the latter using the improvements described in section 3. The reparameterized models were also post-processed with a quick simplification method called “shrink” which is part of the ABC package [7]. The longest runtime for weak reparameterization was 16 ms, for strong reparameterization 28 ms and for the simplification phase 50 ms.2 Reductions are listed in table Table 2.
For comparison, Table 2 also include the results of running an industrial implementation of the BDD based algorithm of [1]. Because runtimes are significantly longer with this algorithm, they are given their own column. These results were given to us from IBM, and according to their statement “are not tweaked as much as they could be”.
All benchmarks were given to three engines: Property Directed Reachability [2, 6], BDD-based reachability [3], and Interpolation-based Model Checking [9]. The complete table of results is given in Table 3. A slice of this table, showing only results for PDR, with and without (strong) reparameterization, is given in Table 4 together with a scatter plot. Analysis. Firstly, we see a speedup of 100x-1000x over previous work in the runtime of the reparameterization algorithm itself, with comparable quality of results for the application under consideration (models resulting from localization abstraction). This means the algorithm can always be applied without the need for careful orchestration. Secondly, we see an average speedup of 2.5x in verification times when applying reparameterization in conjunction with PDR, which is also the best overall engine on these examples. For two benchmarks, 6s121 and 6s150, BDD reachability do substantially better than PDR, and for the latter (where runtimes are meaningful) the speedup due to reparameterization is greater than 3x. Furthermore, for BDD reachability one can see that on several occasions (6s30 in particular), reparameterization is completely crucial for performance. Finally, interpolation based modelchecking (IMC) seems to be largely unaffected by reparameterization.
2Benchmarks from HWMCC’12 are quite small. For comparison: running reparameterization on a 7 million gate design from one of our industrial collaborators took 4.1 s. ! ! ! Design !! #And 6s102 !! 6,594 6s121 !! 1,636 6s132 !! 1,216 6s144 !! 41,862 6s150 !! 5,448 6s159 !! 1,469 6s164 !! 1,077 6s189 !! 36,851 6s194 !! 12,049 6s30 !! 102,535 6s43 !! 7,408 6s50 !! 16,700 6s51 !! 16,701 bob05 !! 18,043 bob1u05cu !! 32,063
Reparameterization
BDD Reparam.
#PI
Runtime
!! Depth #FF Weak
Weak
0.1 0.1 1000 Products Forms from Binary Decision Diagrams. In Proc. of SASIMI, 1992.