Describing and verifying synchronous circuits with the Boyer-Moore theorem prover

  • Laurence Pierre
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 987)


In this paper, we address the problem of finding a simple and efficient functional form for describing synchronous sequential circuits in the Boyer-Moore logic. By simple, we mean that it must be both user-readable and easily obtained by translation from a Hardware Description Language like VHDL. By efficient, we mean that it must be well-adapted to the proof mechanisms of the tool, Nqthm.

We propose two different recursive models, which are inspired from former results. We explain how they can be expressed in the Boyer-Moore logic, and we compare them on simple but illustrative examples. We also give the Nqthm proof of their equivalence. Finally, we conclude about their respective advantages and drawbacks.


Recursive Function Formal Verification Primary Input Recursive Model Mechanical Proof 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. [BD,77]
    R.BURSTALL, J.DARLINGTON: “A transformation system for developing recursive programs”. Journal of the ACM. Vol. 24, 1. January 1977.Google Scholar
  2. [BF,93]
    J.M.BERGé, A.FONKOUA, S.MAGINOT, J.ROUILLARD: “VHDL'92: The New Features of the VHDL Hardware Description Language”. Kluwer Academic Pub., 1993.Google Scholar
  3. [BK,91]
    F.P.BURNS, D.J.KINNIMENT, A.M.KOELMANS: “Correct interactive transformational synthesis of DSP hardware”. Proc. European Design Automation Conference. Amsterdam (The Netherlands). 25–28 February 1991.Google Scholar
  4. [BM,88]
    R.S.BOYER, J S.MOORE: “A Computational Logic Handbook”. Perspectives in Computing, Vol. 23. Academic Press, Inc. 1988.Google Scholar
  5. [BP,92]
    D.BORRIONE, L.PIERRE, A.SALEM: “Formal Verification of VHDL Descriptions in the PREVAIL Environment”. IEEE Design&Test Magazine, Vol. 9, nℴ2. June 1992.Google Scholar
  6. [Br,89]
    A.BRONSTEIN: “String-Functional Semantics and the Boyer-Moore Mechanization for the Formal Verification of Synchronous Circuits”. PhD Thesis, Stanford University, Report nℴ STAN-CS-89-1293. December 1989.Google Scholar
  7. [BT,89]
    A.BRONSTEIN, C.L.TALCOTT: “Formal Verification of Pipelines based on String-Functional Semantics”. Proc. IFIP WG 10.2 Int. Workshop Nov. 1989. In “Formal VLSI Correctness Verification”, L.Claesen Ed., North Holland, 1990.Google Scholar
  8. [Ca,87]
    R.CAMPOSANO: “Structural Synthesis: Some References”. Advanced Summer Course on “Logic Synthesis and Silicon Compilation for VLSI Design”. L'Aquila (Italy). 13–18 July 1987.Google Scholar
  9. [CP,88]
    P.CAMURATI, P.PRINETTO: “Formal Verification of Hardware Correctness: Introduction and Survey of Current Research”. IEEE Computer, Vol.21, nℴ7. July 1988.Google Scholar
  10. [CP,91]
    S.COUPET-GRIMAL, L.PIERRE: “Recursive Models for Synchronous Sequential Devices”. Research Report IMAG/ARTEMIS nℴ 855-I, Grenoble (France). July 1991.Google Scholar
  11. [Di,78]
    D.DIETMEYER: “Logic Design of Digital Systems”. Allyn and Bacon. 1978.Google Scholar
  12. [Go,80]
    M.GORDON: “The denotational semantics of sequential machines”. Information Processing Letters, Vol.10, nℴ1. February 1980.Google Scholar
  13. [Go,84]
    M.GORDON: “LCF-LSM”. Technical Report nℴ41. Univ. of Cambridge (UK). 1984.Google Scholar
  14. [Go,85]
    M.GORDON: “HOL: a machine-oriented formulation of higher order logic”. Technical Report nℴ68. University of Cambridge (UK). May 1985.Google Scholar
  15. [Gu,92]
    A.GUPTA: “Formal Hardware Verification Methods: a Survey”. Formal Methods in System Design, Vol.1, 1992.Google Scholar
  16. [GW,85]
    S.M.GERMAN, Y.WANG: “Formal Verification of Parameterized Hardware Designs”. Proc. IEEE Int. Conf. on Computer Design: VLSI in Computers, October 1985.Google Scholar
  17. [HB,89]
    W.A.HUNT, B.C.BROCK: “The Verification of a Bit-slice ALU”. Workshop on Hardware Specification, Verification and Synthesis: Mathematical Aspects. Cornell University, Ithaca, NY (USA). 5–7 July 1989.Google Scholar
  18. [HK,92]
    P.HARRISON, H.KHOSHNEVISAN: “A new approach to recursion removal”. Theoretical Computer Science 93, 1992.Google Scholar
  19. [HL,78]
    G.HUET, B.LANG: “Proving and Applying Program Transformations Expressed with Second-Order Patterns”. Acta Informatica 11. 1978.Google Scholar
  20. [Hu,86]
    W.A.HUNT: “FM8501: A verified microprocessor”. Institute for Computing Science, University of Texas, Austin (USA). Technical Report nℴ47. February 1986.Google Scholar
  21. [Ie,88]
    IEEE Standard VHDL Language Reference Manual, IEEE. 1988.Google Scholar
  22. [Jo,84]
    S.D.JOHNSON: “Synthesis of Digital Designs from Recursion Equations”. The MIT Press, Cambridge. 1984.Google Scholar
  23. [Jo,86]
    S.D.JOHNSON: “Digital Design in a Functional Calculus”. In G.J.Milne and P.A.Subrahmanyam Eds., Proc. of the Workshop on Formal Aspects of VLSI Design. Elsevier Science Publishers, 1986.Google Scholar
  24. [Ka,74]
    G.KAHN: “The Semantics of a Simple Language for Parallel Programming”. Proc. IFIP Congress 74. Amsterdam (The Netherlands). 1974.Google Scholar
  25. [KP,94]
    M.KAUFMANN, P.PECCHIARI: “Interaction with the Boyer-Moore Theorem Prover: a Tutorial Study using the Arithmetic-Geometric Mean Theorem”, Technical Report nℴ100, Computational Logic Inc., August 1994.Google Scholar
  26. [OD,87]
    J.T.O'DONNELL: “Hardware Description with Recursion Equations”. Proc. Int. Conf. on CHDL'87, Amsterdam (The Netherlands). M.Barbacci and C.Koomen Eds., Elsevier Science Publishers, 1987.Google Scholar
  27. [Pi,91a]
    L.PIERRE: “One Aspect of Mechanizing Formal Proof of Hardware: the Generalization of Partial Specifications”. Proc. ACM International Workshop on Formal Methods in VLSI Design. Miami (USA). January 1991.Google Scholar
  28. [Pi,91b]
    L.PIERRE: “From a HDL Description to Formal Proof Systems: Principles and Mechanization”. Proc. 10th Int. Symposium CHDL'91. Marseille (France), April 1991. In “CHDL and their Applications”, D.Borrione & R.Waxman ed., North Holland, 1991.Google Scholar
  29. [Pi,94]
    L.PIERRE: “An automatic generalization method for the inductive proof of replicated and parallel architectures”. Proc. International Conference on Theorem Provers in Circuit Design. Bad Herrenalb (Germany), September 1994.Google Scholar
  30. [Ru,92]
    D.M.RUSSINOFF: “A Mechanical Proof of Quadratic Reciprocity”. Journal of Automated Reasoning, Vol.8, nℴ1, 1992.Google Scholar
  31. [Sh,85]
    N.SHANKAR: “A mechanical proof of the Church-Rosser theorem”. Institute for Computing Science, University of Texas, Austin. Technical Report nℴ45. March 1985.Google Scholar
  32. [VV,92]
    D.VERKEST, J.VANDENBERGH, L.CLAESEN, H.DE MAN: “A description methodology for parameterized modules in the Boyer-Moore logic”. In “Theorem provers in circuit design”, V.Stavridou, T.Melham & R.Boute ed., North Holland, 1992.Google Scholar
  33. [Yu,90]
    Y.YU: “Computer Proofs in Group Theory”. Journal of Automated Reasoning, Vol.6, nℴ3, 1990.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • Laurence Pierre
    • 1
  1. 1.Laboratoire d'Informatique de MarseilleURA CNRS 1787 CMI / Université de ProvenceMarseille Cedex 13France

Personalised recommendations