Abstract
In formal synthesis methodology, circuit implementations are derived from specifications by means of elementary logical transformation steps, which are performed within a theorem prover. In this approach, additionally to the circuit implementation, the proof that the result is a correct implementation of a given specification is obtained automatically. In the paper, we formally describe the functional semantics of system specifications in higher order logic.This semantics builds the basis for formal synthesis at system level. Further, theorems for circuit optimisation at this level are proposed.
This work has been partly financed by the Deutsche Forschungsgemeinschaft, Project SCHM 623/6-3.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
C. Blumenröhr and D. Eisenbiegler. Performing High-Level Synthesis via Program Transformations within a Theorem Prover, In: Digital System Design Workshop at the 24th EUROMICRO 98 Conference, 1998.
C. Blumenröhr and V. Sabelfeld. Formal Synthesis at the Algorithmic Level, In: Correct Hardware Design and Verification Methods, Charme’99, 1999.
C. Blumenröhr. Aformal approach to specify and synthesize at the system level, In: M. Mutz and N. Lange, eds., GI/ITG/GME Workshop Modellierung und Verifikation von Schaltungen und Systemen, Braunschweig, Germany, February 1999, pp. 11–20, Shaker-Verlag.
M.J.C. Gordon and T.F. Melham. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic, Cambridge University Press, 1993.
J. Iyoda, A. Sampaio, L. Silva. ParTS: APartitioning Transformation System, In: FM’99-Formal Methods, World Congress on Formal Methods in the Development of Computing Systems, LNCS 1709, pp.1400–1419.
K. Jensen. Colored Petri Nets. Basic Concepts, Analysis Methods and Practical Use, Vol.1: Basic Concepts, Springer Verlag 1992.
M. Larsson. An engineering approach to formal digital system design.The Computer Journal, 38(2):101–110, 1995.
T. F. Melham. Automating Recursive Type Definitions in Higher Order Logic, In:G. Birtwistle and P.A. Subrahmanyam, eds., Current Trends in Hardware Verification and Automated Theorem Proving, pp.341–386, Springer-Verlag, 1989.
R. Sharp, O. Rasmussen. The T-Ruby design system. In: IFIP Conference on Hardware Description Languages and their Applications, pp. 587–596, 1995.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Sabelfeld, V., Blumenröhr, C., Kapp, K. (2001). Semantics and Transformations in Formal Synthesis at System Level. In: Bjørner, D., Broy, M., Zamulin, A.V. (eds) Perspectives of System Informatics. PSI 2001. Lecture Notes in Computer Science, vol 2244. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45575-2_16
Download citation
DOI: https://doi.org/10.1007/3-540-45575-2_16
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43075-9
Online ISBN: 978-3-540-45575-2
eBook Packages: Springer Book Archive