Approximate Symbolic Model Checking Using Overlapping Projections
Abstract
Bugs in hardware cost money. Whenever an error creeps into a design, time and money must be spent to locate the problem and correct it. With the growing complexity of digital systems, and the tremendous pressure for early-time-to-market schedules, the need for verification tools that can help designers catch bugs at an early stage in the design process cannot be overemphasized. Traditional methods of verification are empirical in nature and are based on extensive simulation of hand-written or automatically generated diagnostic test vectors. Although provably effective in the early stages of the debugging process, their effectiveness drops quickly as the size of the state space grows larger. There has been extensive research on more formal methods based on the use of theorem provers to comprehensively verify designs. But these techniques are time consuming and often require a great deal of human expertise to construct a detailed logical proof. An alternative formal verification approach is model checking, in which efficient search procedures are used to automatically determine if the state space of a design satisfies an abstract logical specification. Symbolic model checking extends the scope of verification problems that can be handled automatically, by using symbolic representations with binary decision diagrams (BDDs) rather than explicitly searching the entire state space of the model. However, even the most sophisticated symbolic model checking methods cannot be directly applied to many of today's large designs. Approximate symbolic model checking is an attempt to trade off accuracy with the capacity to deal with bigger designs. This work explores the idea of using a new approximation scheme called overlapping projections. Under this new approximation scheme, the state space is represented using a collection of BDDs that constrain possibly overlapping subsets of the state variables in the system.
Document Details
- Document Type
- Technical Report
- Publication Date
- Aug 01, 2000
- Accession Number
- ADA401015
Entities
People
- Gaurishankar Govindaraju
Organizations
- Stanford University