Boolean satisfiability (SAT) based methods have traditionally been popular for formally verifying properties for digital circuits. We present a novel methodology for formulating a SPICE-type circuit simulation problem as a satisfiability problem. We start with a circuit level netlist, capture the non-linear behavior of the circuits at the transistor level via conservative approximations and transform the simulation problem into a search problem that can be exhaustively explored via a SAT solver. Thus, for DC as well as fixed time-step based transient and periodic steady state (PSS) simulation formulations, the solutions produced by the solver are formal in nature. We also present algorithms for abstraction refinement and smart interval generation to improve the computational efficiency of our proposed solution scheme. We have implemented our ideas into a tool called fSpice which is the first attempt at building a formal SPICE engine. We demonstrate the applicability of our ideas by showing experimental results using pruned versions of real designs that faced challenges during chip tape-out. Categories and Subject Descriptors I.6.5 [Simulation and Modeling]: Model Development General Terms Algorithms, Design

Abstraction techniques have been very successful in model checking large systems by enabling the model checker to ignore irrelevant details. Most abstraction techniques in literature are based on refinement. We introduce the notion of broken traces which capture the necessary and sufficient conditions for the existence of an error path in the abstract model. We formulate abstraction as learning the abstract model from samples of broken traces. Our iterative algorithm for abstraction-based model checking is not based on refinement and can generate the smallest abstract model that proves the property. We present an implementation of this algorithm for the verification of safety properties on gate-level net-lists with localization abstraction. Experimental results prove the viability of our techniques.

We describe new techniques for model checking in the counterexample-guided abstraction-refinement framework. The abstraction phase "hides" the logic of various variables, hence considering them as inputs. This type of abstraction may lead to "spurious" counterexamples, i.e., traces that cannot be simulated on the original (concrete) machine. We check whether a counterexample is real or spurious with a satisfiability (SAT) checker. We then use a combination of 0-1 integer linear programming and machine learning techniques for refining the abstraction based on the counterexample. The process is repeated until either a real counterexample is found or the property is verified. We have implemented these techniques on top of the model checker NuSMV and the SAT solver Chaff. Experimental results prove the viability of these new techniques.

We describe new techniques for model checking in the counterexample guided abstraction/refinement framework. The abstraction phase ‘hides’ the logic of various variables, hence considering them as inputs. This type of abstraction may lead to ‘spurious’ counterexamples, i.e. traces that can not be simulated on the original (concrete) machine. We check whether a counterexample is real or spurious with a SAT checker. We then use a combination of Integer Linear Programming (ILP) and machine learning techniques for refining the abstraction based on the counterexample. The process is repeated until either a real counterexample is found or the property is verified. We have implemented these techniques on top of the model checker NuSMV and the SAT solver Chaff. Experimental results prove the viability of these new techniques. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

In this paper, we present a new technique for the efficient dynamic detection and removal of inactive clauses, i.e. clauses that do not affect the solutions of interest of a Boolean Satisfiability (SAT) problem. The algorithm is based on the extraction of gate connectivity information during generation of the Boolean formula from the circuit, and its use in the inner loop of a branch-and-bound SAT algorithm. The motivation for this optimization is to exploit the circuit structure information, which can be used to find unobservable gates at circuit outputs under dynamic conditions. It has the potential to speed up all applications of SAT in which the SAT formula is derived from a logic circuit. In particular, we find that it has considerable impact on an image computation algorithm based on SAT. We present practical results for benchmark circuits which show that the use of this optimization consistently improves the performance for reachability analysis, in some cases enabling the prototype tool to reach more states than otherwise possible.