Data processing: structural design – modeling – simulation – and em – Modeling by mathematical expression
Reexamination Certificate
2000-10-23
2004-04-27
Paladini, Albert W. (Department: 2125)
Data processing: structural design, modeling, simulation, and em
Modeling by mathematical expression
C716S030000, C716S030000
Reexamination Certificate
active
06728665
ABSTRACT:
I. DESCRIPTION
I.A. Field
The present disclosure is related to image and pre-image computation. Specifically, this disclosure teaches a technique that combines Binary Decision Diagram (BDD)-based techniques and Satisfiability Testing (SAT)-based techniques to exploit their complementary benefits.
I.B. Background
Image and pre-image computation play a central role in symbolic state space traversal, which is at the core of a number of applications in Very Large Scale Integrated Circuits (VLSI) Computer Aided Design (CAD) like verification, synthesis, and testing. Exact reachability analysis for sequential system verification is emphasized in this disclosure, though the techniques can also be used for exact invariant checking, exact model checking, approximate reachability analysis, approximate invariant checking, and approximate model checking. For simplicity and easier understanding, only image computation is considered. It should be noted that, the techniques presented could be used for pre-image computation as well.
I.B.1. BDD-based Methods
Verification techniques based on symbolic state space traversal rely on efficient algorithms based on BDDs for computing the image of an input set over a Boolean relation. For further details on symbolic state space traversal, see J. R. Burch, E. M. Clarke, D. E. Long, K. L. McMillan, and D. L. Dill; and Symbolic model checking for sequential circuit verification.
IEEE Transactions on Computer
-
Aided Design
, 13(4):401-424, April 1994, and O. Coudert, C. Berthet, and J. C. Madre. Verification of synchronous sequential machines using symbolic execution. In
Proceedings of the International Workshop on Automatic Verification Methods for Finite State Systems
, Volume 407 of Lecture Notes in Computer Science, pages 365-373, June 1989. For further details on BDDs, see R. E. Bryant. Graph-based algorithms for Boolean function manipulation.
IEEE Transactions on Computers, C-
35(8):677-691, August 1986.
The input set for the verification problem is the set of present states P, and the Boolean relation is the transition relation T, i.e., the set of valid present-state, next-state combinations. In case of hardware, it is also convenient to include the primary inputs in the definition of T. The use of BDDs to represent the characteristic function of the relation, the input, and the image set, allows image computation to be performed efficiently through Boolean operations and variable quantification. As an example of an application, the set of reachable states is computed by starting from a set P which denotes the set of initial states of a system, and using image computation iteratively, until a fixpoint is reached.
A number of researchers have proposed the use of partitioned transitioned relations, where the BDD for the entire transition relation is not built a priori. See J. R. Burch, E. M. Clarke, and D. E. Long. Representing circuits more efficiently in symbolic model checking, In
Proceedings of the
28
th Design Automation Conference
, pages 403-407, June 1991; and H. J. Touati, H. Savoj, B. Lin, R. K. Brayton, and A. Sangiovanni-Vincentelli. Implicit state enumeration of finite state machines using BDDs. In
Proceedings of the International Conference on Computer
-
Aided Design
, pages 130-133, 1990.
Typically, the partitions are represented using multiple BDDs, and their conjunction is interleaved with early variable quantification during image computation. Many heuristics have been proposed to find a good quantification schedule, i.e., an ordering of the conjunctions which minimizes the number of peak variables. For more details, see D. Geist and I. Beer. Efficient model checking by automatic ordering of transition relation partitions, in
Proceedings of the International Conference on Computer
-
Aided Verification
, Volume 818 of Lecture Notes in Computer Science, pages 299-310, 1994; and R. K. Ranjan, A. Aziz, R. K. Brayton, B. F. Plessier, and C. Pixley. Efficient BDD algorithms for ESM synthesis and verification, in
International Workshop for Logic Synthesis
, May 1995. Lake Tahoe, Calif. Further, there has also been an interest in using disjunctive partitions of the transition relations and state sets, which effectively splits the image computation into smaller sub-problems. For more details, see G. Cabodi, P. Camurati, and S. Quer. Improving the efficiency of BDD-based operators by means of partitioning,
IEEE Transactions on Computer
-
Aided Design of Integrated Circuits and Systems
, 18(5):545-556, May 1999; I.-H. Moon, J. Kukula, K. Ravi, and F. Somenzi. To split or to conjoin: The question in image computation, in
Proceedings of the Design Automation Conference
, pages 23-28, June 2000; and A. Narayan, A. J. Isles, J. Jam, H. K. Brayton, and A. Sangiovanni-Vincentelhi. Reachability analysis using partitioned ROBDDs, in
Proceedings of the International Conference on Computer
-
Aided Design
, pages 388-393, 1997.
Importantly, BDD-based techniques work well when it is possible to represent the sets of states and the transition relation using BDDs. The representation-can be as a whole, or in a usefully partitioned form. However, BDD size is very sensitive to various factors including: the number of variables, variable ordering, and the nature of the logic expressions being represented. In spite of a large body of conventional work, the verification techniques based purely on BDD technique have been unreliable for designs of realistic size and functionality.
I.B.2. Combining BDDs with SAT-based Methods
On the other hand, an alternative technique used extensively in testing applications, uses Conjunctive Normal Form (CNF) to represent transition relation and further, uses Boolean Satisfiability Checking (SAT) for performing analysis. For more details, see T. Larrabee., Test pattern generation using Boolean satisfiability,
IEEE Transactions on Computer
-
Aided Design of Integrated Circuits and Systems
, 11(1):4-15, January 1992. SAT solver technology has improved significantly in recent years with a number of sophisticated packages now available, e.g. J. P. Marquez-Silva, Grasp package, http://algos.inesc.pt/{tilde over ( )}jpms/software.html.
For checking equivalence of two given combinational circuits C
1
and C
2
, a typical approach is to prove that the XOR of their corresponding outputs can never evaluate to 1, as shown in FIG.
1
. Such an XOR of the corresponding output is also called the miter circuit output. A proof for the above proposition can be provided either by building a BDD for the miter, or by using a SAT solver to prove that no satisfying assignment exists for the miter output. In cases where the two methods fail individually, BDDs and SAT can also be combined, for example, in the manner shown in
FIG. 1. A
cut is identified in the miter circuit to divide the circuit into, two parts: the part P
I
of the circuit between the circuit inputs and the cut, and the part P
O
of the circuit between the cut and the output. A BDD is built for P
O
, while P
I
is represented in CNF. A SAT solver then tries to enumerate all valid combinations at the cut using the CNF for P
I
, while checking that it is not contained in the on-set of the BDD for P
O
. See A. Gupta and P. Ashar. Integrating a Boolean satisfiability checker and BDDs for combinational verification. In
Proceedings of the VLSI Design Conference
, January 1998. Enumerating the valid combinations at the cut corresponds exactly to computing the image of the input set over the Boolean relation corresponding to P
I
. Other ways of combining BDDs and SAT for equivalence checking have also been proposed. See J. Burch and V. Singhal. Tight integration of combinational verification methods. In
Proceedings of the International Conference on Computer
-
Aided Design
, pages 570-576, 1998.
For property checking, the effectiveness of SAT solvers for finding bugs has also been demonstrated in the context of bounded model checking and symbolic reachability analysis. See P. A. Abdulla, P. Bjesse, and N. Een. Symbolic reachability analysis based on SAT-solvers. In
Tools and
Ashar Pranav
Gupta Aarti
Yang Zijiang
NEC Corporation
Paladini Albert W.
LandOfFree
SAT-based image computation with application in reachability... does not yet have a rating. At this time, there are no reviews or comments for this patent.
If you have personal experience with SAT-based image computation with application in reachability..., we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and SAT-based image computation with application in reachability... will most certainly appreciate the feedback.
Profile ID: LFUS-PAI-O-3223122