Test generation using SAT-based bounded model checking for validation of pipelined processors

Functional verification is one of the major bottlenecks in microprocessor design. Simulation-based techniques are the most widely used form of processor verification. Efficient test generation is crucial for the simulation-based verification. We present an efficient test generation methodology using SAT-based bounded model checking (BMC). This paper addresses two important challenges in test generation using SAT-based BMC: determination of bound for each property, and application of design and property decompositions to improve test generation time as well as memory requirement. Our experimental results using a MIPS processor demonstrate the feasibility and usefulness of our approach. Categories and Subject Descriptors: B.6.3 [Logic Design]: Design Aids - verification General Terms: Verification

• Type: Conference
• Year: 2006
• Where: GLVLSI
• Authors: Heon-Mo Koo, Prabhat Mishra
• Keywords: Efficient Test Generation, GLVLSI 2006, Test Generation, Test Generation Methodology, VLSI