Up until now classical logic has been the logic of choice in formal hardware verification. This paper advances the application of intu-itionistic logic to the timing analysis of digital circuits. The intuitionistic setting serves two purposes at the same time. The model-theoretic prop-erties are. exploited to handle the second-order nature of bounded delays in a purely prepositional 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 proposi-tional logic, as a special case of a Kripke constraint model for Proposi-tional Lax Logic [4], in which validity is validity up to stabilization. We show that this semantics is equivalently characterized in terms of sta-bilization bounds so that implication D comes out as "boundedly gives rise lo," An intensional semantics for proofs is presented which allows us effectively to compute quantitative stabilization bounds. We discuss the application of the theory to the timing analysis of combi-national circuits. To test our ideas we have implemented an experimental prototype tool and run several simple examples. Proofs are omitted as they appear in an extended technical report [13].
展开▼
