caa a22 4500 475797566 CHVBK 20180406123728.0 cr unu---uuuuu 170329e20000801xx s 000 0 eng 10.1023/A:1008780817617 doi (NATIONALLICENCE)springer-10.1023/A:1008780817617 Mendler Michael Department of Computer Science, University of Sheffield, Regent Court, 211 Portobello Street, S1 4DP, Sheffield, UK aut Timing Analysis of Combinational Circuits in Intuitionistic Propositional Logic [Elektronische Daten] [Michael Mendler] Classical logic has so far been the logic of choice in formal hardware verification. This paper proposes the application of intuitionistic logic to the timing analysis of digital circuits. The intuitionistic setting serves two purposes. The model-theoretic properties are exploited to handle the second-order nature of bounded delays in a purely propositional setting without need to introduce explicit time and temporal operators. The proof-theoretic properties are exploited to extract quantitative timing information and to reintroduce explicit time in a convenient and systematic way. We present a natural Kripke-style semantics for intuitionistic propositional logic, as a special case of a Kripke constraint model for Propositional Lax Logic (Information and Computation, Vol. 137, No. 1, 1-33, 1997), in which validity is validity up to stabilisation, and implication ⊃ comes out as "boundedly gives rise to.” We show that this semantics is equivalently characterised by a notion of realisability with stabilisation bounds as realisers. Following this second point of view an intensional semantics for proofs is presented which allows us effectively to compute quantitative stabilisation bounds. We discuss the application of the theory to the timing analysis of combinational circuits. To test our ideas we have implemented an experimental prototype tool and run several examples. Kluwer Academic Publishers, 2000 formal verification nationallicence timing analysis nationallicence combinational circuits nationallicence intuitionistic logic nationallicence realisability nationallicence Formal Methods in System Design Kluwer Academic Publishers 17/1(2000-08-01), 5-37 0925-9856 17:1<5 2000 17 10703 https://doi.org/10.1023/A:1008780817617 text/html Onlinezugriff via DOI 1 research-article jats NATIONALLICENCE 856 40 https://doi.org/10.1023/A:1008780817617 text/html Onlinezugriff via DOI NATIONALLICENCE 100 1- Mendler Michael Department of Computer Science, University of Sheffield, Regent Court, 211 Portobello Street, S1 4DP, Sheffield, UK aut NATIONALLICENCE 773 0- Formal Methods in System Design Kluwer Academic Publishers 17/1(2000-08-01), 5-37 0925-9856 17:1<5 2000 17 10703 Metadata rights reserved Springer special CC-BY-NC licence nationallicence BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-springer