Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Timing Analysis of Combinational Circuits in Intuitionistic Propositional Logic

  • Published:
Formal Methods in System Design Aims and scope Submit manuscript

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.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. ACM, in International Workshop on Timing Issues in the Specification and Synthesis of Digital Systems, Intermar Hotel Malente, Germany, September 1993.

    Google Scholar 

  2. S. Akers, "Binary decision diagrams,” IEEE Transactions on Computers, Vol. C-27, pp. 509–516, 1978.

    Google Scholar 

  3. D. Basin, “Extracting circuits from constructive proofs,” in Int'l Workshop on: Formal Methods for VLSI Design, Miami, USA, January 1991. IFIP-IEEE.

  4. D. Basin and N. Klarlund, “Hardware verification using monadic second-order logic,” in Proc. Computer Aided Verification CAV'95. LNCS, Vol. 939, Springer, 1995, pp. 31–41.

    Google Scholar 

  5. J.A. Bergstra and J.W. Klop, “A proof rule for restoring logic circuits,” INTEGRATION, the VLSI Journal, Vol. 1, pp. 161–178, 1983.

    Google Scholar 

  6. M.A. Breuer, “A note on three-valued logic simulation,” IEEE Transactions on Computers, Vol. C-21, No. 4, pp. 399–402, April 1972.

    Google Scholar 

  7. R.E. Bryant, “A switch-level model and simulator for MOS digital systems,” IEEE Transactions on Computers, Vol. C-33, pp.160–177, February 1984.

  8. R.E. Bryant, “Boolean analysis of MOS circuits,” IEEE Transactions on Computer-Aided Design, Vol. 6, No.4, pp. 634–649, July 1987.

    Google Scholar 

  9. J.A. Brzozowski and M. Yoeli, “On a ternary model of gate networks,” IEEE Transactions on Computers, Vol. C-28, pp. 178–184, 1979.

    Google Scholar 

  10. A. Church, “Logic, arithmetic and automata,” in Proc. of the Int. Congr. of Mathematicians, Stockholm, 1962, Almquist and Wiksells, 1963, pp. 23–35.

    Google Scholar 

  11. A.G. Dragalin, Mathematical Intuitionism. Introduction to Proof Theory, American Mathematical Society,1988.

  12. R. Dyckhoff, “Contraction-free sequent calculi for intuitionistic logic,” The Journal of Symbolic Logic, Vol.57, No. 3, pp. 795–807, September 1992.

    Google Scholar 

  13. E.B. Eichelberger, “Hazard detection in combinational and sequential switching circuits,” IBM J. Res. Div., Vol. 9, pp. 90–99, 1965.

    Google Scholar 

  14. H. Eveking and Ch. Mai, “Formal verification of timing conditions,” in European Design Automation Conference,1990, pp. 512–517.

  15. M. Fairtlough and M. Mendler, “Propositional lax logic,” Information and Computation, Vol. 137, No. 1, pp.1–33, August 1997.

    Google Scholar 

  16. M. Fourman, “ Proof and design,” in M. Broy (Ed.), Deductive Program Design, Springer, 1996, pp. 397–439.

  17. T. Franzén, “Algorithmic aspects of intuitionistic propositional logic,” Research Report SICS R87010, Swedish Institute of Computer Science, 1987.

  18. J. Fröl and Th. Kropf, “A new model to uniformly represent function and timing of MOS circuits and its application to VHDL simulation,” in European Design Automation Conference, 1994.

  19. G. Gentzen, “Untersuchungen über das Logische Schlieβen,” Math. Z., Vol. 39, pp. 176–210, 405-431,1934-1935.

    Google Scholar 

  20. J.Y. Girard, Y. Lafont, and P. Taylor, Proofs and Types, Cambridge University Press, 1989.

  21. K. Gödel, “Zum Intuitionistischen Aussagenkalkül,” Akademie der Wissenschaften in Wien, Mathematisch-Naturwissenschaftliche Klasse. Anzeiger., Vol. 69, pp. 65–66, 1932.

    Google Scholar 

  22. M. Gordon, “Why higher-order logic is a good formalism for specifying and verifying hardware,” in P.A. Subrahmanyam and G. Milne (Eds.), Formal Aspects of VLSI Design, North Holland, 1986, pp. 153–178.

  23. M.J.C. Gordon, P. Loewenstein, and M. Shahaf, “Formal verification of a cell library: A case study in technology transfer,” in L.J.M. Claesen (Ed.), Proceedings of the IFIP International Workshop on Applied Formal Methods for Correct VLSI Design, Leuven, Belgium, 1990, North-Holland, Vol. 2, pp. 409–417.

    Google Scholar 

  24. C.T. Gray, W. Liu, and R.K. Cavin III, “Exact timing analysis considering data dependent delays,” in Internatinal Workshop on Timing Issues in the Specification and Synthesis of Digital Systems, Malente, September1993. ACM/GMD.

  25. D.J. Gurr, “Semantic frameworks for complexity,” PhD Thesis, Edinburgh University, Department of Computer Science, January 1991.

  26. S. Hayashi and H. Nakano, PX, A Computational Logic, MIT Press, 1989.

  27. J.P. Hayes, “Uncertainty, energy, and multiple-valued logics,” IEEE Transactions on Computers, Vol. C-35, No. 2, pp. 107–114, February 1986.

    Google Scholar 

  28. J. Herbert, “Formal verification of basic memory devices,” Technical Report 124, University of Cambridge, Computer Laboratory, February 1988.

  29. C.A.R. Hoare, “A theory for the derivation of C-mos circuit designs,” in W.H.J. Feijen, A.J.M. van Fasteren, D. Fries, and J. Misra (Eds.), Beauty is our Business, Springer, 1990.

  30. S.C. Kleene, Introduction to Metamathematics, North Holland, Amsterdam, 1952, Ch. XII, Par. 64.

    Google Scholar 

  31. A. Kolmogoroff, “Zur Deutung der intuitionistischen Logik,” Mathematische Zeitschrift, Vol. 35, pp. 58–65,1932.

    Google Scholar 

  32. K.C. Lam and R.K. Brayton, Timed Boolean Functions. A Unified Formalism for Exact Timing Analysis, Kluwer, 1994.

  33. S. Malik, “Analysis of cyclic combinational circuits,” in International Conference on Computer-Aided Design, IEEE, 1993, pp. 618–625.

  34. T. Margaria and M. Mendler, “Model-based automatic synthesis and analysis in second-order monadic logic,” in Proceedings First ACM SIGPLAN Workshop on Automated Analysis of Software, Paris, France, January1997, pp. 99–112.

  35. L.R. Marino, “General theory of metastable operation,” IEEE Transactions on Computers, Vol. 30, No. 2, pp.107–115, February 1981.

    Google Scholar 

  36. P.C. McGeer and R.K. Brayton, Integrating Functional and Temporal Domains in Logic Design, Kluwer,1991.

  37. Ju.T. Medvedev, “Interpretation of logical formulas by means of finite problems,” Soviet Math. Dokl., Vol. 7, No. 4, pp. 857–860, 1966.

    Google Scholar 

  38. M. Mendler, “Characterising timing analysis in intuitionistic modal logic,” in R.J.G.B. de Queiroz and M. Finger (Eds.), Workshop on Logic, Language, Information, and Computation, Department of Computer Science, IME/USP University of São Paulo, Brazil, 1998, pp. 132–140.

    Google Scholar 

  39. M. Mendler and M. Fairtlough, “Ternary simulation: A refinement of binary functions or an abstraction of real-time behaviour?” in M. Sheeran and S. Singh (Eds.), Proceedings of the 3rd Workshop on Designing Correct Circuits (DCC96), Springer, October 1996. Springer Electronic Workshops in Computing.

  40. M. Mendler and T. Stroup, “Newtonian arbiters cannot be proven correct,” Formal Methods in System Design, Vol. 3, No. 3, pp. 233–257, November/December 1993.

    Google Scholar 

  41. P. Miglioli, U. Moscato, M. Ornaghi, S. Quazza, and G. Usberti, “Some results on intermediate constructive logics,” Notre Dame Journal of Formal Logic, Vol. 30, No. 4, pp. 543–562, 1989.

    Google Scholar 

  42. I. Mitchell and M.R. Greenstreet, “Proving newtonian arbiters correct, almost surely,” in M. Sheeran and S. Singh (Eds.), Designing Correct Circuits, Springer Electronic Workshops in Computing, 1996.

  43. E. Moggi, “The partial lambda calculus,” PhDThesis, Edinburgh University, Department of Computer Science, August 1988.

  44. E. Moggi, “Notions of computation and monads,” Information and Computation, Vol. 93, pp. 55–92, 1991.

    Google Scholar 

  45. B. Moszkowski, “A temporal logic for multilevel reasoning about hardware,” IEEE Computer, Vol. 18, No.2, pp. 10–19, 1985.

    Google Scholar 

  46. M. Parigot, “Programming with proofs: A second-order type theory,” in H. Ganzinger (Ed.), European Symposium on Programming. LNCS, Vol. 300, Springer, 1988, pp. 145–159.

  47. K. Schütte, Systeme Modaler und Intuitionistischer Logik, Vol. 42, Ergebnisse der Mathematik und ihrer Grenzgebiete, Springer, 1968.

  48. R. Statman, “Intuitionistic propositional logic is polynomial space complete,” Theoretical Computer Science,Vol. 9, pp. 67–72, 1973.

    Google Scholar 

  49. P.A. Subrahmanyam, “Towards a framework for dealing with system timing in very high level silicon compilers,” in G. Birtwistle and P. Subrahmanyam (Eds.), VLSI Specification, Verification, and Synthesis, Kluwer,1988, pp. 159–215. Workshop on Hardware Verification.

  50. P. Tharau, BinProlog 4.0 User Guide, Department d'Informatique, Université de Moncton, Canada, September1995.

    Google Scholar 

  51. A.S. Troelstra, “Realizability,” in S.R. Buss (Ed.), Handbook of Proof Theory, Elsevier, 1998, Ch. VI, pp.407–474.

  52. D. van Dalen, “Intuitionistic logic,” in D. Gabbay and F. Guenthner (Ed.), Handbook of Philosophical Logic, Vol. III, Reidel, 1986, Ch. 4, pp. 225–339.

  53. G. von Bochmann, “Hardware specification with temporal logic: An example,” IEEE Transactions on Computers, Vol. C-31, No. 3, pp. 223–231, March 1982.

    Google Scholar 

  54. D. Weise, “Multilevel verification of MOS circuits,” IEEE Transactions on Computer-Aided Design, Vol. 9, No. 4, pp. 341–351, April 1990.

    Google Scholar 

  55. G. Winskel, “A compositional model of MOS circuits,” in G.M. Birtwistle and P.A. Subrahmanyam (Eds.), VLSI Specification, Verification and Synthesis, Kluwer, 1987.

  56. M. Yoeli and J.A. Brzozowski, “Ternary simulation of binary gate networks,” in J.M. Dunn and G. Epstein (Eds.), Modern Uses of Multiple-Valued Logic, D. Reidel, 1977, pp. 41–50.

  57. M. Yoeli and S. Rinon, “Application of ternary algebra to the study of static hazards,” Journal of the ACM, Vol. 11, pp. 84–97, 1964.

    Google Scholar 

  58. Chaochen Zhou and C.A.R. Hoare, “A model for synchronous switching circuits and its theory of correctness,” Formal Methods in System Design, Vol. 1, No. 1, pp. 7–28, July 1992.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Sheffield, Regent Court, 211 Portobello Street, Sheffield, S1 4DP, UK

    Michael Mendler

Authors
  1. Michael Mendler
    View author publications

    You can also search for this author in PubMed Google Scholar

Rights and permissions

Reprints and permissions

About this article

Cite this article

Mendler, M. Timing Analysis of Combinational Circuits in Intuitionistic Propositional Logic. Formal Methods in System Design 17, 5–37 (2000). https://doi.org/10.1023/A:1008780817617

Download citation

  • Issue Date:

  • DOI: https://doi.org/10.1023/A:1008780817617

Search

Navigation