Title: 3-Valued Abstraction in (Bounded) Model Checking for Hardware

Orna Grumberg (Technion)


Abstract:
Model Checking is the problem of verifying that a given model satisfies a
specification, given in a formal specification language. Abstraction
is one of the most successful methods to avoid the state explosion problem
in model checking. It simplifies the model being checked, in order to
make model checking easier.
3-valued abstraction is a simple way to obtain abstraction in hardware.
It lets the state variables range over the ternary domain {0,1,X},
where X stands for ``unknown''. X is used to abstract away parts
of the circuit that are irrelevant for the property being checked.

For 3-valued abstractions, checking an abstract model may result in 1 or 0,
if the property holds or fails on the model, respectively. Alternatively,
it may result in X, if it is impossible to determine whether the property
holds or fails due to a too coarse abstraction. In the latter case,
the abstract model is refined by replacing some of the X's with the relevant
parts of the circuit. The 3-valued abstraction and refinement can be applied
either automatically or manually.

In this talk we present an automata theoretic approach to
3-valued abstraction in hardware model checking.
We show how our 3-valued framework can be incorporated into SAT based
bounded model checking and induction based unbounded model checking.
We implemented it within Intel's BMC tool and obtained outstanding results.


This is a joint work with Avi Yadgar, Alon Flaisher, and Michael Lifshits