Abstract
Since the beginning of time, the semantics of choice for synchronous circuits has been the finite state machine (FSM). Years of research on FSMs have provided many tools for the design and verification of synchronous hardware. But from a mathematical manipulation point of view, FSMs have several drawbacks, and a new hardware specification style based on the functional approach has gained ground recently. Earlier we described a functional semantics for synchronous circuits based on monotonic length-preserving (MLP) functions on finite strings. We have now implemented this theory inside the Boyer-Moore theorem prover, and proved correctness properties for a variety of circuits. In 1985 Paillet presented an interesting sequence of synchronous circuits of increasing "sequential complexity", with hand-proofs of their correctness in his P-calculus. Our semantics supports a calculus which extends his. It was therefore very tempting to investigate mechanical proofs of those circuits in the Boyer-Moore implementation of our theory. We present the results here.
This research was partially supported by Digital Equipment Corp. and by ARPA contract N00039-84-C-0211.
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
Amblard, Paul; Caspi, Paul; Halbwachs, Nicolas. Describing and Reasoning about Circuit Behaviour by Means of Time Functions. In 7th Int'l. Conf. on Computer Hardware Design Languages, pp. 39–48, 1985.
Booth, Taylor L., Sequential Machines and Automata Theory. John Wiley & Sons, New York, 1967.
Borrione, D.; Paillet, J.L.; Pierre, L. Formal Verification of CASCADE Descriptions. In Int'l. Conf. on Fusion of Hardware Design and Verification, pp. 183–208, 1988.
Boute, Raymond T. An Introduction to System Semantics. In Embedded Systems (LNCS 284), pp. 91–107, 1987.
Boyer, Robert S.; Moore, J Strother. A Computational Logic. Academic Press, New York, 1979.
Boyer, Robert S.; Moore, J Strother. A Mechanical Proof of the Unsolvability of the Halting Problem. ICSCA-CMP-28,Institute for Computing Science, Univ. of Texas at Austin, TX 78712, 1982.
Boyer, Robert S.; Moore, J Strother. The User's Manual for A Computational Logic. TR 18, CLInc, 1717 W. 6th St., Suite 290, Austin TX 78703, 1988.
Bronstein, Alexandre; Talcott, Carolyn L. String-Functional Semantics for Formal Verification of Synchronous Circuits. STAN-CS-88-1210, Computer Science Dept., Stanford University, CA 94305, 1988.
Cohn, A. A Proof of Correctness of the VIPER Microprocessor: The First Level. In VLSI Specification, Verification and Synthesis, pp. 27–71, 1988.
Dill, David L. Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits. Ph.D. Th., CMU-CS-88-119, Computer Science Dept., Carnegie-Mellon Univ., Pittsburgh PA 15213, 1988.
Dill, D.L.; Clarke, E.M. "Automatic Verification of Asynchronous Circuits Using Temporal Logic", IEE Proceedings, v. 133, pt. E, no. 5, pp. 276–282 (1986).
Halbwachs, N.; Longchamp, A.; Pilaud, D. Describing and Designing Circuits by means of a Synchronous Declarative Language. In From HDL Descriptions to Guaranteed Correct Circuit Designs, pp. 255–268, 1987.
Hobley, K.M.; Thompson, B.C.; Tucker, J.V. Specification and Verification of Synchronous Concurrent Algorithms: A Case Study of a Convolution Algorithm. In Int'l. Conf. on Fusion of Hardware Design and Verification, pp. 342–369, 1988.
Hunt, Warren A. Jr. FM8501: A Verified Microprocessor. Ph.D. Th., TR 47, Institute for Computing Science, Univ. of Texas at Austin, TX 78712, 1985.
Johnson, Steven D. Synthesis of Digital Designs from Recursion Equations. Ph.D. Th., Indiana University, The MIT Press, Cambridge, Massachusetts, 1983.
Johnson, Steven D. Applicative Programming and Digital Design. In 11th Symp. on Principles of Programming Languages, Salt Lake City, pp. 218–227, 1984.
Kloos, Carlos Delgado. Semantics of Digital Circuits. Ph.D. Th., Lecture Notes in Computer Science 285, Springer-Verlag, 1987.
Kogge, Peter M.. The Architecture of Pipelined Computers. Hemisphere Publishing, New York, 1981.
Leiserson, Charles E.; Saxe, James B. "Optimizing Synchronous Systems". Journal of VLSI and Computer Systems, v. 1, no. 1, pp. 41–67 (1983).
Leiserson, Charles E.; Saxe, James B. Retiming Synchronous Circuitry. TR 13, Digital Systems Research Center, 130 Lytton AV, Palo Alto CA 94301, 1986.
McCluskey, Edward J.. Logic Design Principles. Prentice-Hall, Englewood Cliffs, New Jersey 07632, 1986.
Mead, Carver A.; Conway, Lynn A.. Introduction to VLSI Systems. Addison-Wesley, Reading, Massachusetts, 1980.
O'Donnell, John T. Hardware Description with Recursion Equations. In 8th Int'l. Conf. on Computer Hardware Description Languages, pp. 363–382, 1987.
O'Donnell, J. HYDRA: Hardware Description in a Functional Language Using Recursion Equations and High Order Combining Forms. In Int'l. Conf. on Fusion of Hardware Design and Verification, pp. 305–324, 1988.
Paillet, J.L. Un Modèle de Fonctions Séquentielles pour la Vérification Formelle de Systèmes Digitaux. Rep. 546, IMAG-ARTEMIS, Grenoble, France, 1985.
Paillet, J.L. A Functional Model for Descriptions and Specifications of Digital Devices. In From HDL Descriptions to Guaranteed Correct Circuit Designs, pp. 21–42, 1987.
Sheeran, Mary. μFP — an Algebraic VLSI Design Language. Ph.D. Th., PRG-39, Oxford Univ. Computing Lab, 8–11 Keble Rd. Oxford OX1 3QD, England, 1983.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1990 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bronstein, A., Talcott, C.L. (1990). Formal verification of synchronous circuits based on string-functional semantics: The 7 paillet circuits in boyer-moore. In: Sifakis, J. (eds) Automatic Verification Methods for Finite State Systems. CAV 1989. Lecture Notes in Computer Science, vol 407. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-52148-8_27
Download citation
DOI: https://doi.org/10.1007/3-540-52148-8_27
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-52148-8
Online ISBN: 978-3-540-46905-6
eBook Packages: Springer Book Archive