Synchronous Methodology for Hardware,
Software, and Mixed Embedded Systems
Part 1: the Synchronous Model
Gérard Berry
Chief Scientist
www.esterel-technologies.com
[email protected]
© Esterel Technologies, 2003
G. Berry, VLSI'2004 synchronous tutorial, 1 - 1
The Synchronous Model
• Born in the mid 80's (Esterel, Lustre, Signal)
• Industrial since the mid 90's
• Dedicated to embedded systems
• Embedded software: avionics, automobile
• Hardware: control-intensive circuits, SoC verification
• Versatile cycle-based computation model
clock cycle, bus cycle, transaction cycle, sampling cycle
• Efficient implementation / verification
original Esterel, Lustre Signal
GMD, Synopsys, Karlsruhe (Quartz), Columbia University
© Esterel Technologies, 2003
G. Berry, VLSI'2004 synchronous tutorial, 1 - 2
Global Agenda
Part 1 : Synchrony for embedded languages
Part 2 : The Esterel language
Part 3 : Semantics, synthesis, optimization
Part 4 : Verification, test generation
Demos
© Esterel Technologies, 2003
G. Berry, VLSI'2004 synchronous tutorial, 1 - 3
Agenda - Part 1
Synchrony for Embedded Systems
• Embedded systems and correctness issues
• The three models of concurrency
• The synchronous model : data and control
• The synchronous design flows
• Current applications and envisioned extensions
© Esterel Technologies, 2003
G. Berry, VLSI'2004 synchronous tutorial, 1 - 4
Agenda - Part 1
Synchrony for Embedded Systems
• Embedded systems and correctness issues
• The three models of concurrency
• The synchronous model : data and control
• The synchronous design flows
• Current applications and envisioned extensions
© Esterel Technologies, 2003
G. Berry, VLSI'2004 synchronous tutorial, 1 - 5
Embedded Systems
• computers -> embedded and networked SoCs
• complete change in device interaction
• growing number of critical applications
airplanes, automobiles, medical devices, robot surgeon
smart cards, electronic wallets
© Esterel Technologies, 2003
G. Berry, VLSI'2004 synchronous tutorial, 1 - 6
Automatic
toll
Air Con
Radio
Light control
Alarm detection
Panel
Engine control
Sleep
detector
GPS
Gearbox
Airbags
Clutch
Direction
Radar
ABS
Supension
Global Coordination
© Esterel Technologies, 2003
G. Berry, VLSI'2004 synchronous tutorial, 1 - 7
Embedded Systems on Chip
• Many processing units
• Large embedded software
CPU
DSP
RAM
ROM
GLU
FPGA
Hardware or Software?
© Esterel Technologies, 2003
G. Berry, VLSI'2004 synchronous tutorial, 1 - 8
Embedded Systems Issues
• Direct cost
hardware cost (consumer, automobile, etc.)
development cost
verification cost
• User aspects
functionality and ergonomics
usage cost: power (batteries)
• Correctness issues
central for users
potential business killer
certification constraints
=> high indirect cost
© Esterel Technologies, 2003
G. Berry, VLSI'2004 synchronous tutorial, 1 - 9
Ennemy number 1 : the bug
• Therac 25 : lethal irradiations
• Dharan's Patriot
• Ariane V
• Mars explorers
• High-end automobile problems
• Pentium, SMP cpu networks
• Telephone and camera bugs
Bugs grow faster than Moore's law!
© Esterel Technologies, 2003
G. Berry, VLSI'2004 synchronous tutorial, 1 - 10
As soon as we started programming, we found to our surprise
that it wasn’t as easy to get programs right as we had thought.
Debugging had to be discovered.
I can remember the exact instant when I realized that a large
part of my life from then on was going to be spent in finding
mistakes in my own programs.
Maurice Wilkes, 1949
© Esterel Technologies, 2003
G. Berry, VLSI'2004 synchronous tutorial, 1 - 11
How to avoid or control bugs?
• Traditional : better verification by fancier simulation
• Next step : better design
better and more reusable specifications
simpler computation models, formalisms, semantics
reduce architect / designer distance
reduce hardware / software distance
• Better tooling
higher-level synthesis
formal property verification / program equivalence
certified libraries
© Esterel Technologies, 2003
G. Berry, VLSI'2004 synchronous tutorial, 1 - 12
Classical computation models
are inadequate
• Turing complete => too powerful, too hard to verify
• No need for fancy dynamic memory allocation
• Concurrency is mandatory, but too difficult (e.g. threads)
• Determinism is mandatory, but contradicts concurrency
• Implementation of classical control theory not obvious
• Inadapted to circuit design
© Esterel Technologies, 2003
G. Berry, VLSI'2004 synchronous tutorial, 1 - 13
There are much simpler models !
Asynchronous data-flow: Kahn Networks, Ptolemy
simple, easy concurrency, nice semantics
widely used in multimedia devices
data-deterministic, but no support for distributed control
Domain-specific synchronous languages
simple, easy concurrency, nice semantics
determinism, distributed control
same source code compiled to hardware or software
Direct match with embedded systems foundations
control engineering : sampling theory, automata theory
circuit design : RTL logic, transactional modeling
© Esterel Technologies, 2003
G. Berry, VLSI'2004 synchronous tutorial, 1 - 14
Synchronous languages
• Started in the 80's
ESTEREL : Ecole des Mines / INRIA, SyncCharts : Un. Nice
LUSTRE : IMAG, SIGNAL : INRIA Rennes
SAO : Aerospatiale -> Airbus, Gala : Thalès
Reactive C : Ecole des Mines, TCCP : Xerox, Quartz : Karlsruhe,
Ptolemy : Berkeley, Lava : Chalmers, Xilinx
• Industrial use in the 90's
LUSTRE / SCADE : nuclear plants (Schneider), avionics (Airbus)
Esterel : avionics (Dassault), telecom
Signal / SILDEX : continuous control (SNECMA, EDF)
Ptolemy-based systems (CoCentric) : hardware & signal processing
• => Full development in the 2000's
© Esterel Technologies, 2003
G. Berry, VLSI'2004 synchronous tutorial, 1 - 15
Agenda - Part 1
Synchrony for Embedded Systems
• Embedded systems and correctness issues
• The three models of concurrency
• The synchronous model : data and control
• The synchronous design flows
• Current applications and envisioned extensions
© Esterel Technologies, 2003
G. Berry, VLSI'2004 synchronous tutorial, 1 - 16
Q
R
P
P||Q
Concurrency : the compositionality principle
© Esterel Technologies, 2003
G. Berry, VLSI'2004 synchronous tutorial, 1 - 17
d
t
Q
P
t’
t’’
R
P||Q
t’’ = t + d + t’
t’’ ~ t ~ d ~ t’
t~t+t
© Esterel Technologies, 2003
G. Berry, VLSI'2004 synchronous tutorial, 1 - 18
Only 3 solutions :
• t arbitrary
asynchrony
•t=0
synchrony
• t predictable
vibration
© Esterel Technologies, 2003
G. Berry, VLSI'2004 synchronous tutorial, 1 - 19
t arbitrary : Brownian Motion
H+
Cl
_
H+
_ HCL
Cl
H+
Cl
_
HCL
H+
HCL
Chemical reaction
_
+
H + Cl
© Esterel Technologies, 2003
Internet routing
HCL
G. Berry, VLSI'2004 synchronous tutorial, 1 - 20
Zero delay example:
Newtonian Mechanics
Concurrency + Determinism
Calculations are feasible
© Esterel Technologies, 2003
G. Berry, VLSI'2004 synchronous tutorial, 1 - 21
The most difficult real-time manoeuver ever
Here should be a fabulous drawing of Hergé’s
"On a Marché sur la Lune", in English
"Explorers on the Moon". French edition, page 10,
first drawing.
Drunk Captain Haddock has become a satellite
of the Adonis asteroid. To catch him, Tintin,
courageously standing on the rocket's side,
asked Pr. Calculus to start the rocket's atomic engine.
At precisely the right time, he shouts "STOP"!
This is the trickiest real-time manoeuver ever
performed by man. It required a perfect understanding
of Newtonian Mechanics and absolute synchrony.
© Esterel Technologies, 2003
G. Berry, VLSI'2004 synchronous tutorial, 1 - 22
Here should be the 3rd
drawing of page 10 of
"Explorers on the Moon".
Tintin's manoeuver was
a perfect success, and
he now catches Haddock
with a lasso (highly nontrivial in deep space!)
Digital synchronous circuits
the RTL zero-delay model
Synchronous languages
Esterel, Lustre, Signal, ...
Excellent abstract model
© Esterel Technologies, 2003
G. Berry, VLSI'2004 synchronous tutorial, 1 - 23
t predictable : vibration
Nothing can illustrate vibration better than
Bianca Castafiore, Hergé's famous prima
donna. See [1] for details. The power of her
voice forcibly shakes the microphone and
the ears of the poor spectators.
[1] King's Ottokar Sceptre, Hergé, page 29,
last drawing.
propagation of light, electrons, program counter...
© Esterel Technologies, 2003
G. Berry, VLSI'2004 synchronous tutorial, 1 - 24
The synchronous model
Bianca Castafiore singing for the King
Muskar XII in Klow, Syldavia. King's Ottokar
Sceptre, page 38, first drawing.
Although the speed of sounds is finite, it is
fast enough to look infinite. Full abstraction!
If room small enough,
predictable delay implements zero-delay
Specify with zero-delay
Implement with predictable delay
Control room size (delay analysis)
© Esterel Technologies, 2003
G. Berry, VLSI'2004 synchronous tutorial, 1 - 25
Software Synchronous Systems
Cycle based
read inputs
compute reaction
produce outputs
Synchronous = within the same cycle
propagate control
propagate signals
Zero-delay : standard model in control theory
© Esterel Technologies, 2003
G. Berry, VLSI'2004 synchronous tutorial, 1 - 26
Hardware - the RTL model
REQ
OK
TRY
PASS
GO
GET_TOKEN
PASS_TOKEN
OK = REQ and GO
PASS = not REQ and GO
GO = TRY or GET_TOKEN
PASS_TOKEN = reg(GET_TOKEN)
© Esterel Technologies, 2003
G. Berry, VLSI'2004 synchronous tutorial, 1 - 27
Synchronous Languages
Characteristics
• A very simple computation model
valid for software and hardware
• A high degree of concurrency
but still deterministic
• Mathematical semantics
made understandable and usable
• Translation algorithms to hardware and software
correct by construction
• Formal verification
based on mathematical semantics
© Esterel Technologies, 2003
G. Berry, VLSI'2004 synchronous tutorial, 1 - 28
Agenda - Part 1
Synchrony for Embedded Systems
• Embedded systems and correctness issues
• The three models of concurrency
• The synchronous model : data and control
• The synchronous design flows
• Current applications and envisioned extensions
© Esterel Technologies, 2003
G. Berry, VLSI'2004 synchronous tutorial, 1 - 29
Data vs. Control
signals
signals
control
data
values
Esterel
SyncCharts
Argos
PBS
© Esterel Technologies, 2003
values
Lustre
SCADE
Signal
Lava
Esterel v7
G. Berry, VLSI'2004 synchronous tutorial, 1 - 30
Data-Dominated Designs
Behavior steady,data flows
data path, signal processing, continuous control
Lustre / SCADE : sequential equations, declarative
0.
U
pre
Yt = sin(Xt) * cos(Yt-1)
*
+
X
sin
pre
1.
+
Y = sin(X) * cos(pre(Y))
cos
S
pre
boxes = operators
arrows = data flows
© Esterel Technologies, 2003
G. Berry, VLSI'2004 synchronous tutorial, 1 - 31
Control-Dominated Designs
Behavior keeps changing, little data handling
state-machine control
bus protocols, memory / cache / pipeline control
Esterel v5 / SyncCharts : imperative + hierarchical behavior
abort
sustain DmaReq
when DmaOk;
abort
abort
every ByteIn do
emit ByteOut (?ByteIn)
end every
when DmaEnd
when 10 MilliSecond do
emit TimeOut
end abort
© Esterel Technologies, 2003
boxes = states
arrows = transitions
names = signals
hierarchy = preemption
G. Berry, VLSI'2004 synchronous tutorial, 1 - 32
The Evolution: Mixed Designs
Tricky control path + extensive data path
Multi-mode signal processing, alarm detection and handling
Bus bridges, QoS arbiters, fancy memory control
• Software: SCADE incorporates Esterel state machines
• Hardware: Esterel v7 incorporates Lustre equations
• + more system-oriented design features
UML architecture description
configuration management
requirement traceability
© Esterel Technologies, 2003
G. Berry, VLSI'2004 synchronous tutorial, 1 - 33
Data-control interaction :
actions and predicates
+
1
0
*
© Esterel Technologies, 2003
G. Berry, VLSI'2004 synchronous tutorial, 1 - 34
Agenda - Part 1
Synchrony for Embedded Systems
• Embedded systems and correctness issues
• The three models of concurrency
• The synchronous model : data and control
• The synchronous design flows
• Current applications and envisioned extensions
© Esterel Technologies, 2003
G. Berry, VLSI'2004 synchronous tutorial, 1 - 35
Maximal quality constraints:
DO-178B Certified Avionics Software Flow
• Mandatory for civilian avionics, reference elsewhere
• Very strong software engineering control
• Full traceability from source code to embedded bits
Synchronous technology: certifiable code generation
• Code generator certified with the same DO-178-B constraints
• No unit testing needed on generated code
• Airbus: 50 % cost improvement
© Esterel Technologies, 2003
G. Berry, VLSI'2004 synchronous tutorial, 1 - 36
DO-178B Development Processes
System Life Cycle (ARP-4754)
System
Requirements
System
Requirements
Allocated to Software
process
SW
Requirements
process
Change
requests
Software Life Cycle (DO-178B)
High-Level Requirements
SW
Design
process
Change
requests
Low-Level Requirements
& Architecture
Source
Code
SW Coding
process
Integrated
Executable
SW Integration
process
© Esterel Technologies, 2003
G. Berry, VLSI'2004 synchronous tutorial, 1 - 37
Embedded software design flow
Informal specs
simulation
animation
SCADE
data flow
automata
Matlab / Simulink modeling
Formal verification
SAT + numbers
(Prover plug-in)
DO 178-B certifiable
code generator
Embedded C / ADA code
Semantics preservation + compiler certification:
= no unit test needed on C code. Airbus : 50% savings
© Esterel Technologies, 2003
G. Berry, VLSI'2004 synchronous tutorial, 1 - 38
© Esterel Technologies, 2003
G. Berry, VLSI'2004 synchronous tutorial, 1 - 39
Current Software Users
• Avionics: Airbus, Dassault Aviation, EADS, Elbit,
Eurocopter, Flight Dynamics, NASA, Thales, etc.
• Aircraft engines: Hispano-Suiza, Pratt&Whitney, etc.
• Automobile: Audi, General Motors, PSA, etc.
• Automobile equipment: Johnson Controls, Visteon, etc.
• Energy / transportation: CSEE, Framatome, DESS, etc.
© Esterel Technologies, 2003
G. Berry, VLSI'2004 synchronous tutorial, 1 - 40
Esterel v7 Hardware Design Flow
Paper spec
Esterel Spec
(unique reference)
C simulation
System C
FPGA proto.
Formal verification
Test generation
hardware : VHDL, Verilog
software: C, C++
semantics is preserved throughout the flow
and identical for hardware and software
© Esterel Technologies, 2003
G. Berry, VLSI'2004 synchronous tutorial, 1 - 41
Current Hardware Users
• Module-level design: Intel, STM, Thales, T.I, Xilinx
• Application / coprocessor fast prototyping: TI, STM
• SoC modeling and analysis: STM, Philips
• Protocols : Eurecom
• Test generation: T.I., Oberthur
© Esterel Technologies, 2003
G. Berry, VLSI'2004 synchronous tutorial, 1 - 42
Extract of UART with OPB Interface (Xilinx)
© Esterel Technologies, 2003
G. Berry, VLSI'2004 synchronous tutorial, 1 - 43
UART Hardware / Software implementation
on XILINX Virtex Chip XCV2V1000
Hardware (CLB)
Software (SoftCore)
(courtesy of Satnam Singh, Xilinx)
© Esterel Technologies, 2003
G. Berry, VLSI'2004 synchronous tutorial, 1 - 44
Comparison with HDL, SW, and
system-level languages
• Esterel is not a replacement for HDLs, SystemC, or C
Esterel modules can be plugged into any of the above
• Semantics is defined formally, not by implementation
Full mathematical study available
• Everything is synthesizable in hardware and software
Formal semantics and implementation are 100% in agreement
At least 5 different implementation techniques available
• Formal verification is directly based on the semantics
© Esterel Technologies, 2003
G. Berry, VLSI'2004 synchronous tutorial, 1 - 45
Compilers
• Data-flow to software (Lustre / SCADE, Signal)
inline expansion, toplogical sorting
optimization: memory allocation, locality
(limited by traceability)
• Control-flow to hardware (Esterel)
structural translation to RTL + sequential optimization
program dependency graph + smart encoding (Columbia)
• Control-flow to software
RTL simulation in software (Esterel v5 / v7)
static scheduling of control-flow graph (Synopsys)
static scheduling of aggregated blocks (France Telecom, INRIA, Columbia)
© Esterel Technologies, 2003
G. Berry, VLSI'2004 synchronous tutorial, 1 - 46
Different communities, different needs
Safety-critical software : keep it simple
prefer graphical programming
add unit-delays to break cyclic dependencies
=> strong acyclicity constraints on dependencies
=> simplified state machines
Efficient hardware : maximal power
textual programming + some state machines
agressively pack computations in the cycle
play with combinational / sequential logic (pipeline)
accept clever cycles (reincarnation, combinational cycles)
=> minimal language restrictions
© Esterel Technologies, 2003
G. Berry, VLSI'2004 synchronous tutorial, 1 - 47
Different communities, same needs
Better specifications
early executable models from architectural descriptions
golden models, linked to system models
formal contracts with subcontractors
Better synthesis
why recode by hand?
Better formal verification
property checking
sequential equivalence
Architects and designers start understanding
the value of formal methods
© Esterel Technologies, 2003
G. Berry, VLSI'2004 synchronous tutorial, 1 - 48
Agenda - Part 1
Synchrony for Embedded Systems
• Embedded systems and correctness issues
• The three models of concurrency
• The synchronous model : data and control
• The synchronous design flows
• Current applications and envisioned extensions
© Esterel Technologies, 2003
G. Berry, VLSI'2004 synchronous tutorial, 1 - 49
• Current main sweetspot : compact unitary systems
software : flight control, brakes, suspension, airbag,
alarm management, climate control, etc.
hardware : equipment interface (disk, camera), protocols,
DMAs, memory control, caches, etc.
both : simulation, synthesis, formal verification
compatibility with current design chains
• Extensions for full system handling
software : multi-computer distributed system handling
hardware : SoC modeling, multiclock circuits, clock gating
both : controlled non-determinism for modeling
• Towards GALS : Globally Asynchronous Locally Synchronous
use local synchrony as much as possible
connect synchronous islands asynchronously
very similar to a company organization!
© Esterel Technologies, 2003
G. Berry, VLSI'2004 synchronous tutorial, 1 - 50
Descargar

Aucun titre de diapositive