IEEE Transactions on Computers · 1998 · 101 citations · 17 references
ComputingComputer EngineeringComputer ScienceFormal MethodsHardware Description LanguagesModel-based Systems EngineeringControl-flow AnalysisFinite State Machine ModelingVerificationAbstractionCoverageCoverage AnalysisFormal VerificationFunctional CoverageState Space ExplorationState-space StructureTest Generation
The enormous state spaces which must be searched when verifying the correctness of, or generating tests for, complex circuits precludes the use of traditional approaches. Hard-to-find abstractions are often required to simplify the circuits and make the problems tractable. This paper presents a simple and automatic method to extract the control flow of a circuit so that the resulting state space can be explored for validation coverage analysis and automatic test generation. This control flow, capturing the essential "behavior" of the circuit, is represented as a finite state machine called the ECFM (Extracted Control Flow Machine). Simulation is currently the primary means of verifying large circuits, but the definition of a coverage measure for simulation vectors is an open problem. We define functional coverage as the amount of control behavior covered by the test suite. We then combine formal verification techniques, using BDDs as the underlying representation, with traditional ATPG techniques to automatically generate additional sequences which traverse uncovered parts of the control state graph. We also demonstrate how the same abstraction techniques can complement ATPG techniques when attacking hard-to-detect faults in the control part of the design for which conventional ATPG alone proves to be inadequate or inefficient at best. Results on large designs show significant improvement over conventional algorithms.
17
Graph-Based Algorithms for Boolean Function Manipulation
Bryant · IEEE Transactions on Computers · 1986 · 8.9K citations · Full text
HITEC: a test generation package for sequential circuits
T.M. Niermann, J.H. Patel · 2002 · 522 citations
Sequential circuit verification using symbolic model checking
Jerry R. Burch, E. M. Clarke, Kenneth L. McMillan et al. · 1990 · 413 citations · Full text
Implicit state enumeration of finite state machines using BDD's
H.J. Touati, H. Savoj, Binshan Lin et al. · 2002 · 403 citations