Automatic Fault Localization for Property Checking

Author

Fey, Görschwin ; Staber, Stefan ; Bloem, Roderick ; Drechsler, Rolf

Author_Institution

Univ. of Bremen, Bremen

Volume

27

Issue

6

fYear

2008

fDate

6/1/2008 12:00:00 AM

Firstpage

1138

Lastpage

1149

Abstract

We present an efficient fully automatic approach to fault localization for safety properties stated in linear temporal logic. We view the failure as a contradiction between the specification and the actual behavior and look for components that explain this discrepancy. We find these components by solving the satisfiability of a propositional Boolean formula. We show how to construct this formula and how to extend it so that we find exactly those components that can be used to repair the circuit for a given set of counterexamples. Furthermore, we discuss how to efficiently solve the formula by using the proper decision heuristics and simulation-based preprocessing. We demonstrate the quality and efficiency of our approach by experimental results.

Keywords

CAD; electronic engineering computing; fault location; integrated circuit design; temporal logic; Boolean formula; automatic fault localization; circuit repair; decision heuristics; linear temporal logic; property checking; safety properties; satisfiability; simulation-based preprocessing; Automatic logic units; Circuit faults; Circuit simulation; Debugging; Fault diagnosis; Formal verification; Hardware design languages; Safety; Sequential circuits; Debugging; formal verification; satisfiability checking; sequential circuit fault diagnosis;

fLanguage

English

Journal_Title

Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on

Publisher

ieee

ISSN

0278-0070

Type

jour

DOI

10.1109/TCAD.2008.923234

Filename

4526741