Temporal abstraction of digital designs

From datacite.

Abstract

Formal techniques have been used to verify the function of reasonably large digital devices ([Hunt85], [Cohn87]), and also to describe and reason about digital signal behaviour at a detailed timing level [Hanna85] [Herbert86]. Different models are used: simple synchronous models of components are the basis for verifying high-level functional specifications; more detailed models which capture the behaviour of signals in real time are the basis for proofs about timing. The procedure called temporal abstraction is a technique for formally relating these two behavioral models. The background to temporal abstraction is presented and the details of its implementation in HOL. The HOL language ([Gordon85a]) is a computerised version of higher-order logic which has an associated proof assistant also called HOL. In HOL one may specify behaviour at both the functional and timing levels. This work describes how the relationship between these levels may also be described in HOL and reasoned about using the HOL system. The formal transformation of descriptions of behaviour at the timing level to behaviour at the functional level involves generating and verifying timing constraints. This process can be identified with the conventional design activity of timing analysis. This work shows that timing verification can be viewed, not as a separate phase of design, but as part of a single verification process which encompasses functional and timing verification. A single formal language, HOL, is used to describe all aspects of the behaviour and a single verification system provides all the proofs of correctness. The use of uniform, formal techniques is shown to have a number of advantages.