An Introduction to the Esterel Studio Compiler for Constructing
Contents
1. 255 emit Count pre Count 1 amp Warning ESTEREL strleic 0 no main module Warning ESTEREL eiclink 0 found no main module linking root modules Error ESTEREL stn 1 no main module to compile Info ESTEREL esterel exit errors during stn 1 Log Errors Find Dutput Browsing Figure 4 Counter Source Code The reason why warnings and one error occurred is because no main module name as depicted in Figure 3 is provided This is done on purpose to illustrated what will happen if such a main module name is missing Even when main is specified in front of the Keyword module within source code no warnings and errors will be detected while checking the model but simulation compilation will fail with the following message Compilation stopped main module reguired Setting a source file as main module can also be achieved by right click on the desired model Set As Main Module 3 3 Model Generation The subseguent chapter deals with the source code description source compilation as well as source code debugging issues Source Description A textual description of the project plus interface is previously given in chapter 3 2 Now through the use of Esterel Language a much more formal description given in Appendix B should be achieved and explained underneath For a better understand ing about fulfilling the achievable reguirements the counter is illustrated in Figure 5 as a schematics drawin2. Es terel Studio Esterel Studio The integrated development environment after start up Esterel Technologies products uses the FLEXnet license manager from Macrovision Cooperation for product license administration is portrait in Figure 1 Generally there are three different main windows as de scribed in Figure 1 which are identified and highlighted in yellow e_ In the Tree Window project file modules and Safe State Machine are listed Use this window for project management e The Document Window basically serves as a editor to create view and edit Esterel source code Safe State Machine objects and textual documents e Status error output etc messages are displayed inside the Console Window to inform the user with various statements Wa Esterel Studio R et vizmiusummp tE A gt EZ amp D amp S O D Figure 1 Esterel Studio Workspace Extended information about the workspace and its features are presented during the given up down counter example described in the following 3 2 Project Creation Before any new project can be created some specification must be made about what actually should be modelled and later on source code should be generated either for software or hardware with the help of the synchronous programming language Therefore a short verbal specification about the following project is given As a simple project an up down counter should be designed an
3. 27 1 Introduction The purpose of this document is to guickly become familiar with the reactive system design environment Esterel Studio by using the synchronous programming language Esterel Originally Esterel development has been done by Jean Paul Marmorat and Jean Paul Rigault back in 1984 They invented an original information notation to solve their problems by expressing control algorithms in an ordinary and intuitive way Later G rard Berry now Chief Scientist of Esterel Technologies created Es terel s first formal semantics Established on this semantics the first generated Esterel tool was used for during experiments by companies such as AT amp T Bell Labs Das sault Aviation etcetera More about Esterel history can be found on the official Es terel Technologies E02 website 2 Development Environment To be able to construct and run a program designed and generated by Esterel one out of two available software packages must be chosen An short overview of available software is given underneath Name Version Comments Esterel exe v5 92 Most recent free Esterel Compiler Xesterel bat v5 02 Graphical user interface for free Esterel Compiler Xes bat v5 92 Graphical simulation tool for free Esterel Compiler Esterel Studio v5 2 le Integrated Development Environment commercialized Basically two Esterel compiler version are available Readily available is the free downloadable Esterel Version v5_92 This compiler version can b
4. A FACHHOCHSCHULE TECHNIKUM WIEN TECHNICAL REPORT An Introduction to the Esterel Studio Compiler for Constructing Reactive Systems PROJECT DECS DESIGN METHODS FOR EMBEDDED CONTROL SYSTEMS Martin Zauner The project DECS is funded by the FHplus programme of the Austrian Federal Ministries BMVIT and BMBWK and managed by the Austrian Research Agency FFG under grant 811414 Revision History Autor Date Last Changes Zauner 2006 01 12 First draft Zauner 2006 02 08 Document changes for clarification after correction by Roland H ller Table of Contents 1 Introduction 2 Development Environment 2 4 Installation Free Esterel Compiler Esterel Studio Suite 3 Esterel Studio 3 1 Workspace 3 2 Project Creation Interface Project 3 3 Model Generation Source Description Simulation Compilation Simulation Source Code and State Pair Coverage 3 4 Model Verification Verification process 3 5 Code Generation Target Code Testbench ESO Co execution 4 References 10 10 11 12 14 16 17 20 20 20 22 23 5 Appendix A 5 1 COUNTER Source Code Coverage Report 5 2 COUNTER Coverage Report Appendix B 6 1 Counter Source Code 6 2 Counter Source Code including Assertion 6 3 Observer Source Code counter observer strl Appendix C 7 1 Visual Studio Test Bench Output 7 2 Keil Vision 2 Test Bench Output 24 24 25 25 25 25 26 26 26
5. CountinBound I S Counter example scenario Verification engine used Prover SL plug in Figure 15 Project Verification Formulating verification questions depends on the selected properties Basically there are six possibilities to select specific properties e Asserstions e Externel Observers e Output Relations e Outputs e Single Signals e Environment Assertions To add an assertion to the counter example copy the source code under caption Counter Source Code including Assertion from Appendix B to the design Conse quently in the Verification Window under the tab Assertions the specified assertion is listed Check the given assertion with the right click gt Always true to verify if these special logic signal is always true No signal verification can be achieved by right click on the signal Not checked External Observer Within this paper an observer is appended to the system model To make the output of the observer available to the verification session change to External Observers tab right click on the counter observer signal OverUnderFlow Potential questions for observers are shown in Figure 16 18 External Observers Property Observers counter_observer Possibly Present Possibly Absent Not Checked Figure 16 Verify External Observer Output Relations The design represented here does not include Output Relations As soon as Output Relations is part of the design they cover predicate
6. RSS and RPS are explained The given definitions are extracted from E03 as well Reachable State Set An Esterel model execution uses binary registers grouped in a state bit vector to encode the system global state After every tick reaction of the system the global state is reevaluated based on the inputs and the events and the current state bit vector modified accordingly The set of possible bitvector configura tions is called the Reachable States Set RSS Each bit vector configuration in the RSS represents a unique state of the model 15 Reachable Pairs of State Set State enumeration does not test a model completely because it only tests a static view of the model To test a model completely its transitions the capa bility to go from one state to another must also be tested A transition is defined by a start state an end state and an event that makes the transition possible One can decompose the transition into the pair of states start end and the event The theoretical transition number is infinite because no limitation to the event expression capability exists however the possible pair of states cannot be greater than N2 where N is the number of states The set of possible pair of states is called the Reachable Pairs Set RPS To be able to perform such State Pair Coverage configuration must be set accord ingly to Figure 11 More configuration details of State Pair Coverage is presented in E03 Not to forg
7. and Line C Programme Esterel Technologies EsterelStudio bin esterelv7 Lc main COUNTER B counter D D EsterellUpDownCounter Def ault Code ID Esterel UpDownCounter D EsterelUpDownCounter counter strl e cre Com Figure 3 Configuration Properties Make sure in the register card General Compilation Main Module the Esterel main module name is entered In this case the module name is called COUNTER not necessarily case sensitive In the second register card Code Gen select C ANSI as a target language All other registers are untouched at the moment The next step is writing the source code for the counter model and try to check the model in relation to internal correctness and completeness Figure 4 shows the Esterel source code as well as some errors and warning during first model check Vig Esterel Studio counter etp counter strl GD File Edit View Project Simulation Tools Window Help DSE GR lt gt lt mmux oe R BEI YY iE SE R module COUNTER input UD input 5 output Count every do counter etp C3 Model amp S counter strl za COUNTER Extem O Data Observer C Constraint y Configuration else else end if end if end every end module Projec 1 Design Modules bool init true unsigned 2 8 init 0 if UD true then emit Count pre Count 1 sod 256 if pre Count 0 then emit Count pre Count
8. c Esterel bin where a lot of various batch files are accumulated These files are associated with the 4 different executables which are obligatory used while generating C or BLIF files Within these batch files the above mentioned environment variables are set Hence as long as these batch files are utilized Esterel and Tcl TK environment variables will be set correctly In addition to the Esterel compiler which is responsible to generate source code out of the synchronous programming language the utilized compiler e g gcc with re spect to Linux or the pentant c exe for Windows and appropriate linker must be visible in order to instantiate these programs efficiently Due to the fact that Esterel program compilation is executed in the context of a DOS shell correct environment variables for the e g C compiler and linker must be set For the Microsoft Visual Studio compiler cl exe and linker link exe following variables are obligatory e VSINSTALLDIR e PATH e INCLUDE e LIB Correct setting of the above mentioned environment variables are achieved by calling the batch file vsvars32 bat located within the Microsoft development software E g as an example for the Microsoft NET development suite the file can be found in the directory Microsoft Visual Studio Net 2003 Common7 Tools In order to use the Esterel compiler from the DOS box the batch file vsvars32 bat must be called in ad vanced before the compiler ca
9. d implemented in software on the evaluation board Phytec KC167CR Depending on the environment the up down counter should increase decrease its value by one every second and emit the counter value to its environment The range of the counter is given by the formula 2 1 whereby N is 8 bit wide and unsigned Consequently the counter will wrap around at a value of 255 followed by 0 while increasing and again wrap around at a value of 0 followed by 255 during decrease mode The initial counter value is set to 0 Counter should count up when the up down signal is true 1 7 Interface Input Signal UD up down signal corresponding to the counter direction Input Signal S timer interval in seconds Output Signal Count counter value to display Project Before programming a new project must be specified within Esterel Studio This can be attained by click on the menu bar to File New Project Choose a location for your project and name it counter In Figure 2 the created project is visualized CT In the Tree Window the just created counter example is Ele Ect View Project Tb shown There are 6 folders generated whereas meanwhile D GEG 5 only 2 folders will be used These are the Model and Configuration folders Right click on the Model folder will bring up a context menu to add a new file to the folder A pop up window appear Now choose data type Esterel Code strl and store it in a suitable folder and under the file
10. e obtain either via the official Esterel website E02 or by the academic website E01 Additionally to the free compiler version an extensive commercialized Esterel tool set Esterel Stu dio Compiler Verification Kit etc is available from the Esterel Technologies Com pany E02 Also included in the free compiler version is an graphical user interface for the com piler xesterel plus a graphical simulation tool xes constructed on the free devel opment platform Tcl TK More information about Tcl TK can be found in T01 After download and installation of the compiler version v5_92 a full functional none restricted synchronous programming development environment is ready to use 2 1 Installation The installation procedure for the free Esterel version compared to the commercial Esterel Studio is distinctive Within this document the commercialized Esterel Studio Version is recommended because of its simple installation procedure ordinary use and the available support by the manufacturer Nevertheless the free compiler ver sion 5 92 can be utilized to get familiar with synchronous programming of reactive systems without paying any frees Esterel compiler setup is discussed followed by the commercial Esterel Studio version The installation steps described underneath are only given for the Windows OS no installation comments about accomplishment on Linux are supplied by now Free Esterel Compiler The free available software pac
11. e_case Lvhdl XMLstats main COUNTER B counter D D Esterel UpDownCounter Default Code ID Esterel UpDownCounter x ee Figure 17 Code Generation After selecting the desired language code can be generated by choosing Project Gen erate Code A short cut for generating code is also depicted in Figure 7 More useful information about generating embedded software non modular hardware and modu lar hardware is introduced in E03 beginning with page 259 Testbench Esterel Studio can automatically generate executable code which is used for a test bench to deliver a predetermined input sequence into a design to in return observe its response To be able to generate a test bench an ESI scenario file see chapter Source Code and State Pair Coverage must be available as an input file A test bench is composed of the following components e Stimulus generator Generates test inputs to stimulate the design 20 e Checker Checks what outputs are expected for a valid design Figure 18 illustrates the design flow for a test bench and its model usage Externer Simulator Esterel Studio Simulation Figure 18 Test Bench Design Flow As illustrated in Figure 18 simulation and computation as well as test bench genera tion is done in Esterel while the generated code and test bench is used as an input for an external e g HDL simulator such as ModelSim The target language specified for the test bench depends on the Act
12. ect To File Past starting the simulator Esterel monitors the ESO file in order to provided dy namic information on the scenario content like number of step in the scenario and the current step in particular The ESO Co execution can be observed dashed line in Figure 18 which runs from the ESO file to Simulation amp Computation 22 4 References B01 B02 B03 CGPO1 E01 E02 E03 E04 HO1 I01 TO1 G rard Berry The Foundations of Esterel Ecole des Mines de Paris and INRIA Route des Lucioles 2004 http www sop inria fr esterel org home htm G rard Berry The Esterel v5 Language Primer Version v5_91 Centre de Mathematigues Appliguees Ecole des Mines and INRIA Route des Lucioles 2004 http www esterel technologies com G rard Berry The Esterel v5_91 System Manual Centre de Mathematigues Appliguees Ecole des Mines and INRIA Route des Lucioles 2004 Edmund M Clarke Jr Orna Grumberg Doron A Peled Model Cecking Lucent Technologies 1999 ISBN 0 262 03270 8 Esterel org Academic Esterel Homepage Free Download of Esterel pro gram documentation and examples http Www sop inria fr esterel org Esterel Technologies Commercialized Esterel Homepage Additional Es terel Tools and documentation http www esterel technologies com Esterel Studio User Manual Esterel Technologie SA 8 rue Blaise Pascal 78990 Elancourt France Revision ESUM ET 0128u1 ES5 2 h
13. emon strate its utilization The source code is offered in Appendix B After adding the ob server file to the project it must be made available in the Active Configuration within tab Environment Double click on the displayed observer file and finally click apply to activate the observer for the verification process How to design an environment constraint or a observer file see literature E03 Next step in carry out a verification process one out of two verification engines must be specified by activating the cor responding option field in Active Configuration Verification Inside the counter example project the full model checking based on SAT technology more about SAT see I01 is used Information about the two different verification engines and there appropriate usage is discussed in E03 on page 203 as well as in CGP01 Verification process Launching a verification process is done by choosing Project Verify or pressing the toolbar verification button shown in Figure 7 After verification computation is com 17 pleted the following window given in Figure 15 is shown Nofe In order to get the same screen as shown in Figure 15 extend the Esterel source code as exposed in Appendix B capture 6 2 VT Verification of project counter Use the right click button to set inputs and properties to verify in the tabs below Assertions External Observers Outputs Single Signals Environment Settings Log Assertions COUNTER
14. et a previous recorded scenario file this is done either by storing a simulation to a file or by performing a verification must be available The execution is accomplished by pressing Project gt Coverage Analysis from the main menu he Coverage Analysis lt Report created in DXEstereUpDownCounteriDefaulhieportsicoverage Report html C Open generated report Status Done Figure 13 Screen Shot of Coverage Analysis The result of State Pair Coverage is depicted in Figure 13 Moreover a Coverage Report is automatically generated which summarizes the Coverage Analysis in some way An example report can be found in Appendix A 3 4 Model Verification While still in the design phase Esterel Studio allows to detect corner cases which are probably not covered during Simulation Source Code and State Pair Coverage As a result Esterel Studio has a build in design verifier which implements formal verifi cation techniques The reason for such design verifier is that it can be very hard to detect enough input sequences for any reasonable sized design while simulating in order to determinate the expected behavior Esterel Technologies states the need of formal verification techniques by saying Formal property verification is an alternative and complementary approach to functional verification of hardware designs Using mathematical methods it 16 can be proved that a given property of the DUV Device Under Verification can
15. example that the signal S is present active and the condition of UD is true As a result the condition of signal Count is evaluated to true hence Count is emit ted 13 Source Code and State Pair Coverage Before Source Code Coverage can be put into practice a few modifications must be done in the Tree Window under Configuration Thus the default configuration file see Figure 2 can be duplicated after simulation is stopped in order to switch be tween various configurations without doing a lot of modifications and conseguently impede miss configurations Enabling one specific configuration file is done by right click on the file gt Set Active Pi counter Configuration Source Coverage General Code Gen Simson Coverage Verification Environment Dire Selected Scenarios Source Coverage Measure s Da V Compute coverage X md tcenaio eti X sim scenario es E Reached v Unrenchedl Report Name test coverage States Coverage Measure v Sates v Transitions States Complebion Scenario 7 States 7 transitions Sequences Short v Limit Fle Results v Symbok Space Sue Sot Chyorologesi v 1 See Envronmerk tab for additional Cover age settings cx Cem ww Figure 11 Source Code and State Pair Coverage Configuration Source Code Coverage is used to display and obtain statistics about what part of the source code is reachable and finally reached during computation As shown in cover age configura
16. g Up Down UD Value Count I NN Seocnds S Counter Figure 5 Counter schematics Two inputs UD S and one output signal Count coming going from to the environ ment are specified If and only if the value of signal UD is true and the signal S is present the counter will count up In case the value of signal UD is false and the sig nal S is present then the counter will count down In each case as soon as the signal S is available the output signal Count is emitted to the environment When signal S is absent Count will not be emitted to the environment In the beginning UD is ini tialized with true means count up and Count is initialized with zero The declara tion of Count with unsigned lt 2 8 gt equals 25 which signifies that only 256 positive values are allowed Therefore unsigned lt 2 8 gt presents all the natural numbers for 0 to 255 not the set of number one can write with 256 bits which is un signed lt 2 256 gt 10 The every statement a simple delay expression is a Boolean test The delay expres sion then elapses at the first instant in the strict future where the test is true The emit statement is an emission of the valued signal Count Depending on UD or the valued signal Count itself the instantaneous Count value is emitted to the environment The pre Count data expression reads the value at the previous instant of Count The previous value is defined at the first ins
17. ic report generation is included Advance and more precise information can be obtained from E03 11 Simulation Starting a project simulation at the first time without previously building the stand alone simulator the simulation will run through the complete compilation procedure first before starting the simulator Past successful compilation the simulator looks like exemplified in Figure 8 Wi Esterel Studio counter etp Ele Edi View Inset Format Project Simulation Tools Window Help DEREN lt gt gt mamx oc R tevzsssem R 9 COUNTER 5 fl COUNTERGCOUNTER module COUNTER 8 input UD bool init true UD boo z input D sone output Count unsignedc2 8 init O D Count unsigned 8p Detrue then emit Count pre Count 1 mod 256 1s else if pre Count 0 then emit Count pre Count 255 el se emit Count pre Count 1 nd if Type unsigned lt 8 gt EI p Input nest E User npa Watch 1 Figure 8 Esterel Simulator The environment interface is clarified within the Tree Window The input UD S and the output Count is shown The bottom of Figure 8 reveals two additional win dows surrounded in red named Simulation Control and Simulation Observation In the control section all inputs and within observation section all outputs are listed The tabs in the control and the observation panel can be used to sort signals Simula tion is started through the T
18. ick button Signal colors can be either red or blue Blue means the signal is absent and can thus not be emitted in the next Tick whereas red indicates that a signal is present and will be emitted with the next Tick This corre sponds to the Pure and likewise to the Valued Signal type Additionally to the Pure Signal a value must be specified while using Valued Signal types An example is given in Figure 8 which is the UD signal This signal carries a Boolean value there fore TRUE or FALSE can be specified To change the status of any signal left mouse click on the signal or right mouse context menu Emit Should the signal be emit ted over a period of Ticks the user can specify this by using the context menu gt Keep Input Furthermore the input and output signals can be visualized as a timing diagram by selecting Simulation View Session Waveform 12 GTKWave Cex File Edt Traces Time Markers View Qa amp amp iesi e OB sw is es From 0 s To 20 ns Marker Cursor 0s Signals Time clk UD UD data S Count Count data 7 0 RT Figure 9 Session Waveform The waveform window is presented in Figure 9 All input and output signals can be listed and altered in many ways As the user progresses through the simulation ele ments of the Esterel language are highlighted both in the Tree and Document Window Breakpoints transitions halt points and signals the user wants to locate are h
19. ighlighted in following colors Color Description Red Activated halt point for a state or emitted signal for a transition Green Transition active i e trigger is present and condition is true Pink Signal with an unknown status emitted or not emitted Gray Breakpoint Oran ge Signal highlighted with View Bindings Yellow Suspended Table 1 Simulation Color Definition Such a highlighted example is pictured in Figure 10 In the Tree Document and Simulation Control Window some elements are highlighted in orange to symbolize View Bindings Count signal is emitted and therefore colored in red within Simula tion Observation Window The input signal S is also colored in red and additionally underlined which indicates that the signal keeps its value for further Ticks Li z COUNTER T amp COUNTER COUNTER module COUNTER Interface input UD bool init true E UD bool E input B 5 pue output Count unsigned lt 2 8 gt init 0 s do P if UDetrue then emit Count pre Count 1 mod 256 D Count unsigned lt 8 gt Project Design Modules Tick Ree 2 amp HX HB N _ Name Value i Type _ ele amp Name Value Type Bub tue bool o D Count 18 unsigned 8 ps D c 2 5 9 2 c s ED Input next E User input Watch 1 DD ouput ED ieu AI Watch 2 Figure 10 Simulation Highlight All elements colored in green inside the Document Window signifies in case of the counter
20. io Test Bench Output T contes tesitesch Microsoft Visual C Unterbrechung countar COUNTER thc Datei Bewbeten dnde projit Erstellen Debupgen Eras Fede Hffe u x gg tee p y Debug gp COUP O Court 3E323 Abe RR L2 HR sa 92303 m Be counter COUNTER the x Propitmagpen pore court 9 X J rc IL mt Expected Value 4 gt O cownter testbench D Besson Cwr bignum and strimgs delete 26 72 Keil Vision 2 Test Bench Output WP counter_testbench pVision2 D Esterel WpDownCounterWefault Keil counter_COUNTER_tb c E Ble Edt yw Project Debug Peripherals Tools SVCS Window Heb Jasmdaeme oc 4722 RE Ja 2 6 Q mm Sere amp HOBP Po gt Be ARISODE jSASiYA3Y AA 4 3 4 3 3 31 0 3 33 3 CLK cycle number 7 YYTRXYTXYYYYYYYTTNIYYTY Y YTY COUNTER I S Reinitialize Real Outputs COUNTER run Dump CAC expected outputs COUNTER 0 Count Expected Status true COUNTER 0 Count Expected Value 5 CycleAccuracyCheck Reinitialize Expected Outputs LCD Modul Count value 5 ASM ASSIGN BreakDisable BreakEnable 27
21. ive Configuration settings configured under the Code Gen tag hence test bench generation for target language such as C or C is supported too For the given counter model test benches used for ModelSim VHDL Visual Studio ANSI C and Keil u Vision 2 ANSI C were created Figure 19 presents the Esterel simulation waveform outcome upper part of Figure 19 which is compared with the external simulation waveform produced by ModelSim lower part of Figure 19 Example test bench outputs generated by Visual Studio and Keil u Vision 2 development environment are presented in Appendix C Figure 19 Esterel vs ModelSim Waveform 21 ESO Co execution During the external simulation session in ModelSim and the ability of Esterel Studio to instrument HDL code and write ESO Esterel Simulator Output files the per formed external simulation session can be visualized within the Esterel model whereas the simulation control is still handled by the external simulator Co execution is done by activating Signal Record Instrumentation within Active Con figuration Code Gen After HDL source code and test bench generation the model must be simulated in the external simulator Right after the simulator is started an xxxxx eso file is created where all dynamic inputs and outputs are written to Be fore continuing with the external simulation an Esterel simulation must be started and the just created ESO dump file must be loaded Simulation Conn
22. kage downloaded see B02 contains a Self Extractor WinZip file After double click the executable file the user will be prompted to choose a temporarily location where to unpack the compressed file for further installation The executable suggests c Temp Esterel In case the folder c Temp does not exist the WinZip programme will create one If another folder for unpacking the self extractor file is chosen no c Temp folder will be created But in order to be able to use the compiler Esterel compulsorily needs a folder named c Temp to store all the intermediate compiled files which are needed during the compile and build process Hence as long as a c Temp folder is available on the computer system no problems will arise during compilation procedure Environment Variables Translating Esterel soures files into a seguential programming language such as C or even into a Berkely Logic Interchange Format BLIF from which a conversion to a hardware description language like VHDL or Verilog is possible additional convert ers are needed all compulsory environment variables must be set accordingly Fol lowing variable is mandatory for the functional correctness of the compiler e ESTEREL As soon as the graphical debugger xes or the graphical user interface xesterel shall be used the variables underneath are mandatory as well e 9o TCL LIBRARY 46 e 9oTK LIBRARY 40 In general the program folder for Esterel contains a folder named
23. ment variable ESTERELD LICENSE FILE to lt PortNumber gt lt Server gt 1 1 lt PortNumber gt is the free TCP port number specified in the license file 1 2 Server is the name of the computer where the FLEXnet License Server is installed Inside Technikum Wien the lt PortNumber gt is set to 29030 and the Server name is given as embsyslic Hence the variable ESTERELD LICENSE FILE must have the value 29030 embsyslic Furthermore the server name embsyslic must be specified inside the hosts file locate in Microsoft Windows OS under the path C WINDOWS system32 drivers etc Following line must be added to this file e 10 128 202 250 embsyslic embsyslic After successful setup the development suite Esterel Studio can be utilized 3 Esterel Studio This chapter gives an overview of how the Esterel workspace is divided and in what way the integrated development environment can be used to design verify and gen erate code for Reactive Systems The basic integrated menus and tools are explained in the light of the up down counter example in the remainder of this document For a comprehensive list of menus and tools about Esterel Studio refer to the User Manual E03 The command line version for the free Esterel compiler is not part of this document This information can be obtained be reading literature B03 3 1 Workspace Esterel Studio can be started by click on the appropriate link Start gt Program gt
24. n be executed Make sure you always call the batch file as soon as anew DOS box is in use Esterel Studio Suite A much more convenient way concerning the installation procedure as well as Es terel project management can be found in the commercialized version of Esterel known as Esterel Studio This version is not free but as a academic institution spe cial programs are offered to obtain Esterel Studio including SCADE a graphical version of LUSTRE for one year free After the expiration date a license renewal is possible Before Esterel Studio can be installed make sure a Microsoft Development Studio is properly set up At least Microsoft Visual Studio 6 plus Service Pack 3 must be available in order to use Esterel Studio Simulator To start the installing procedure just insert the CD and run es_setup exe Be aware in case of a previous installation of the free Esterel compiler that the environment vari able ESTEREL will be overwritten due to the Esterel Studio setup and therefore can only be used for the new development environment Changing it back can be accom plished only by hand and can cause some disturbances in case of wrong settings within correct behaviour of the Esterel compilers Environment Variables Basically a Licences Server for Esterel Studio and SCADE is running within the Technikum Wien Campus Using the Esterel Studio the License Server must be reachable This can be achieved be setting the local environ
25. name counter Right after storing the file will be visible in the Tree Window under the folder Model In the Document Window a empty file is shown This is the Esterel source code document Additional under Configuration folder an already defined configuration file Default is available Figure 2 Project Tree In the Console Window a log message is displayed that the project counter etp is loaded Furthermore the default configuration file must be altered in order to simu late and compile the source code In the first step no verification are applied on the model Next double click on the configuration file Defaulf and the following win dow as depicted in Figure 3 will be opened counter Configuration Default General Code Gen Simulation Coverage Verification Environment Dire Project Language Esterel V7 Compilation Basename counter Main Module C Compilation Options for Simulation Additional Include Directories Additional Compiler Options 7 Compile simulator with debug info Description Coc Lees Le x Ei counter Configuration Default Target Language Compilation Type Expanded Mode Variables static allocation Authorize shared variables Signal record instrumentation C ANSI Sorted Equations 7 Verbose mode C Do not generate code C Static size check Warnings Normal Optimization None Advanced Options Code Gen Simulation Code Gen Specific Comm
26. not possibly be violated by any input seguence The method implemented by the Design Verifier is known as Model Checking In model checking all behav iors that could potentially lead to the violation of a given property are exhaus tively examined If no such behaviors can be found the property is proved cor rect On the other hand if there is a behaviors that violates the property the model checking procedure generates a counter example that is an input se guence demonstrating the violation of the property This statement was taken form E03 on page 196 Descent information about model checking and its advantages are introduced in CGPO1 The generated counter example can be used as an input scenario for the simulator to facilitate the investiga tion of the violation Two possibilities are available to form a more precise environment activity if needed when verifying a model Such possibilities are available as environment constraints file and observer files These files can be written either in Safe State Machine scg or Esterel strl format Depending on the file which is created in the Tree Window click right on Observer or Constraint folder and add a new file as illustrated in Figure 14 KE Observer a Insert File Folder 383 Insert Current Document Expand All Subfolders Collapse All Subfolders Check Figure 14 Add Observer File During verification within the counter example an observer file is used to d
27. optimi State COUNTER K100 Tel whether the program is stlacte 5 2 COUNTER Coverage Report Completion Scenario File D Esterel UpDownCounter Default Simulation Scenarios simul_scenario_3 esi Files are CHRONOLOGICALLY sorted nien prp gt gt gt sm enao 2 gt gt 2 Generated on 01 04 2006 15 38 15 by Esterel Studio 5 2 1e build i10 6 Appendix B 6 1 Counter Source Code module COUNTER input UD bool init true input S output Count unsigned lt 2 8 gt init 0 every S do if UD true then emit Count pre Count 1 mod 256 else if pre Count 0 then emit Count pre Count 255 else emit Count pre Count 1 end if end if end every end module 6 2 Counter Source Code including Assertion module COUNTER input UD bool init true input S 25 output Count unsigned lt 2 8 gt init 0 every S do if UD true then emit Count pre Count 1 mod 256 else if pre Count 0 then emit Count pre Count 255 else emit Count pre Count 1 end if end if end every ll assertion section sustain assert CountInBound Count gt 0 and Count lt 255 end module 6 3 Observer Source Code counter _observer strl module COUNTERCONSTRAINT input Count unsigned lt 2 8 gt init 0 input S output OverUnderFlow every S do if Count lt 0 then emit OverUnderFlow end if end every end module 7 Appendix C 7 1 Visual Stud
28. s on output which must always hold Further information are exposed by E04 on page 73 Model Outputs In order to check the model output if they are possibly present or absent during veri fication go to the Output tab and select the corresponding output signal Right click to select the condition of an output s status Single Signal Emission If two and more emissions of the same incarnation of a single valued signal is per formed a run time error is produced To detect the presence of such multiple emis sions go to the Single Signals tab right click on the signal choose Always Signal Emission Environment The environment tab contains two fields labeled as Model Inputs and Environment Constraints Use the labeled field Model Inputs to directly constrain the offered in puts to either Always Present or Always Absent Additionally if a constraint file ex ists this can be seen under the second labeled field named Environment No selection can be made in this panel Settings and Log As described earlier in this paragraph under tab Sertings one out of two verification engines can be chosen Within the Log tab information produced during verification process are displayed At the bottom of the Log tab verification results are revealed after clicking the verify button In the Results panel the type of property e g Assertion Output etc the prop erty name as well as the status e g Always True Always Single Emis
29. sion etc is published Additionally in case a formulated guestion evaluates to e g Possibly ab sent Potential multiply emission etc a counter example is produce to lead to the possible misbehavior of the model By double clicking on the generated counter ex 19 ample a simulation can be started in order to follow the path which directly escort the model designer to the possibly fault behavior In depth information are presented in E03 chapter Formal Property Verification 3 5 Code Generation This chapter deals with the target dependable code generation as well as test bench generation Only basic issues are covered detailed information are found in E03 Target Code Past a successful model generation and verification embedded code generation can be carried out Thus the corresponding target language must be selected in the Active Configuration under tab Code Gen Esterel supports different target languages such as ANSI C C VHDL Verilog only to mention a few An illustration about differ ent types of target languages is also given in Figure 17 Target Language Compilation Type C Expanded Mode Authorize shared variables Modular VHOL Signal record instrumentatiq Verification Code Logical Circuit BLIF No 3 Warnings Optimization Advanced Options Code Gen Simulation Code Gen Specific Command Line C Programme Esterel TechnologieslEsterelStudiolbinlesterelv7 strleic ignor
30. source code purple has al ready been reached while other parts of the source code blue are not yet been reached Finally after the simulation has ended the source coverage must be stopped Conseguently the Source Code Coverage Report can be saved to a location provided by the user A possible coverage report for the introduced model in this paper is pre sented in Appendix A More detailed source coverage information can be extracted form E03 In addition State Pair Coverage can be applied in order to ensure that all possible states RSS Reachable State Set and transitions RPS Reachable Pairs of states Set have been attained The importance of State Pair Coverage is underlined by the following statement When you measure and complete coverage you test the global state machine GSM of your system or a flattened version of your system where each state is a combination of all states of the system components That is you test all possible combinations of states and transitions not just the ones in a single automaton or a collection of sequential components in a Safe State Machine A model is considered to be completely tested when the set of simulation scenar ios used to test the model the Global State Machine have reached all states in the Reachable State Set RSS or the Reachable Pairs Set RPS which was taken from the Esterel User Manual given in E03 on page 220 Subse quently for a better understanding the term
31. tant that follows the value definition If the signal has an initial value it is also the initial value of pre Count More details about Esterel language definition can be found in E04 Simulation Compilation Before the source code written in Esterel will be compiled a check of the generated model should be performed in order to satisfy all rules like static cycles etc asso ciated with the synchronous programming language Esterel An overview where the most important properties of Synchronous Programming of Reactive Systems are discussed can be found in H01 In Esterel such a check can be activated by pressing the button circled in red in Figure 6 v d EIS Check model F4 Figure 6 Toolbar Check Model Funktion In case of an error a message is printed in the Console Window otherwise in the Log register the message Syntax analysis successful can be obtained After a suc cessful model check the project can be compiled to a so called Standalone Simula tion Build Standalone Generate Verification Simulator Testbench ezrek seas ve Simulation Coverage Analysis Generate Code Figure 7 Toolbar Description For that reason the red button exclamation mark illustrated in Figure 7 must be pressed in order to build and start the simulation There are buttons available for cov erage analysis source code as well as test bench generation and a button for model verification Additionally an automat
32. tion see Figure 11 the appropriate checkboxes under Source Coverage Measure must be activated in order to perform coverage analysis Additionally turn on corresponding simulation scenario by activating the recorded simulation file un der the region Selected Scenarios in Figure 11 If no scenario file is available a model simulation must be performed see chapter Simulation in order to save the simulation as a scenario file This is simple done by just saving the performed simu lation to a file For a better visibility to highlight reached unattained or dead source code following text coloring are used throughout Source Code Coverage e Grey Dead code not reachable e Blue Reachable code that has not yet been reached e Purple Code successfully reached at completion of computation Starting Source Code Coverage while performing e g a recorded simulation is done by pressing the Start Source Coverage button in the Simulation Coverage toolbar or through the main menu Simulation Start Source Coverage An example source coverage analysis is presented in Figure 12 14 COUNTER module COUNTER input UD bool init true input 3 output unsigned lt 2 8 gt init 0 if 2UD true Un ENS DENNIS 1 mod 256 else if pre Count 0 then emit Count pre Count 255 else emit Count pre Count l Figure 12 Highlighted Coverage Source Code Here in Figure 12 it is obvious that some portion of the
33. ttp www esterel technologies com Esterel Studio Language Reference Manual Esterel Technologie SA 8 rue Blaise Pascal 78990 Elancourt France http www esterel technologies com Nicolas Halbwachs Synchronous Programming of Reactive Systems A Tutorial and Commented Bibliography Verimag Grenoble France Internet The International Conferences on Theory and Applications of Satisfiability Testing SAT http www satisfiability org Tcl TK Tcl Developer Xchange Tool Command Language http www tcl tk ET 5 Appendix A 5 1 COUNTER Source Code Coverage Report Generated on 12 29 2005 10 43 07 by Esterel Studio 5 2 1e build i10 List of scenarios files mind Number of manually played ticks 0 Total number of ticks played 9 Reached statements Ma ns cca dic dccus icc every UNTER 1234567 2 3 4 5 6 7 8 9 9 if 2 3 4 5 6 7 8 9 m emt s COUNTER 555 00 0 0 prso 0 Comw preCCowo J7__ 10____ COUNTER _ 5 0 55 000000 A789 on ge s s counter p 00 jJ ft 5 0 io L j COUNTER p B ft 8 00 00 en p jJcouvrR p Su le emt fi 5 couNTER fpf 6 Countgpre Couny 10 io couNTER p fi 0 0 0 0 pe ur couNTBR p 0 go ST pmi f 2 s counter p h ST Countpre Coun 12 io couNTER po 0 p 00000000 45 Reached SSM objects SSM object net explanations zd n I e Or gate that bears selection incompatibility information used for verification and
Download Pdf Manuals
Related Search