A Modal Logic for Handling Behavioural Constraints in Formal Hardware Verification

From bibtex.

Abstract

The application of formal methods to the design of correct computer hardware depends crucially on the use of abstraction mechanisms to partition the synthesis and verification task into tractable pieces. Unfortunately however, behavioural abstractions are genuine mathematical abstractions only up to behavioural constraints, i.e. under certain restrictions imposed on the device's environment. Timing constraints on input signals form an important class of such restrictions. Hardware components that behave properly only under such constraints satisfy their abstract specifications only approximately. This is an impediment to the naive approach to formal verification since the question of how to apply a theorem prover when one only knows approximately what formula to prove has not as yet been dealt with. In this thesis we propose, as a solution, to interpret the notion of 'correctness up to constraint' as a modality of intuitionistic predicate logic so as to remove constraints from the specification and to make them part of its proof. This provides for an 'approximate' verification of abstract specifications and yet does not compromise the rigour of the argument since a realizability semantics can be used to extract the constraints. Also, the abstract verification is separated from constraint analysis which in turn may be delayed arbitrarily. In the proposed framework constraint analysis comes down to proof analysis and a computational semantics on proofs may be used to manipulate and simplify constraints.