Abstract
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.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
R.BURSTALL, J.DARLINGTON: “A transformation system for developing recursive programs”. Journal of the ACM. Vol. 24, 1. January 1977.
J.M.BERGé, A.FONKOUA, S.MAGINOT, J.ROUILLARD: “VHDL'92: The New Features of the VHDL Hardware Description Language”. Kluwer Academic Pub., 1993.
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.
R.S.BOYER, J S.MOORE: “A Computational Logic Handbook”. Perspectives in Computing, Vol. 23. Academic Press, Inc. 1988.
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.
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.
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.
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.
P.CAMURATI, P.PRINETTO: “Formal Verification of Hardware Correctness: Introduction and Survey of Current Research”. IEEE Computer, Vol.21, nℴ7. July 1988.
S.COUPET-GRIMAL, L.PIERRE: “Recursive Models for Synchronous Sequential Devices”. Research Report IMAG/ARTEMIS nℴ 855-I, Grenoble (France). July 1991.
D.DIETMEYER: “Logic Design of Digital Systems”. Allyn and Bacon. 1978.
M.GORDON: “The denotational semantics of sequential machines”. Information Processing Letters, Vol.10, nℴ1. February 1980.
M.GORDON: “LCF-LSM”. Technical Report nℴ41. Univ. of Cambridge (UK). 1984.
M.GORDON: “HOL: a machine-oriented formulation of higher order logic”. Technical Report nℴ68. University of Cambridge (UK). May 1985.
A.GUPTA: “Formal Hardware Verification Methods: a Survey”. Formal Methods in System Design, Vol.1, 1992.
S.M.GERMAN, Y.WANG: “Formal Verification of Parameterized Hardware Designs”. Proc. IEEE Int. Conf. on Computer Design: VLSI in Computers, October 1985.
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.
P.HARRISON, H.KHOSHNEVISAN: “A new approach to recursion removal”. Theoretical Computer Science 93, 1992.
G.HUET, B.LANG: “Proving and Applying Program Transformations Expressed with Second-Order Patterns”. Acta Informatica 11. 1978.
W.A.HUNT: “FM8501: A verified microprocessor”. Institute for Computing Science, University of Texas, Austin (USA). Technical Report nℴ47. February 1986.
IEEE Standard VHDL Language Reference Manual, IEEE. 1988.
S.D.JOHNSON: “Synthesis of Digital Designs from Recursion Equations”. The MIT Press, Cambridge. 1984.
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.
G.KAHN: “The Semantics of a Simple Language for Parallel Programming”. Proc. IFIP Congress 74. Amsterdam (The Netherlands). 1974.
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.
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.
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.
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.
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.
D.M.RUSSINOFF: “A Mechanical Proof of Quadratic Reciprocity”. Journal of Automated Reasoning, Vol.8, nℴ1, 1992.
N.SHANKAR: “A mechanical proof of the Church-Rosser theorem”. Institute for Computing Science, University of Texas, Austin. Technical Report nℴ45. March 1985.
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.
Y.YU: “Computer Proofs in Group Theory”. Journal of Automated Reasoning, Vol.6, nℴ3, 1990.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Pierre, L. (1995). Describing and verifying synchronous circuits with the Boyer-Moore theorem prover. In: Camurati, P.E., Eveking, H. (eds) Correct Hardware Design and Verification Methods. CHARME 1995. Lecture Notes in Computer Science, vol 987. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60385-9_3
Download citation
DOI: https://doi.org/10.1007/3-540-60385-9_3
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60385-6
Online ISBN: 978-3-540-45516-5
eBook Packages: Springer Book Archive