Guiding simulation with increasingly refined abstract traces

Traces Kuntal Nanshi, Fabio Somenzi University of Colorado at Boulder ne abstraction refinement and simulation to provide a more efficient approach to checking invariant properties whose only counterexamples are very long traces. We allow each transition of act error trace to map to multiple transitions of the concrete error trace and simulate pseudorandom vectors to build segments of the concrete trace. This approach addresses the capacity limitation of the formal verification engine as well as the short-sightedness of the simulator, thus providing a more effective technique for deep, subtle bugs. Categories and Subject Descriptors B.6.3 [Logic design]: Design aids--Verification General Terms: Verification, Algorithms

• Type: Conference
• Year: 2006
• Where: DAC
• Authors: Kuntal Nanshi, Fabio Somenzi
• Keywords: Act Error Trace, Concrete Error Trace, Concrete Trace, DAC 2006, Design Automation