Verification techniques using symbolic state space traversal rely
on efficient algorithms based on Binary Decision Diagrams(BDDs) for
reachability computation. Unfortunately, BDD size is very sensitive to
the number of variables, variable ordering, and the nature of the logic
expressions being represented. In spite of a large body of work, the
current purely BDD-based approach has been unreliable for designs of
realistic size and functionality because of the state-space explosion
problem.
In this thesis, we propose three approaches to cope with the problem.
The first approach combines Boolean Satisfiability(SAT) techniques with
BDD-based techniques in a single integrated framework. It can be
regarded as SAT providing a disjunctive decomposition of the image
computation into many subproblems, each of which is handled in the
standard way using BDDs. Various novel heuristics such as BDD bounding,
partition-based decision and dynamic detection and removal of inactive
clauses have been proposed to improve the performance further. The
second approach is motivated by the fact that the number of variables
is a critical parameter that affects the performance of BDD packages.
We propose a technique called variable reuse to reduce the variable
usage. It works synergetically with conjunctive partitioning and early
quantification, leading to further savings in reachability
analysis. The third approach explores behavioral hierarchy of the
designs. It is most useful in modern software design languages that
promote hierarchy as one of the key constructs for structuring complex
specifications.
Full thesis
Department of Computer and Information Science,
University of Pennsylvania