Abstract
Formal Synthesis is a methodology developed at Kent for combining circuit design and verification. We have reinterpreted this methodology in Isabelle’s theory of higher-order logic so that circuits are synthesized using higher-order resolution. Our interpretation simplifies and extends Formal Synthesis both conceptually and in implementation. It also supports integration of this development style with other synthesis methodologies and leads to techniques for developing new classes of circuits, e.g., recursive descriptions of parameterized circuits.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
David A. Basin. Logic frameworks for logic programs. In 4th International Workshop on Logic Program Synthesis and Transformation, (LOPSTR'94), volume 883 of LNCS, pages 1–16, Pisa Italy, June 1994. Springer-Verlag.
David A. Basin and Nils Klarlund. Hardware verification using monadic second-order logic. In Computer-Aided Verification (CAV’ 95), volume 939 of LNCS, pages 31–41. Springer-Verlag, 1995.
A. J. Camilleri, M. J. C. Gordon, and T. F. Melham. Hardware verification using higher-order logic. In D. Borrione, editor, From HDL Descriptions to Guaranteed Correct Circuit Designs. North Holland, September 1986.
Martin David Coen. Interactive program derivation. Technical Report 272, Cambridge University Computer Laboratory, Cambridge, November 1992.
S. Finn, M. P. Fourman, M. Francis, and R. Harris. Formal system design — interactive synthesis based on computer-assisted formal reasoning. In Dr. Luc Claesen, editor, IMEC-IFIP International Workshop on Applied Formal Methods for Correct VLSI Design, volume 1, pages 97–110, Amsterdam, 1989. Elsevier Science publishers B.V. (North-Holland).
Cordell Green. Application of theorem proving to problem solving. In Proceedings of the IJCAI-69, pages 219–239, 1969.
F. Keith Hanna, Neil Daeche, and Mark Longley. Formal synthesis of digital systems. In IMEC-IFIP International Workshop on: Applied Formal Methods For Correct VLSI Design, volume 2, pages 532–548, Leuven, Belgium, 1989.
F.K. Hanna, N. Daeche, and M. Longley. VERITAS+: A specification language based on type theory. In Handware Specification, Verification and Synthesis: Mathematical Aspects, Ithaca, New York, 1989, Springer-Verlag.
John L. Hennessy and David A. Patterson. Computer Architecture, a Quantitative Approach. Morgan Kaufmann, 1990.
Lawrence C. Paulson. Isabelle: a generic theorem prover; with contributions by Tobias Nipkow, volume 828 of LNCS. Springer, Berlin, 1994.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Basin, D., Friedrich, S. (1996). Modeling a hardware synthesis methodology in isabelle. In: Goos, G., Hartmanis, J., van Leeuwen, J., von Wright, J., Grundy, J., Harrison, J. (eds) Theorem Proving in Higher Order Logics. TPHOLs 1996. Lecture Notes in Computer Science, vol 1125. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0105395
Download citation
DOI: https://doi.org/10.1007/BFb0105395
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61587-3
Online ISBN: 978-3-540-70641-0
eBook Packages: Springer Book Archive