Guiding simulation with increasingly refined abstract traces

11 years 2 months ago
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
Kuntal Nanshi, Fabio Somenzi
Added 13 Nov 2009
Updated 13 Nov 2009
Type Conference
Year 2006
Where DAC
Authors Kuntal Nanshi, Fabio Somenzi
Comments (0)