Once a design is both retimed and sequentially optimized, sequential equivalence verification becomes very hard since retiming breaks the equivalence of the retimed sub-blocks although the design equivalence is preserved.

Circuits can be simplified for combinational equivalence checking by transforming internal functions, while preserving their ranges. In this paper, we investigate how to effectively apply the idea to improve equivalence checking. We propose new heuristics to identify groups of nets in a cut, and elaborate detailed aspects of the new equivalence checking method. With a given miter, we identify a group of nets in a cut and transform the function of each net into a more compact representation with less variables. These new compact parametric representations preserve the range of nets as well as of the cut. This transformation significantly reduces the size of intermediate BDDs and enables the verification to be conclusive for many designs which state-of-the-art equivalence checkers fail to verify. Iterative groupings and transformations are performed until no grouping is possible for a cut. Then we proceed to the next cut and continue until the compare point is reached. Our experimental results show the effectiveness of our strategy and new grouping heuristics on the new method.

Image computation is the key step in fixpoint computations that are extensively used in model checking. Two techniques have been used for this step: one based on conjunction of the terms of the transition relation, and the other based on recursive case splitting. We discuss when one technique outperforms the other, and consequently formulate a hybrid approach to image computation. Experimental results show that the hybrid algorithm is much more robust than the “pure” algorithms and outperforms both of them in most cases. Our findings also shed light on the remark of several researchers that splitting is especially effective in approximate reachability analysis.

A paradigm for automatic approximation/refinement in conservative CTL model checking is presented. The approximations are used to verify a given formula conservatively by computing upper and lower bounds to the set of satisfying states at each sub-formula. These approximations attempt to perform conservative verification with the least possible number of BDD variables and BDD nodes. We present new forms of operational graphs to avoid limitations associated with previously used operational graphs. Three new techniques for efficient automatic refinement of approximate system are presented. These methods make it easier to find the locality. We also present a new type of don't cares (approximate satisfying don't cares) that can make model checking more efficient in time and space. On average, an order of magnitude speedup was achieved.

The knowledge of the reachable states of a sequential circuit can dramatically speed up optimization and model checking. However, since exact reachability analysis may be intractable, approximate techniques are often preferable. H. Cho et al. (1996) presented the machine-by-machine (MBM) and frame-by-frame (FBF) methods to perform approximate finite state machine (FSM) traversal. FBF produces tighter upper bounds than MBM; however, it usually takes much more time and it may have convergence problems. In this paper, we show that there exists a class of methods-least fixpoint approximations-that compute the same results as RFBF ("reached FBF", one of the FBF methods). We show that one member of this class, which we call "least fixpoint MBM" (LMBM), is as efficient as MBM, but provably more accurate. Therefore, the trade-off that existed between MBM and RFBF has been eliminated. LMBM can compute RFBF-quality approximations for all the large ISCAS-89 benchmark circuits in a total of less than 9000 seconds.

RDCs (Reachability Don’t Cares) can have a dramatic impact on the cost of CTL model checking [18]. Unfortunately, RDCs, being a global property, are often much more difficult to compute than the satisfying set of typical CTL formulas. We address this problem through the use of Approximate Reachability Don’t Cares (ARDCs), computed with the algorithms developed for the VERITAS sequential synthesis package [4, 5]. Approximate Reachable states represent an upper bound on the set of true reachable states, and thus a lower bound on the set of unreachable (Don’t Care) states. ARDCs can be 10X to 100X (or much more for very large circuits) cheaper to compute than RDCs, and in some cases have the same dramatic effect on CTL model checking as the real RDCs. We also discuss the application of ARDCs to the problem of exact computation of the RDCs themselves. Experiments on industrial benchmarks show that order of magnitude speedups are possible, and occur frequently. The experimental results presented strongly support our claim that ARDCs play a safe and important way out of a serious dilemma: RDCs are necessary for tractable model checking of many large circuits, but the computation of the RDCs themselves is often intractable. We include, and theoretically justify, significant extensions of the VERITAS algorithms, and show that they can be up to an order of magnitude faster, while computing a virtually identical upper bound. 1

We present an algorithm that restructures the state transition graph (STG) of a sequential circuit so as to reduce power dissipation.The STG is modified without changing the behavior of the circuit, by exploiting state equivalence.Bather than aiming primarily at reducing the number of states, our algorithm redirects transitions so that the new destination states are equivalent to the original ones, while the average activity of the circuit is decreased.The impact on area is also estimated to increase the accuracy of the power analysis.The STG and all other major data structures are stored as decision diagrams, and the algorithm does not enumerate explicitly the states or the transitions.(i.e., it is symbolic.)Therefore, it can deal with circuits that have millions of states.Once the STG has been restructured we apply symbolic factoring algorithms, based on Zero-suppressed BDDs, to convert the optimized graph into a multilevel circuit.We derive an efficient circuit from the BDDs of the STG by incorporating power constraints in the symbolic factoring algorithms.