Formal design verification is a methodology for detecting logical errors in
systems. In formal design verification, the designer describes a system in a
language with a mathematical semantics, and then the system description is
analyzed against various correctness requirements. The paradigm is called
*model checking* when the analysis is performed automatically by
exhaustive state-space exploration. A correctness requirement is usually
specified either as a formula expressed in temporal logic, or as an abstract
design expressed in the system's description language. If the requirement is
specified as an abstract design, the verification problem is called
*refinement checking*. This thesis extends the state-of-art by
increasing both the class, and the size of systems on which automatic and
semi-automatic refinement checking are viable.

Refinement checking problems are formulated in the form *I < S*, where
*I* is a description of the system, *S* is the requirement, and <
is a preorder over system descriptions. Depending on the properties we
ascribe to the < preorder, we get different notions of refinement. Three
orthogonal property classes characterize the refinement preorder, namely,
(1) linear and branching views of time, (2) finite and fair views of system
behaviors, and (3) spatial and temporal abstraction of the requirement. We
develop the theory of fair branching refinements, and give an efficient
algorithm to check such refinements. We propose a novel and efficient
algorithm to check refinements involving temporal abstractions.

Refinement checking algorithms usually explore and analyze the state space of
the system. As we seek to enhance the applicability of model checking to
complex designs, we are faced with the so-called *state-explosion*
problem: the size of the state space grows exponentially with the size of the
system description, making exhaustive state-space exploration infeasible.
Scalable approaches to refinement checking make use of the compositional
structure of both implementation and specification, and divide the
verification task at hand into simpler subtasks. Each such subtask involves
checking if an implementation-component refines its corresponding
specification-component. Discharging such subtasks requires assumptions
about inputs to the implementation-component. These assumptions are taken
into account by the *assume-guarantee* approach, which uses the
specification for the inputs as assumptions on the inputs (the apparent
circularity in such proofs is resolved by an induction over time). We prove
soundness of the assume-guarantee rule when applied to branching refinements
(both finite and fair cases). We propose a new assume-guarantee proof rule
for checking refinements of implementations against requirements that are
both spatially and temporally abstract.

The techniques have been implemented in a new verification tool called Mocha. Mocha has been used successfully to detect and fix elusive bugs in a signal-processing chip that has 6 million transistors.

Ph.D. thesis, University of California at Berkeley, September 1999, 142 pages.

Download PostScript / PDF document.