Correct Hardware Design and Verification Methods

Abstract

In this paper, we emphasize the importance of efficient debugging in formal verification and present capabilities that we have developed in order to augment debugging in Intel’s Formal Verification Environment. We have given the name the counter-example wizard to the bundle of capabilities that we have developed to address the needs of the verification engineer in context of counter-example diagnosis and rectification. The novel features of the counterexample wizard are the multi-value counter-example annotation, multiple root cause detection, and constraint-based debugging mechanisms. Our experience with the verification of real-life Intel designs shows that these capabilities complement one another and can considerably help the verification engineer diagnose and fix a reported failure. We use real-life verification cases to illustrate how our system solution can significantly reduce the time spent in the loop of model checking, specification and design modification.