Paper Info
Title
Timing Analysis of Combinational Circuits in Intuitionistic Propositional Logic
Abstract
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.
Year
DOI
Venue
2000
10.1023/A:1008780817617
Formal Methods in System Design
Keywords
Field
DocType
formal verification,timing analysis,combinational circuits,intuitionistic logic,realisability
Intuitionistic logic,Autoepistemic logic,Computer science,Zeroth-order logic,Theoretical computer science,Modal logic,Many-valued logic,Well-formed formula,Propositional variable,Intermediate logic
Journal
Volume
Issue
ISSN
17
1
1572-8102
Citations 
PageRank 
References 
5
0.69
24
Authors
1
Name
Order
Citations
PageRank
Michael Mendler131434.60