A Modal Logic for Handling Behavioural Constraints in Formal Hardware Verification
Michael Mendler · 2018
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 tr~table pieces.Unfortunately however, behavioural abstractions are genuine mathernatical abstractions only up to behavioural con- straints, i.e. under certain restrictions imposed on the device's environment.Timing constraints on input signals form an irnportant 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 approzimately 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 rnodality 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.university degree before.Some of the introductory ma.teria.l in Cha.pter 1 a.nd Section 2.3, a.nd the exa.mple in Section 4.2 ha.ve alrea.dya.ppeared in an early version a.s (Men9la].