Abstract
The Esterel synchronous programming language is dedicated to hardware or software reactive systems. The constructive semantics determines the reaction of a program to an input event. Esterel programs can be implemented in several ways that yield different time / space tradeoffs. For all the implementations, the code is composed of a control finite-state machine that drives data-handling actions. The FSM can be explicit or implicit. Implicit machines are Boolean circuits that may contain cycles. The cycles are analyzed and removed using BDD based technique. Optimization techniques consist in register removal and logic optimization techniques; they can be tailored to both hardware and software targets. Verification of Esterel programs is based either on synchronous observers and symbolic reachability techniques or on explicit or implicit bisimulation reduction.
Chapter PDF
References
G. Berry. The Constructive Semantics of Esterel. available on the Web at address http://www.inria.fr/meije/esterel/Documentation/main-papers.html, 1996.
G. Berry and G. Gonthier. The Esterel synchronous programming language: Design, semantics, implementation. Science Of Computer Programming, 19(2):87–152, 1992.
F. Boussinot and R. de Simone. The Esterel language. Another Look at Real Time Programming, Proceedings of the IEEE, 79:1293–1304, 1991.
N. Halbwachs. Synchronous Programming of Reactive Systems. Kluwer, 1993.
N. Halbwachs, P. Lagnier, and C. Ratel. Programming and verifying critical systems by means of the synchronous data-flow programming language Lustre. IEEE Transactions on Software Engineering, Special Issue on the Specification and Analysis of Real-Time Systems, September 1992.
S. Malik. Analysis of cyclic combinational circuits. IEEE Trans. Computer-Aided Design, 13(7):950–956, 1994.
E.M. Sentovich, K.J. Singh, L. Lavagno, C. Moon, R. Murgai, A. Saldanha, H. Savoj, P.R. Stephan, R.K. Brayton, and A.L. Sangiovanni-Vincentelli. Sis: A system for sequential circuit synthesis. Technical report, University of California at Berkeley, May 1992.
T. Shiple and G. Berry. Constructive analysis of cyclic circuits. In Proc. International Design and Test Conference ITDC 96, Paris, France, 1996.
H. Toma, E. Sentovich, and G. Berry. Latch optimization in circuits generated from high-level descriptions. In Proc. International Conf. on Computer-Aided Design ICCAD'96, 1996.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Berry, G. (1997). Hardware and software synthesis, optimization, and verification from Esterel programs. In: Brinksma, E. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 1997. Lecture Notes in Computer Science, vol 1217. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0035376
Download citation
DOI: https://doi.org/10.1007/BFb0035376
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-62790-6
Online ISBN: 978-3-540-68519-7
eBook Packages: Springer Book Archive