Contents |
Esterel is a formal synchronous language for the unambiguous specification and correct-by-construction either hardware or software implementation of reactive systems, with particular focus on embedded systems. Esterel was initially developed in Academia, in strong cooperation with industrial users. The current Esterel v7 language version to be standardized has been developed within the Esterel Consortium, evolving from the previous Esterel v5 academic version by adding new features necessary for hardware design. Esterel v7 is based on a reactive kernel composed of a dozen primitive constructs whose semantics has been formally defined. Esterel programs can be fully and faithfully translated to hardware circuit descriptions written in standard HDLs (hardware description languages) or to equivalent software code (C, C++, SystemC), with the very same behavior in both cases. Esterel v7 natively supports verification assertions, and Esterel v7 programs can also be translated to input for formal verification systems such as model-checkers, in such a way that verified properties are guaranteed to equally hold on hardware and software implementations.
The proposed project will create an IEEE standard based on the existing Esterel v7 language, ensuring unambiguous definition of the language syntax and semantics, and, therefore, full interoperability between Esterel-based compilation, circuit synthesis, static analysis, and verification tools. The output of the project will be the standard Esterel v7 Language Reference Manual.
[edit]The purpose of this project is to provide the EDA, semiconductor, systems design, and software communities with a well-defined and official IEEE definition of the Esterel v7 language. This is needed because Esterel v7 is not a minor variant of existing HDLs or software languages that could be defined with an addendum to existing standards. Esterel v7 is unique in its way to formally merge the kind of sequencing only found in software languages, the kind of large-scale synchronous concurrency found in hardware description languages, specific temporal control primitives that drive the life and death of activities, and full support for multiclock designs. For datapath specification, Esterel v7 supports formally defined arbitrary precision exact arithmetic, bitvectors with conversion from and to numbers according to predefined or user-defined numerical encodings, and arrays of arbitrary dimensions and types. The integration of these features provides the user with a much higher level of abstraction than with current languages that support only a few of them at a time. Experience has shown that Esterel v7 designs can be 3 to 5 times smaller than HDL or C designs, while being much easier to develop, verify, and communicate.
Esterel v7 is interoperable with other standards since it can generate synthesizable HDL code (Verilog, VHDL, etc.) as well as executable software code (C, C++, SystemC, etc.), The fact that equivalent hardware and software targets can be obtained from a single source increases confidence in hardware simulation by software means, and helps delaying choices between hardware and software final implementations.
The key technical objective is to stabilize and fully define the syntax and semantics of the language. Because of the considerable amount of previous scientific work in the field, there is no doubt that this objective can be achieved in a rigorous way, thus providing a fully solid basis for users as well as tool builders, and ensuring full interoperability between tools of diverse origins.
Esterel is a formal synchronous language for the unambiguous specification and implementation of hardware and software embedded systems. Esterel was initially developed in Academia, in strong cooperation with industrial users. The current Esterel v7 language version to be standardized has been developed within the Esterel Consortium, evolving from the previous Esterel v5 academic version by adding new features necessary for hardware design. Because of the formal character of the language kernel semantics, Esterel programs can be fully and faithfully translated to hardware circuit descriptions written in standard HDLs (hardware description languages) or to equivalent software programs, with the very same behavior in both cases. Esterel programs can also be translated to input for formal verification systems such as model-checkers, in such a way that verified properties are guaranteed to equally hold on hardware and software implementations.
The proposed project will create an initial IEEE standard based on the existing Esterel v7 language, ensuring unambiguous definition of the language syntax and semantics, and, therefore, full interoperability between Esterel-based compilation, circuit synthesis, static analysis, and verification tools. The output of the project will be the standard Esterel Language Reference Manual.
[edit]The purpose of this project is to provide the EDA, Semiconductor, and System Design communities with a well-defined and official IEEE definition of the Esterel language. This is needed because Esterel is not a minor variant of existing languages that could be defined with an addendum to existing standards. Esterel is unique in its way to formally merge the kind of sequencing only found in software languages, the kind of single-clock or multiclock concurrency found in hardware description languages, and unique temporal primitives that drive the life and death of activities within programs and simplify behavior specification. Esterel also support formal definition of datapath based on arbitrary precision exact arithmetic, bitvectors with conversion to number according to predefined or user-definable number representation, and arrays of arbitrary dimensions and types. These language primitives facilitate the expression of complex behavior by at least one order of magnitude, providing the user with unmatched clarity and productivity for specification, design, and verification activities. The fact that equivalent hardware and software targets can be obtained from a single source increases confidence in hardware simulation by software means, and makes it possible to perform late choices between hardware and software final implementation.
The key technical objective is to stabilize and fully define the syntax and semantics of the language. The technical aspects to be scrutinized concern the various sorts of signals used in Esterel programs, the datapath arbitrary precision and exact arithmetic features, and the temporal statements particular to Esterel that control the life and death of statements and signals. Because of the considerable amount of previous scientific work in the field, there is no doubt that all the involved questions can be solved in a completely rigorous way, thus providing a fully solid basis for users as well as tool builders, and ensuring full interoperability between tools of diverse origins. A derived objective is to ensure that a given Esterel design can be effectively compiled to other standardized languages such as VHDL, Verilog, SystemVerilog, C, and SystemC, with the same guaranteed behavior for all these different targets. This requires to check that all Esterel constructs are synthesizable in hardware or software, up to well-identified limitations of back-end synthesis or compilation tools.
Retrieved from "http://monster/mwiki/index.php/Esterel_v7_Standardization_PAR"