http://www.eecg.utoronto.ca/~veneris/10aspdac.pdf
Debugging is still the most time consuming part of IC design. Typical debug includes: (a) find out the checkers that indicate errors, (b) investigate waveforms of observation points (typically primary outputs) which may propagate errors to the checkers, (c) trace drivers of those observation points, (d) indicate error sources, (e) fix them, and finally (f) re-run simulation to make sure the bugs disappear. The whole process is very, very labor intensive. Are there any automation tools that can help?
This paper presents the techniques for automatic debugging. Given design source code (RTL) and simulation error traces, the tool automatically tells designers “OK, the error sources come from those lines; please take care of them”. In other words, automatic debugging let designers skip steps (a)(b)(c)(d) and focus on steps (e)(f).
The basic underlying techniques of an automatic debugging tool are very similar to those of formal verification tools: BDDs, SAT, QBF, etc… Thus, the notorious challenges that accompany those techniques are the same – scaling – larger design with longer error traces. To conquer the problem, the authors introduce an important observation: “error sources are often excited temporally close to failure points”. They even make some experiments by simplifying the error behavior model and calculating the probability of error sources to prove the observation. No matter how realistic the experiment reveals, this part is the most interesting section that is worth reading again.
Based on the “error source temporal proximity to failure point” observation, the authors propose the approach “bounded model debugging” which is very similar to the concept of BMC (bounded model checking) used in formal property verification. The experiments show that 2.7 times more problems can be solved.




Discussion
No comments for “[Jack’s Paper Study Note] Managing Verification Error Traces with Bounded Model Debugging – Sean Safarpour et al. @ ASPDAC’10”