BDD-based debugging of designs using language containment and fair CTL

Abstract

Formal design verification should be used to reveal bugs early in the design cycle. A tool exhibiting counter-examples (a debugger) is therefore essential. We describe debugging techniques for two important approaches to formal design verification: model checking using Computation Tree Logic ([Cla86]) and language containment using L-automata ([Kur90]). The contributions of this work are: 1. A debugger for language containment (LC), using L-automata, which guarantees some minimality criteria. 2. A debugger for fair CTL ([Eme87]) model checking based on the algorithms for LC debugging. 3. Enhanced early failure detection (EFD) ([Hoj92]) algorithms for LC, and simple EFD algorithms for a subset of CTL formulas, called ACTL (for All CTL) in positive normal form. All algorithms are based on Binary Decision Diagrams (BDD’s). The algorithms have been partly implemented. We comment on some experimental results.