Title :
Automatic Fault Localization for Property Checking
Author :
Fey, Görschwin ; Staber, Stefan ; Bloem, Roderick ; Drechsler, Rolf
Author_Institution :
Univ. of Bremen, Bremen
fDate :
6/1/2008 12:00:00 AM
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;
Journal_Title :
Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on
DOI :
10.1109/TCAD.2008.923234
