Download files
Abstract
Computing devices are pervading our everyday life and imposing challenges for designers
that have the responsibility of producing reliable hardware and software systems. As systems
grow in size and complexity, it becomes increasingly difficult to verify whether a design works as
intended. Conventional verification methods, such as simulation and testing, exercise only parts
of the system and from these parts, draw conclusions about the correctness of the total design.
For complex designs, the parts of the system that can be verified are relatively small. Formal
verification aims to overcome this problem. Instead of exercising the system, formal verification
builds mathematical models of designs and proves whether properties hold in these models. In
doing so, it at least aims to cover the complete design. Model checking is a formal verification
method that automatically verifies a model of a design, or generates diagnostic information if
the model cannot be verified. It is because of this usability and level of automation that model
checking has gained a high degree of success in verifying circuit designs.
The major disadvantage of model checking is its poor scalability. This is due to its algorithmic
nature: namely, every state of the model needs to be enumerated. In practice, properties of
interest may not need the exhaustive enumeration of the model state space. Many properties
can be verified (or falsified) by examining a small number of states. In such cases, exhaustive
algorithms can be replaced with search algorithms that are directed by heuristics. Methods based
on heuristics generally scale well.
This thesis investigates non-exhaustive model checking algorithms and focuses on error detection
in system verification. The approach is based on a novel integration of symbolic model checking,
heuristic search and abstraction techniques to produce a framework that we call abstractiondirected
model checking. There are 3 main components in this framework. First, binary decision
diagrams (BDDs) and heuristic search are combined to develop a symbolic heuristic search algorithm.
This algorithm is used to detect errors. Second, abstraction techniques are applied in
an iterative way. In the initial phase, the model is abstracted, and this model is verified using
exhaustive algorithms. If a definitive verification result cannot be obtained, the same abstraction
is re-used to generate a search heuristic. The heuristic in turn is used to direct a search
algorithm that searches for error states in the concrete model. Third, a model transformation
mechanism converts an arbitrary branching-time property to a reachability property. Essentially,
this component allows this framework to be applied to a more general class of temporal property.
By amalgamating these three components, the framework offers a new verification methodology
that speeds up error detection in formal verification. The current implementation of this framework
indicates that it can outperform existing standard techniques both in run-time and memory
consumption, and scales much better than conventional model checking.