Title | Managing Verification Error Traces with Bounded Model Debugging |
Author | *Sean Safarpour (Vennsa Technologies, Canada), Andreas Veneris, Farid Najm (University of Toronto, Canada) |
Page | pp. 601 - 606 |
Keyword | debugging, verification, simulation, formal |
Abstract | Managing long verification error traces is one of the key challenges of automated debugging engines. Today, debuggers rely on the
iterative logic array to model sequential behavior which drastically limits their application. This work presents Bounded Model
Debugging, an iterative, systematic and practical methodology to allow debuggers to tackle larger problems than previously possible. Based on the empirical observation that errors are excited in temporal proximity of the observed failures, we present a framework that improves performance by up to two orders of magnitude and solve 2.7$\times$ more problems than a conventional debugger. |
Slides |
Title | A Method for Debugging of Pipelined Processors in Formal Verification by Correspondence Checking |
Author | *Miroslav Velev, Ping Gao (Aries Design Automation, U.S.A.) |
Page | pp. 619 - 624 |
Keyword | formal verification, debugging, pipelined processors, correspondence checking, SAT |
Abstract | Presented is a method for debugging of pipelined processors in their formal verification with the highly automatic and scalable approach of Correspondence Checking, where a pipelined/superscalar/VLIW implementation is compared against a non-pipelined specification via an inductive correctness criterion based on symbolic simulation in a way that guarantees the correctness of the implementation for all possible execution scenarios. The benefit from the proposed method increases with the complexity of the processor under formal verification. For a 12-stage VLIW processor that imitates the Intel Itanium in many features, the method reduced the size of the EUFM correctness formulas from buggy processors by up to an order of magnitude, the number of Boolean variables in the equivalent propositional correctness formulas and the number of 1s in the counterexample traces by up to 2 orders of magnitude, and resulted in an average speedup in detecting the bugs of 2 orders of magnitude, thus increasing the productivity of the processor designers. |