Synchronous Languages and System Design with Esterel Ellen Sentovich Cadence Berkeley Laboratories Outline Context Reactive Systems Principles Synchronous languages Esterel in depth Language Compilation Causality Optimization and Verification New applications ECL Implementing Esterel on CFSM networks System Design Systems produce a steady sequence of input output sequences Inconvenient to specify sequences need models and languages Model Simple and intuitive Accurate enough model of physical reality Mathematically efficient General enough to allow different implementation styles Language Accurate expression of the model Convenient and efficient expression of the design Analysis Implementation compilation to hardware software Reactive Systems signals signals control data sensors values Esterel Statecharts Argos EsterelStudio Lustre SCADE Signal Applications Software and hardware controllers process control embedded systems datapath control Communication Protocols software protocols bus interfaces cache coherence Drivers man machine interface systems drivers pipeline logic Concurrency Determinism Reactive System Characteristics Reactivity continually react at a speed determined by the environment Concurrency at least between system and environment Strict time and reliability requirements Deterministic Mixed hardware software implementations Synchronous Systems Cycle based read inputs compute reaction produce outputs Synchronous within the same cycle at the same time 0 delay must be checked on implementation Synchronous control propagation signal broadcasting Equivalent FSM implementation good analysis techniques Synchronous Languages Invented for the design of reactive kernels not the interactive interface or data management Programmer views system as an instantaneous reactor to events Program behavior is completely deterministic Attempt to resolve concurrency and nondeterminism in other models Esterel Background Esterel is one of a set of synchronous languages developed in France Esterel reactive control Lustre Signal data flow Argos SyncCharts graphical Esterel development goal natural expression of control Specific statements to deal with time preemption Departure from concurrency as interleaving and rendez vous to concurrency as instantaneous propagation of control Esterel Background Synchronous programming environment Language For control dominated reactive systems Constructs for sequencing concurrency preemption Compiler Produces sorted Boolean equations Causality checking symbolic debugging verification Implementation as C code or digital circuits Esterel Basic Principles Synchronous hypothesis instantaneous communication Communication via broadcast signals event signals sensors variables pure valued Boolean and arithmetic operators Modularity program collection of modules Concise programs write things once Concurrency sequencing preemption Well defined semantics Overview of Syntax Signal reading writing emit S emit S value present S then p else q Basic control and looping halt loop p end run module Sequencing concurrency p q p q Preemption suspend p when S abort p when S weak abort when S abort when immediate S Syntax await statement Most basic signal control statement await S Equivalent to abort loop halt end when S Note Await always stops consider await S await S versus await immediate S await immediate S Variables and Ordering Variable manipulation local V value if V value then p else q Variable computations ordered V V Y emit 5 V 1 V S V Signal emissions communication unordered Legal emit S emit S Illegal emit S 3 emit S 5 non deterministic Signal computations ordered Well defined emit S present S Undefined present S then emit S The ABRO Example Wait until both A and B have occurred then output O unless the reset R occurs R A R B R AB O B 0 A O Number of states is exponential in inputs The ABRO Example in Esterel Wait until both A and B concurrency Unless R preemption loop abort await A await B emit O when R end Write things ONCE Code size is linear in inputs efficient circuit Compilation Esterel program extended finite state machine finite inputs deterministic reaction finite program FSM data computations Can be compiled to a single automata EXPENSIVE exhaustive exploration of set of control states Esterel v3 Can be translated to sorted Boolean equations Esterel v5 State machine is represented implicitly Translation to Boolean Circuits Structural translation Network of interconnected cells Implementation of control control signal runs through the circuit boot signal latch initially 1 thereafter 0 Each cell contains signal input output control input output suspend kill resume signals return codes nested preemption One register per halting statement Translation to Boolean Circuits present S then p else q control for q S control control for p control Causality Cycles occur naturally in Esterel specifications Cyclic dependency between variables Some are harmful some not The Causality Problem is analyzing these cycles and deciding which to accept It is related to analyzing hardware in circuits Combinational cycles How do we define a causally correct program We want a unique comprehensible solution All present signals must be emitted somewhere A solution is a set of consistent assignments to all signals Need to be able to express program in a non cyclic way Constructive causality Harmful Cycles No Boolean solution non reactive or several solutions non deterministic Electrically unstable Useless X X X present X then emit X end X X not X present X else emit X end Harmless Cycles Unique Boolean solution Electrical stabilization in bounded time behaves as if acyclic Natural in Esterel programming Natural in high level hardware synthesis Possible exponential saving in space X I Y present I then present X then emit Y end else present Y then emit X end end I X J Y X I and not Y Y J and not X OK unless I J 1 Combinational Cycles in Sequential Circuits 1 X 0 Y The non constructive state 1 1 is unreachable reachability analysis needed Naturally occurring harmless cycles Operator sharing S Malik Y if C then G F X else F G X C 1 0 F C 0 1 X 1 0 C G Y Causality A Real Example Bus arbitration GrantOut TokenOut T ReqIn TokenOut GrantOut Cell n ReqIn TokenIn GrantIn TokenOut GrantOut AckOut AckOut Cell 1 ReqIn TokenIn GrantIn TokenIn GrantIn AckOut Strange Cycles Unique Boolean solution But electrically unstable Electricity Boolean calculus X X Y X and not Y X X 0 X 1 Y Want to build a
View Full Document
Unlocking...