New directions in refinement checking

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-sparce exploration. A correctness requirement is usually specified either in the system's description language. If the requirement is specified as an . 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 Impl $⪯$ Spec, where Impl is a description of the system, Spec 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, the theory of fair branching refinements, and give an efficient algorithm to check such refinements. We propose a novel and efficient algorithm to check 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 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.