The formal analysis of hardware timing properties

A framework is presented in which circuit timing issues may be isolated, specified and formally verified. This approach to reasoning about time differs from current timing analysis work in that a complete formal analysis infrastructure is created rather than a single timing analysis tool. The infrastructure has been used to discover methodologies for rigorously reasoning about the temporal properties of digital hardware. The resulting modelling framework is based on CIRCAL, a formal concurrent process model developed for the purpose of rigorously describing and analysing properties of highly complex concurrent systems such as those found in integrated circuit hardware. Fundamental to this analytical infrastructure is an algebraic or constructive technique for establishing the timing properties of a complex circuit´s modules from the timing properties of its constituent parts. The intention is to use a formal model of hardware behaviour to lay the foundations of such tools. The CIRCAL model therefore provides a description language as the single medium in which to specify the behaviour of hardware under analysis and the timing properties which that hardware should possess. Formal verification techniques which ensures that given timing properties are satisfied by a particular circuit design are an intrinsic part of this approach to design and analysis