Michael Mendler

Lax Logic and its Application to the Timing Analysis of Combinational Systems

Traditionally, classical logic is the logic of choice in formal system analysis. This talk discusses the application of an intuitionistic modal logic, Lax Logic, to the timing analysis of combinational systems. In contrast to classical logic, proofs in intuitionistic logic do not only witness the mere extensional fact "that" a given functional specification is valid but also provide intensional information about "how" it is valid. The best-known technical formalisation of this is the so-called "propositions-as-types" or "proofs-as-programs" principle.

The application of Lax Logic rests on a novel variant of this idea, called the "proofs-as-constraints" or "proofs-as-delays" principle. Following this principle I will show how timing information may be extracted from proofs in Propositional Lax Logic (PLL). This suggest a verification-driven timing analysis system, based on an automatic theorem prover for PLL. In my talk I will sketch the basic ingredients of such a system.

The proposed timing analysis framework exploits the fact that in PLL one and the same (Boolean) input-output function may be represented in many different ways. Depending on the particular the specification style different amounts of timing information can be associated with the function. The granularity can be adjusted within wide limits and in this way several standard timing analysis methods, and many non-standard ones, may be characterised as special cases of this general principle.

June 4, 1999
Wean 8220