Abstract We study partial quantifier elimination (PQE) for propositional CNF formulas with existential quantifiers. PQE is a generalization of quantifier elimination where one can limit the set of clauses taken out of the scope of quantifiers to a small subset of clauses. The appeal of PQE is that many verification problems (e.g., equivalence checking and model checking) can be solved in terms of PQE and the latter can be dramatically simpler than full quantifier elimination. We show that PQE can be used for property generation that one can view as a generalization of testing. The objective here is to produce anunwantedproperty of a design implementation, thus exposing a bug. We introduce two PQE solvers called $$ EG \text {-} PQE $$ and $$ EG \text {-} PQE ^+$$ . $$ EG \text {-} PQE $$ is a very simple SAT-based algorithm. $$ EG \text {-} PQE ^+$$ is more sophisticated and robust than $$ EG \text {-} PQE $$ . We use these PQE solvers to find an unwanted property (namely, an unwanted invariant) of a buggy FIFO buffer. We also apply them to invariant generation for sequential circuits from a HWMCC benchmark set. Finally, we use these solvers to generate properties of a combinational circuit that mimic symbolic simulation.

We consider the problem of efficiently checking a set of safety properties P1,...,Pkof one design. We introduce a new approach called JA-verification, where JA stands for “JustAssume” (as opposed to “assume-guarantee”). In this approach, when proving a property Pi, one assumes that every property Pjfor j ≠ i holds. The process of proving properties either results in showing that P1,...,Pkhold without any assumptions or finding a “debugging set” of properties. The latter identifies a subset of failed properties that are the first to break. The design behaviors that cause the properties in the debugging set to fail must be fixed first. Importantly, in our approach, there is no need to prove the assumptions used. We describe the theory behind our approach and report experimental results that demonstrate substantial gains in performance, especially in the cases where a small debugging set exists.

We use testing to check if a combinational circuit N always evaluates to 0 (written as N ≡ 0). We call a set of tests proving N ≡ 0 a complete test set (CTS). The conventional point of view is that to prove N ≡ 0 one has to generate a trivial CTS. It consists of all 2|X|input assignments where X is the set of input variables of N. We use the notion of a Stable Set of Assignments (SSA) to show that one can build a non-trivial CTS consisting of less than 2|X|tests. Given an unsatisfiable CNF formula H(W ), an SSA of H is a set of assignments to W that proves unsatisfiability of H. A trivial SSA is the set of all 2|W|assignments to W. Importantly, real-life formulas can have non-trivial SSAs that are much smaller than 2|W|. In general, construction of even non-trivial CTSs is inefficient. We describe a much more efficient approach where tests are extracted from an SSA built for a projection of N on a subset of its variables. These tests can be viewed as an approximation of a CTS for N. We describe potential applications of our approach. We show experimentally that it can be used to facilitate hitting corner cases and expose bugs in sequential circuits overlooked due to checking "misdefined" properties.

We introduce a new framework for Equivalence Checking (EC) of Boolean circuits based on a general technique called Logic Relaxation (LoR). LoR is meant for checking if a propositional formula G has only “good” satisfying assignments specified by a design property. The essence of LoR is to relax G into a formula Grlxand compute a set S that contains all assignments that satisfy Grlxbut do not satisfy G. If all bad satisfying assignments are in S, formula G can have only good ones and the design property in question holds. Set S is built by a procedure called partial quantifier elimination. The appeal of EC by LoR is twofold. First, it facilitates generation of powerful inductive proofs. Second, proving inequiv-alence comes down to checking the existence of some assignments satisfying Grlxi.e. a simpler version of the original formula. We give experimental evidence that supports our approach.

We compare the complexity of "internal" and "external" equivalence checking. The former is meant for proving the correctness of a synthesis transformation by which circuit N2is obtained from circuit N1. The latter is meant for proving that circuits N1and N2are functionally equivalent without making any explicit assumptions about the origin of N1and N2. We describe logic synthesis procedures that can produce a circuit N2whose equivalence with the original circuit N1, most likely, can not be efficiently proved by an external equivalence checker. On the other hand, there are internal equivalence checking procedures that easily prove that N1and N2are equivalent. We give experimental data showing that these logic synthesis procedures are not a mathematical curiosity but indeed can be used as a powerful method of logic optimization.

We describe a procedure (called the TEP procedure) that, given a multi-output circuit M, builds another multi-output circuit M* that is toggle equivalent to M. The TEP procedure can be used in the following two scenarios. First, since for single- output circuits toggle equivalence means functional equivalence, the TEP procedure can be used in "regular" logic synthesis. Second, the TEP procedure enables a powerful synthesis method called LS_TE (Logic Synthesis preserving Toggle Equivalence). Given a circuit N and its partitioning into subcircuits NiLS_TE builds an optimized circuit N* by replacing subcircuits Niwith their toggle equivalent counterparts Ni. The replacement of Niwith N*iis done by the TEP procedure. We give results of optimizing single-output circuits by the TEP procedure and some preliminary results of using the TEP procedure in LS_TE. These results show the promise of the TEP procedure and LS_TE.

In this paper we develop a theory of equivalence checking (EC) and logic synthesis of circuits with a common specification (CS). We show that two combinational circuits N1 N2 have a CS iff they can be partitioned into subcircuits that are connected "in the same way" and are toggle equivalent. This fact allows one to represent a specification of a circuit implicitly as a partitioning into subcircuits. We give an efficient procedure for checking if circuits N1, N2 have the same predefined specification. As a "by-product", this procedure performs EC of N1 and N2. We show how, given a circuit N1 with a predefined specification, one can efficiently build a circuit N2 satisfying the same specification. We give experimental evidence that EC of N1 N2 is hard if their CS is unknown.

We describe a SAT-solver, BerkMin, that inherits such features of GRASP, SATO, and Chaff as clause recording, fast BCP, restarts, and conflict clause "aging". At the same time BerkMin introduces a new decision making procedure and a new method of clause database management. We experimentally compare BerkMin with Chaff, the leader among SAT-solvers used in the EDA domain. Experiments show that our solver is more robust than Chaff. BerkMin solved all the instances we used in experiments including very large CNFs from a microprocessor verification benchmark suite. On the other hand, Chaff was not able to complete some instances even with the timeout limit of 16 hours.

We introduce the notion of problem symmetry in search-based SAT algorithms. We develop a theory of essential points to formally characterize the potential search-space pruning that can be realized by exploiting problem symmetry. We unify several search-pruning techniques used in modern SAT solvers under a single framework, by showing them to be special cases of the general theory of essential points. We also propose a new pruning rule exploiting problem symmetry. Preliminary experimental results validate the efficacy of this rule in providing additional search-space pruning beyond the pruning realized by techniques implemented in leading-edge SAT solvers.

This paper addresses the problem of combinational equivalence checking (CEC) which forms one of the key components of the current verification methodology for digital systems. A number of recently proposed BDD based approaches have met with considerable success in this area. However, the growing gap between the capability of current solvers and the complexity of verification instances necessitates the exploration of alternative, better solutions. This paper revisits the application of Satisfiability (SAT) algorithms to the combinational equivalence checking (CEC) problem. We argue that SAT is a more robust and flexible engine of Boolean reasoning for the CEC application than BDDs, which have traditionally been the method of choice. Preliminary results on a simple framework for SAT based CEC show a speedup of up to two orders of magnitude compared to state-of-the-art SAT based methods for CEC and also demonstrate that even with this simple algorithm and untuned prototype implementation it is only moderately slower and sometimes faster than a state-of-the-art BDD based mixed engine commercial CEC tool. While SAT based CEC methods need further research and tuning before they can surpass almost a decade of research in BDD based CEC, the recent progress is very promising and merits continued research.

In the paper, we consider the problem of checking whether cubes from a set S are implicants of a DNF formula D, at the same time minimizing the overall time taken by the checks. An obvious but inefficient way of solving the problem is to perform all the checks independently. In the paper, we consider a different approach. The key idea is that when checking whether a cube C from S is an implicant of D we can deduce (learn) implicants of D that are not implicants of C. These cubes can be used in the following checks for search pruning. Experiments on random DNF formulas, DIMACS benchmarks and DNF formulas describing circuits show that the proposed learning procedure reduces the overall time taken by checks by up to two orders of magnitude.

We introduce a new technique for solving some discrete optimization problems exactly. The motivation is that when searching the space of solutions by a standard branch-and-bound (B&B) technique, often a good solution is reached quickly and then improved only a few times before the optimum is found: hence, most of the solution space is explored to certify optimality, with no improvement in the cost function. This suggests that more powerful lower bounding would speed up the search dramatically. More radically, it would be desirable to modify the search strategy with the goal of proving that the given subproblem cannot yield a solution better than the current best one (negative thinking), instead of branching further in search for a better solution (positive thinking). For illustration we applied our approach to the unate covering problem. The algorithm starts in the positive-thinking mode by a standard B&B procedure that generates recursively smaller subproblems. If the current subproblem is "deep" enough, the algorithm switches to the negative thinking mode where it tries to prove that solving the subproblem does not improve the solution. The latter is achieved by a new search procedure invoked when the difference between the upper and lower bound is "small". Such a procedure is complete: either it yields a lower bound that matches the current upper bound, or it yields a new solution better than the current one. We implemented our new search procedure on top of ESPRESSO and SCHERZO, two state-of-art covering solvers used for computer-aided design applications, showing that in both cases we obtain new search engines (respectively, AURA and AURA II) much more efficient than the original ones.

We present a new combinational verification technique where the functional specification of a circuit under verification is utilized to simplify the verification task. The main idea is to assign to each primary input a general function, called a coordinate function, instead of a single variable function as in most BDD-based techniques. BDDs of intermediate nodes are then constructed based on these coordinate functions in a topological order from primary inputs to primary outputs. Coordinate functions depend on primary input variables and extra variables. Therefore combinational verification is performed not over the set of primary input variables but over the extended set of variables. Coordinate functions are chosen in such a way that in the process of computing intermediate functions the dependency on the primary input variables is gradually replaced with that on the extra variables, thereby making Boolean functions associated with primary outputs simple functions only in terms of the extra variables. We show that such a smart choice of coordinate functions is possible with the help of the high-level functional specification of the circuit.

We present a new matrix formulation of the face hypercube embedding problem that motivates the design of an efficient search strategy to find an encoding that satisfies all faces of minimum length. Increasing dimensions of the Boolean space are explored; for a given dimension constraints are satisfied one at a time. The following features help to reduce the nodes of the solution space that must be explored: candidate cubes instead of candidate codes are generated, cubes yielding symmetric solutions are not generated, a smaller sufficient set of solutions (producing basic sections) is explored, necessary conditions help discard unsuitable candidate cubes, early detection that a partial solution cannot be extended to be a global solution prunes infeasible portions of the search tree. We have implemented a prototype package minimum input satisfaction kernel (MINSK) based on the previous ideas and run experiments to evaluate it. The experiments show that MINSK is faster and solves more problems than any available algorithm. Moreover, MINSK is a robust algorithm, while most of the proposed alternatives are not. Besides most problems of the complete Microelectronics Center of North Carolina (MCNC) benchmark suite, other solved examples include an important set of decoder programmable logic arrays (PLA's) coming from the design of microprocessor instruction sets.

We introduce a new technique to solve exactly a discrete optimization problem, based on the paradigm of "negative" thinking. The motivation is that when searching the space of solutions, often a good solution is reached quickly and then improved only a few times before the optimum is found: hence most of the solution space is explored to certify optimality, but it does not yield any improvement of the cost function. So it is quite natural for an algorithm to be "skeptical" about the chance to improve the current best solution. For illustration we have applied our approach to the unate covering problem. We designed a procedure, raiser, implementing a negative thinking search, which is incorporated into a common branch-and-bound procedure. Experiments show that our program, AURA, outperforms both ESPRESSO and our enhancement of ESPRESSO using Coudert's limit lower bound. It is always faster and in the most difficult examples either has a running time better by up to two orders of magnitude, or the other programs fail to finish due to timeout or spaceout. The package SCHERZO is faster on some examples and loses on others, due to a less powerful pruning strategy of the search space, partially mitigated by a more effective computation of the maximal independent set.

We present a new matrix formulation of the face hypercube embedding problem that motivates the design of an efficient search strategy to find an encoding that satisfies all faces of minimum length. Increasing dimensions of the Boolean space are explored; for a given dimension constraints are satisfied one at a time. The following features help to reduce the nodes of the solution space that must be explored: candidate cubes instead of candidate codes are generated, cubes yielding symmetric solutions are not generated, a smaller sufficient set of solutions (producing basic sections) is explored, necessary conditions help discard unsuitable candidate cubes, early detection that a partial solution cannot be extended to be a global solution prunes infeasible portions of the search tree. We have implemented a prototype package MINSK based on the previous ideas and run experiments to evaluate it. The experiments show that MINSK is faster and solves more problems than any available algorithm. Moreover, MINSK is a robust algorithm, while most of the proposed alternatives are not. Besides most problems of the complete MCNC benchmark suite, other solved examples include an important set of decoder PLAs coming from the design of microprocessor instruction sets.