Abstract
Since the synchronous model of computation is shared between synchronous languages and synchronous hardware circuits, synchronous languages lend themselves well for hardware/software codesign in the sense that from the same synchronous program both hardware and software can be generated. In this chapter, we informally describe the syntax and semantics of the imperative synchronous language Quartz and explain how these programs are first analyzed and then compiled to hardware and software: To this end, the programs are translated to synchronous guarded actions whose causality has to be ensured as a major consistency analysis of the compiler. We then explain the synthesis of hardware circuits and sequential programs from synchronous guarded actions and briefly look at extensions of the Quartz language in the conclusions.
Similar content being viewed by others
References
Benveniste A, Bournai P, Gautier T, Le Guernic P (1985) SIGNAL: a data flow oriented language for signal processing. Research report 378, Institut National de Recherche en Informatique et en Automatique (INRIA), Rennes
Benveniste A, Caspi P, Edwards S, Halbwachs N, Le Guernic P, de Simone R (2003) The synchronous languages twelve years later. Proc IEEE 91(1):64–83
Berry G (1992) A hardware implementation of pure Esterel. Sadhana 17(1):95–130
Berry G (1999) The constructive semantics of pure Esterel. http://www-sop.inria.fr/members/Gerard.Berry/Papers/EsterelConstructiveBook.pdf
Berry G (2000) The Esterel v5 language primer. ftp://ftp.inrialpes.fr/pub/synalp/reports/esterel-primer.pdf.gz
Berry G, Gonthier G (1992) The Esterel synchronous programming language: design, semantics, implementation. Sci Comput Program 19(2):87–152
Boussinot F (1998) SugarCubes implementation of causality. Research report 3487, Institut National de Recherche en Informatique et en Automatique (INRIA), Sophia Antipolis
Brandt J (2013) Synchronous models for embedded software. Master’s thesis, Department of Computer Science, University of Kaiserslautern. Habilitation
Brandt J, Gemünde M, Schneider K, Shukla S, Talpin JP (2012) Representation of synchronous, asynchronous, and polychronous components by clocked guarded actions. Des Autom Embed Syst (DAEM). doi: http://10.1007/s10617-012-9087-9
Brandt J, Gemünde M, Schneider K, Shukla S, Talpin JP (2013) Embedding polychrony into synchrony. IEEE Trans Softw Eng (TSE) 39(7):917–929
Brandt J, Schneider K (2011) Separate translation of synchronous programs to guarded actions. Internal report 382/11, Department of Computer Science, University of Kaiserslautern, Kaiserslautern
Brandt J, Schneider K, Shukla S (2010) Translating concurrent action oriented specifications to synchronous guarded actions. In: Lee J, Childers B (eds) Languages, compilers, and tools for embedded systems (LCTES). ACM, Stockholm, pp 47–56
Brzozowski J, Seger CJ (1995) Asynchronous circuits. Springer, New York/Berlin
Cassandras C, Lafortune S (2008) Introduction to discrete event systems, 2nd edn. Springer, New York
Chandy K, Misra J (1989) Parallel program design. Addison-Wesley, Austin
Closse E, Poize M, Pulou J, Sifakis J, Venter P, Weil D, Yovine S (2001) TAXYS: a tool for the development and verification of real-time embedded systems. In: Berry G, Comon H, Finkel A (eds) Computer aided verification (CAV). LNCS, vol 2102. Springer, Paris, pp 391–395
Closse E, Poize M, Pulou J, Venier P, Weil D (2002) SAXO-RT: interpreting Esterel semantics on a sequential execution structure. Electron Notes Theor Comput Sci (ENTCS) 65(5):80–94. Workshop on synchronous languages, applications, and programming (SLAP)
Dill D (1996) The Murphi verification system. In: Alur R, Henzinger T (eds) Computer aided verification (CAV). LNCS, vol 1102. Springer, New Brunswick, pp 390–393
Edwards S (2002) An Esterel compiler for large control-dominated systems. IEEE Trans Comput Aided Des Integr Circuits Syst (T-CAD) 21(2):169–183
Edwards S (2003) Making cyclic circuits acyclic. In: Design automation conference (DAC). ACM, Anaheim, pp 159–162
Edwards S, Kapadia V, Halas M (2004) Compiling Esterel into static discrete-event code. In: Synchronous languages, applications, and programming (SLAP), Barcelona
Gamatie A (2010) Designing embedded systems with the SIGNAL programming language. Springer, New York
Gamatié A, Gautier T, Le Guernic P, Talpin J (2007) Polychronous design of embedded real-time applications. ACM Trans Softw Eng Methodol (TOSEM) 16(2), Article 9. http://dl.acm.org/citation.cfm?id=1217298
Halbwachs N, Maraninchi F (1995) On the symbolic analysis of combinational loops in circuits and synchronous programs. In: Euromicro conference. IEEE Computer Society, Como
Harel D, Naamad A (1996) The STATEMATE semantics of statecharts. ACM Trans Softw Eng Methodol (TOSEM) 5(4):293–333
Howard W (1980) The formulas-as-types notion of construction. In: Seldin J, Hindley J (eds) To H.B. Curry: essays on combinatory logic, lambda-calculus and formalism. Academic, London/New York, pp 479–490
Järvinen H, Kurki-Suonio R (1990) The DisCo language and temporal logic of actions. Technical report 11, Tampere University of Technology, Software Systems Laboratory
Ju L, Huynh B, Chakraborty S, Roychoudhury A (2009) Context-sensitive timing analysis of Esterel programs. In: Design automation conference (DAC). ACM, San Francisco, pp 870–873
Ju L, Khoa Huynh, B., Roychoudhury A, Chakraborty S (2010) Timing analysis of Esterel programs on general purpose multiprocessors. In: Sapatnekar S (ed) Design automation conference (DAC). ACM, Anaheim, pp 48–51
Lamport L (1991) The temporal logic of actions. Technical report 79, Digital Equipment Cooperation
Li YT, Malik S (1999) Performance analysis of real-time embedded software. Kluwer, Boston/Dordrecht
Logothetis G, Schneider K (2003) Exact high level WCET analysis of synchronous programs by symbolic state space exploration. In: Design, automation and test in Europe (DATE). IEEE Computer Society, Munich, pp 10196–10203
Malik S (1993) Analysis of cyclic combinational circuits. In: International conference on computer-aided design (ICCAD). IEEE Computer Society, Santa Clara, pp 618–625.
Malik S (1994) Analysis of cycle combinational circuits. IEEE Trans Comput Aided Des Integr Circuits Syst (T-CAD) 13(7):950–956
Poigné A, Holenderski L (1995) Boolean automata for implementing pure Esterel. Arbeitspapiere 964, GMD, Sankt Augustin
Potop-Butucaru D, de Simone R (2003) Optimizations for faster execution of Esterel programs. In: Formal methods and models for codesign (MEMOCODE). IEEE Computer Society, Mont Saint-Michel, pp 227–236
Potop-Butucaru D, Edwards S, Berry G (2007) Compiling Esterel. Springer, Boston
Rocheteau F, Halbwachs N (1992) Implementing reactive programs on circuits: a hardware implementation of LUSTRE. In: de Bakker J, Huizing C, de Roever WP, Rozenberg G (eds) Real-time: theory in practice. LNCS, vol 600. Springer, Mook, pp 195–208
Rocheteau F, Halbwachs N (1992) Pollux: a Lustre-based hardware design environment. In: Quinton P, Robert Y (eds) Algorithms and parallel VLSI architectures II. Elsevier, Gers, pp 335–346
Schneider K (2000) A verified hardware synthesis for Esterel. In: Rammig F (ed) Distributed and parallel embedded systems (DIPES). Kluwer, Schloß Ehringerfeld, pp 205–214
Schneider K (2001) Embedding imperative synchronous languages in interactive theorem provers. In: Application of concurrency to system design (ACSD). IEEE Computer Society, Newcastle Upon Tyne, pp 143–154
Schneider K (2002) Proving the equivalence of microstep and macrostep semantics. In: Carreño V, Muñoz C, Tahar S (eds) Theorem proving in higher order logics (TPHOL). LNCS, vol 2410. Springer, Hampton, pp 314–331
Schneider K (2009) The synchronous programming language Quartz. Internal report 375, Department of Computer Science, University of Kaiserslautern, Kaiserslautern
Schneider K, Brandt J (2008) Performing causality analysis by bounded model checking. In: Application of concurrency to system design (ACSD). IEEE Computer Society, Xi’an, pp 78–87
Schneider K, Brandt J, Schüle T (2004) Causality analysis of synchronous programs with delayed actions. In: Compilers, architecture, and synthesis for embedded systems (CASES). ACM, Washington, pp 179–189
Schneider K, Brandt J, Schüle T (2004) A verified compiler for synchronous programs with local declarations (proceedings version). In: Synchronous languages, applications, and programming (SLAP), Barcelona
Schneider K, Brandt J, Schüle T (2006) A verified compiler for synchronous programs with local declarations. Electron Notes Theor Comput Sci (ENTCS) 153(4):71–97
Schneider K, Brandt J, Schüle T, Türk T (2005) maximal causality analysis. In: Desel J, Watanabe Y (eds) Application of concurrency to system design (ACSD). IEEE Computer Society, Saint-Malo, pp 106–115
Schneider K, Wenz M (2001) A new method for compiling schizophrenic synchronous programs. In: Compilers, architecture, and synthesis for embedded systems (CASES). ACM, Atlanta, pp 49–58
Schüle T, Schneider K (2004) Abstraction of assembler programs for symbolic worst case execution time analysis. In: Malik S, Fix L, Kahng A (eds) Design automation conference (DAC). ACM, San Diego, pp 107–112
Shiple T (1996) Formal analysis of synchronous circuits. PhD thesis, University of California, Berkeley
Shiple T, Berry G, Touati H (1996) Constructive analysis of cyclic circuits. In: European design automation conference (EDAC). IEEE Computer Society, Paris, pp 328–333
Shiple T, Singhal V, Brayton R, Sangiovanni-Vincentelli A (1996) Analysis of combinational cycles in sequential circuits. In: International symposium on circuits and systems (ISCAS), Atlanta, pp 592–595
Tardieu O, de Simone R (2004) Curing schizophrenia by program rewriting in Esterel. In: Formal methods and models for codesign (MEMOCODE). IEEE Computer Society, San Diego, pp 39–48
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer Science+Business Media Dordrecht
About this entry
Cite this entry
Schneider, K., Brandt, J. (2016). Quartz: A Synchronous Language for Model-Based Design of Reactive Embedded Systems. In: Ha, S., Teich, J. (eds) Handbook of Hardware/Software Codesign. Springer, Dordrecht. https://doi.org/10.1007/978-94-017-7358-4_3-1
Download citation
DOI: https://doi.org/10.1007/978-94-017-7358-4_3-1
Received:
Accepted:
Published:
Publisher Name: Springer, Dordrecht
Print ISBN: 978-94-017-7358-4
Online ISBN: 978-94-017-7358-4
eBook Packages: Springer Reference EngineeringReference Module Computer Science and Engineering