Technical Report PHD-2010-04

In this work we present new approaches to symbolic model checking of hardware systems. Our approaches are aimed at increasing the performance of model checkers. We address the size of the systems that are being checked, the verification runtime, and its memory requirements. Our work is also aimed at increasing the automatization of model checking methodologies, thus decreasing human effort and required expertise of the verification engineer.

In our work we propose a memory efficient hybrid SAT and BDD based algorithm for model checking of circuits. This algorithm exploits the advantages of both SAT and BDD approaches, while avoiding their drawbacks as much as possible.

We also present a 3-valued-SAT based approach for Symbolic Trajectory Evaluation (STE). In this approach, STE is performed by using a novel 3-valued SAT solver, instead of the conventional, BDD-based, approach.

A common approach for addressing the capacity problem in model checking is using abstraction and refinement. In this work we present different methods for automatic refinement in STE, instead of the common manual refinement. These methods require less user effort and expertise, and are less error prone.

We also present an automata theoretic approach to 3-Valued model checking, which can be used for explicit and symbolic model checking. We implement this approach in 3-valued Bounded Model Checking (BMC). Our BMC abstraction outperforms conventional abstraction in BMC both in the sizes of the systems being checked, and in the runtime of the verification tool. We propose a new methodology for using BMC for very large systems, based on our 3-valued abstraction. Our methodology requires significantly less user effort and expertise than the common methodologies for BMC of large designs, and is less error prone.