Formal and semi-formal verification  

Satori : Efficient Sequential SAT for circuits
 
In this project, we develop new methods for checking satisfiability of Boolean constraints in sequential circuits The so-called sequential SAT problem. This has wide application in verification and validation of sequential circuits, logic synthesis, equivalence checking, and debugging.
 
DPLL search in the sequential space
We use a DPLL-style decision procedure for the solver. The satisfiability of a Boolean constraint is translated into checking for reachability of the states where the Boolean constraint is false from a set of initial states. This is done through a backward search using implicit time-frame expansion of the next-state logic of the sequential circuit [1] as shown in Figure 1.
 

Figure 1. A single snapshot of the search in time. Objectives are a set of values on present state lines. A set of states encoded as a cube is found using SAT on the previous state lines. This is then iteratively set as an objective if the initial state is not in the set of new states found. Intuitively, the search can be randomized by collecting different sets of states. We then start search from these sets based on some ordering heuristic.
 
Initially, we start from the states where the constraint is false (the current states). We then find a set of states that can reach the current states in one step and see whether any of these states lie in the initial state set. If so, we terminate, or else we continue, by using the newly reached states as new current states. The one-step reachable states are found using 3-valued logic (0/1/X), which allows us to implicitly enumerate large state sets with minimal overhead. The search is efficiently bounded using additional Boolean constraints to encode the visited states (also called state blocking clauses) as already reached and hence never to be visited again [1, 3]. The procedure is complete and in practice, is quite efficient.
 
We also use additional optimization techniques such as heuristic enlargement of the solution state sets without search, learning on the state solutions, compression of the state sets using two-level minimization techniques, and efficient state caching.
 
Different search strategies employed while traversing the state space yield differing performances on hard benchmarks. We have found that the best strategy is a randomized search that prioritizes the search objective based on a variety of metric.
 
Preliminary Results
 

Figure 2. Property checking on an implementation of the Bakery mutual-exclusion protocol. The time for solving the individual SAT instances for BMC increases exponentially with the number of time-steps, while the asymptotic run-time behavior of sequential SAT is considerably less extreme.
 
Sequential SAT has been applied to property checking and found to be superior to bounded model checking (BMC) [2]. The results can be quite spectacular, as shown in Figure 2. In practice, SATORI performs consistently better than BMC on the benchmarks that we possess, when using a standard SAT solver like Zchaff.  We would appreciate hearing from interested researchers who would like to use this approach and give us feedback on their experience with the tool.
 
The principal benefit of SATORI is the fact that it is complete and can correctly terminate for True properties (constraints), which is not true in general for BMC.
 
Current Status
We are currently applying SATORI to equivalence-checking and validation of circuit models.
 
Availability
The SATORI package is currently maintained by Feng Lu. It has been compiled and tested on x86/sparc platforms running Linux and Solaris using g++2.96. The source code and binaries to SATORI can be downloaded from Download.
 
Publications:
• M. K. Iyer, G. Parthasarathy, and K.-T. Cheng, "SATORI An Efficient Sequential SAT Solver for Circuits",  Proceedings of  the International  Conference on CAD (ICCAD),  Oct, 2003.
• G. Parthasarathy, M.K. Iyer, Li-C. Wang, and K.-T. Cheng, "Evaluation of BDDs, BMC, and Sequential SAT for Model Checking", High Level Design Validation and Test Workshop (HLDVT),  Nov, 2003.
• G. Parthasarathy, M.K. Iyer, Li-C. Wang, and K.-T. Cheng, "Efficient Reachability Analysis Using Sequential SAT", Asia and South Pacific Design Automation Conference(ASP-DAC),  Jan, 2004.
• G. Parthasarathy, M.K Iyer, K.-T. Cheng, "Safety Property Checking using Sequential SAT", To appear, IEEE Design & Test of Computers, IEEE Computer Society, 2004.