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 counter-examples, may contain several hundred thousand cycles. In this work we propose Butramin, a bug trace minimizer. Butramin considers a bug trace produced by a random simulator or a semi-formal 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. We evaluated Butramin on a range of designs, including the publicly available picoJava microprocessor. Our experiments show that in most cases Butramin is able to reduce traces to a small fraction of their initial size, in terms of cycle length and signals involved.