Efficient debugging in a formal verification environment
| Autor: | Osnat Weissberg, Fady Copty, Nathan P. Kropp, Gila Kamhi, Amitai Irron |
|---|---|
| Rok vydání: | 2003 |
| Předmět: |
High-level verification
Functional verification Programming language Computer science media_common.quotation_subject Runtime verification computer.software_genre Intelligent verification Debugging Verification computer Formal verification Software Software verification Information Systems media_common |
| Zdroj: | International Journal on Software Tools for Technology Transfer (STTT). 4:335-348 |
| ISSN: | 1433-2787 1433-2779 |
| Popis: | In this paper, we emphasize the importance of efficient debugging in formal verification and present capabilities that we have developed in order to aid debugging in Intel’s Formal Verification Environment. We have given the name “Counter-Example Wizard” to the bundle of capabilities that we have developed to address the needs of the verification engineer in the context of counter-example diagnosis and rectification. The novel features of the Counter-Example Wizard are the multi-value counter-example annotation, constraint-based debugging, and multiple counter-example generation mechanisms. Our experience with the verification of real-life Intel designs shows that these capabilities complement one another and can 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full text from SpringerLink