Searching for counter-examples intelligently

Details Searching for counter-examples intelligently Searching for counter-examples intelligently

2001-01-16

2003-07-01

Siek, Vuthe (Department: 2825)

Computer-aided design and analysis of circuits and semiconductor

Nanotechnology related integrated circuit design

C716S030000, C716S030000

Reexamination Certificate

active

06587998

ABSTRACT:

FIELD OF THE INVENTION
The present invention relates generally to design verification in transition systems and to reachability analysis in finite state machines, and specifically to hardware and software verification of integrated circuit design using methods of reachability analysis.
BACKGROUND OF THE INVENTION
Hardware verification is currently the bottleneck and the most expensive task in the design of a semiconductor integrated circuit. Model checking is a method of formal verification that is gaining in popularity for this purpose. The method is described generally by Clarke et al., in
Model Checking
(MIT Press, 1999), which is incorporated herein by reference.
To perform model checking of the design of a device, a verification engineer reads the definition and functional specifications of the device and then, based on this information, writes a set of properties (also known as a specification) that the design is expected to fulfill. The properties are written in a suitable specification language for expressing temporal logic relationships between the inputs and outputs of the device. A hardware model (also known as an implementation) of the design, which is typically written in a hardware description language, such as VHDL or Verilog, is then tested to ascertain that the model satisfies all of the properties in the set under all possible input sequences. Such testing is a form of reachability analysis, in that it verifies that beginning from an initial state, the device as designed will, under appropriate conditions, reach an intended final state. Additionally, the testing verifies that particular “bad” states will not be reached from an initial state of the device under any conditions.
Model checking is preferably carried out automatically by a symbolic model checking program, such as SMV, as described, for example, by McMillan in
Symbolic Model Checking
(Kluwer Academic Publishers, 1993), which is incorporated herein by reference. A number of practical model checking tools are available, among them RuleBase, developed by IBM, which is described by Beer et al. in “RuleBase: an Industry-Oriented Formal Verification Tool,” in
Proceedings of the Design Automation Conference DAC'
96 (Las Vegas, Nev., 1996), which is incorporated herein by reference.
Even if the verification engineer is able to detect the existence of a design defect, there is an additional need to construct a sequence of states and transitions (a path) that leads to the problematic state of the design. This path is called a counterexample. Having such a counterexample allows the engineer to assess the impact of the problem and to address the bug specifically during redesign. Recent research described by Aziz and Ganai in “Efficient Coverage Directed State Space Search,” in
Proceedings of the International Workshop on Logic Synthesis
(Lake Tahoe, Calif., 1998), and by Dill and Yand in “Validation with Guided Search of the State Space,” in
Proceedings of the
35
th ACM/IEEE Design Automation Conference
(1998), have noted the importance of this constructive counterexample approach. Both of these articles are incorporated herein by reference.
The most commonly used method in industry of finding a counterexample is to do a type of breadth-first search (BFS) of all states reached from a starting state and see if a problem state is reached. Because BFS is an exhaustive search, it explores all possible transition paths between states. Often, however, some of the paths may be ruled out as potential counterexamples by simple methods. Also, BFS may not detect even a very simple counterexample until it has investigated many other paths. Thus, BFS may spend significantly more time and computational resources than are tolerable to the engineer in arriving at a solution.
Another approach has been to use a directed search, as described by Dill and Yand, cited earlier, and by Abraham et al., in “On Combining Formal and Informal Verification,” in
Proceedings of the Computer Aided Verification Conference
(1997), which is incorporated herein by reference. In a directed search, a heuristic is used to assign scores to states. The scores are meant to represent the likelihood that the state is a member of a counterexample path. By ranking the states by their scores, the search is directed toward those states believed most likely to produce a counterexample.
The efficiency and efficacy of a directed search are highly dependent on the scoring heuristic employed. Methods of directed search known in the art use heuristics that are either chosen a priori by the user or are determined by pre-processing the model immediately prior to beginning the search. Choosing a good heuristic in advance is very difficult. Pre-processing to find a good heuristic can be extremely time consuming.
If a heuristic does not lead to the production of a counterexample when one is known to exist, the heuristic scores must be refined. One approach has been to refine the entire model, as described by Clarke et al., in “Counterexample-Guided Abstraction Refinement,” in
Proceedings of the Computer Aided Verification Conference
(2000), which is incorporated herein by reference.
Any implementation of these approaches relies on an underlying data structure that can represent Boolean functions efficiently. This efficiency is measured by the amount of memory space required by the data structure to represent the function and by the time and complexity required to manipulate the data structures. The data structure of choice used by practitioners in the art has been the binary decision diagram (BDD). In particular, many of the approaches to finding counterexamples mentioned above use implicitly conjoined BDDs, as described by Dill and Hu in “Efficient Verification with BDDs using Implicitly Conjoined Invariants,” in
Lecture Notes in Computer Science
697 (Springer-Verlag, 1993), which is incorporated herein by reference. Some methods of manipulating BDDs are described by Ravi et al., in “Approximation and Decomposition of Binary Decision Diagrams,” in
Proceedings of the
35
th ACM/IEEE Design Automation Conference
(1998), by Ravi and Somenzi, in “High-Density Reachability Analysis,” in
Proceedings of the IEEE International Conference on Computer Aided Design
(1994), and by Beer and Geist in “Efficient Model Checking by Automated Ordering of Transition Relation Partitions,” in
Proceedings of the Computer Aided Verification Conference
(1994), which are incorporated herein by reference.
SUMMARY OF THE INVENTION
Preferred embodiments of the present invention provide an improved method for finding counterexamples in a transition system. The method is particularly useful in formal verification of hardware and software designs. A heuristic is constructed “on the fly” for use in choosing states of the system that are likely candidates to belong to counterexamples. When the current heuristic is discovered to be incorrect, it is refined based on knowledge of earlier mistakes. As a result, the process of refinement is efficient and low in overhead. When the correct heuristic is discovered, it identifies a small portion of the state space of the system in which it is known that a counterexample can be found. This portion of the state space can be searched quickly to find the counterexample.
In preferred embodiments of the present invention, a formal verification framework receives as part of its input a design model having the form of a transition system. The system comprises a set of states, including a subset of initial states and a subset of final states, along with a transition relation between the states. An operator of the system identifies a set of “bad” states, which should not be reachable from an initial state of the system if the model is correct.
The framework works in two directions to find a heuristic that will lead to a counterexample, i.e., a path from an initial state to a bad state. The system searches backwards from the bad states toward the initial states by estimating the minimum number of transition steps needed to reach a bad state f

Affiliated with

Also associated with

Rating

Searching for counter-examples intelligently does not yet have a rating. At this time, there are no reviews or comments for this patent.

If you have personal experience with Searching for counter-examples intelligently, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Searching for counter-examples intelligently will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFUS-PAI-O-3030131