Simulation-Based Bug Trace Minimization With BMC-Based Refinement

Finding the cause of a bug can be one of the most time-consuming activities in design verification. This is particularly true in the case of bugs discovered in the context of a random-simulation-based methodology, where bug traces, or counterexamples, may be several hundred thousand cycles long. In this paper, BUg TRAce MINimization (Butramin), which is a bug trace minimizer, is proposed. Butramin considers a bug trace produced by a random simulator or semiformal verification software and produces an equivalent trace of shorter length. Butramin applies a range of minimization techniques, deploying both simulation-based and formal methods, with the objective of producing highly reduced traces that still expose the original bug. Butramin was evaluated on a range of designs, including the publicly available picoJava microprocessor, and bug traces up to one million cycles long. Experiments show that in most cases, Butramin is able to reduce traces to a very small fraction of their initial sizes, in terms of cycle length and signals involved. The minimized traces can greatly facilitate bug analysis and reduce regression runtime