Backward reasoning with formal properties: a methodology for bug isolation on simulation traces

Automated methods for bug localization for hardware designs typically work on the design implementation to root-cause a given bug. This paper presents a novel debugging approach where instead of using the design implementation in the debugging process, we use causal deduction using formal properties scattered across the design to locate the bug. This has two advantages, namely, (a) the reasoning takes place in the property space instead of the state space of the implementation, which enhances scalability, and (b) new properties can be added in hindsight to perform what-if analysis, which is less expensive than modifying the implementation for each alternative. Experimental results demonstrate the scalability of the approach in debugging designs with large property suites