Abstract
This paper describes a first attempt at building design tools that amalgamate theorem proving and engineering methods. To gain acceptance such a tool must focus on the engineering task and proof steps must be hidden. From these ideas a prototype system based on the HOL proof assistant has been designed. The key features of this system are threefold. First, we use window reasoning for modelling the design process; Second, we have defined a set of application specific derived inference rules that implement common design tasks; Third, we have extended the design representation in logic with annotations to support efficient algorithmic reasoning.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
B. Fjällborg. Pipeline Extraction for Pipeline Synthesis. PhD thesis, Department of Computer and Information Science, Linköping University, S-581 83 Linköping, Sweden, May 1992.
M. Gordon and T. Melham, editors. Introduction to HOL. Cambridge University Press, Cambridge, England, Mar. 1993.
M. J. C. Gordon. Why Higher-Order Logic is a Good Formalism for Specifying and Verifying Hardware. In G. J. Milne and P. A. Subrahmanyam, editors, Formal Aspects of VLSI Design: Proceedings of the Edinburgh Workshop on VLSI, pages 153–177, Edinburgh, Scotland, 1985. North Holland.
J. Grundy. Window Inference in the HOL System. In P. J. Windley, M. Archer, K. N. Levitt, and J. J. Joyce, editors, The Proceedings of the International Tutorial and Workshop on the HOL Theorem Proving System and its Applications, pages 177–189, University of California at Davis, United States, Aug. 1991. ACM/IEEE, IEEE Computer Society Press.
F. K. Hanna, M. Longley, and N. Daeche. Formal Synthesis of Digital Systems. In L. J. M. Claesen, editor, Formal VLSI Specification and Synthesis, VLSI Design Methods-I, volume 1, pages 153–169. IFIP, North Holland, 1990.
S. D. Johnson and B. Bose. DDD — A System for Mechanized Digital System Design Derivation. In Proceedings of the 1991 International Workshop on Formal Methods in VLSI Design, Miami, United States, Jan. 1991. ACM.
M. J. P. Larsson. A Transformational Approach to Formal Digital System Design. Licentiate Thesis 378, Department of Computer and Information Science, Linköping University, May 1993.
E. M. Mayger and M. P. Fourman. Integration of Formal Methods with System Design. In A. Halaas and P. Denyer, editors, VLSI91, Edinburgh, Scotland, 1991. Elsevier.
Z. Peng and K. Kuchcinski. Automated Transformation of Algorithms into Register-Transfer Level Implementations. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 13(2):150–166, Feb. 1994.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Larsson, M. (1994). An engineering approach to formal digital system design. In: Melham, T.F., Camilleri, J. (eds) Higher Order Logic Theorem Proving and Its Applications. HUG 1994. Lecture Notes in Computer Science, vol 859. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58450-1_50
Download citation
DOI: https://doi.org/10.1007/3-540-58450-1_50
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58450-6
Online ISBN: 978-3-540-48803-3
eBook Packages: Springer Book Archive