FSM-based Specification Formalisms
Giovanni De Micheli
Integrated Systems Centre
EPF Lausanne
This presentation can be used for non-commercial purposes as long as this note and the copyright footers are not removed
Giovanni De Micheli All rights reserved
Models of computation
Data-flow oriented models
Focus on computation
Data-flow graphs and derivatives
Control-flow oriented models
Focus on control
Based on finite-state machine models
DF and CF model complementary aspects
(c) Giovanni De Micheli
Module 1
Objectives
FSM models
Languages with a synchronous semantics
Hierarchical FSMs
Expression-based formalisms
(c) Giovanni De Micheli
Formal FSM model
A set of primary inputs patterns X
A set of primary outputs patterns Y
A set of states S
A state transition function:
: X S S
An output function:
: X S Y for Mealy models
:SY
for Moore models
(c) Giovanni De Micheli
Finite-state machines
Primary
Inputs
COMBINATIONAL
CIRCUIT
Primary
Outputs
REGISTERS
clock
A finite-state machine is an abstraction
Computation takes no time
Outputs are available as soon as inputs are
A finite-state machine implementation is a sequential
circuit with a finite cycle-time
(c) Giovanni De Micheli
State diagrams
Directed graph
Vertices = states
Edges = transitions
Equivalent to state transition tables
(c) Giovanni De Micheli
Example
ab + r/0
s0
r/0
r/0
abr/0
abr/0
ar/0
br/0
s1
r/0
abr/1
br/1
s2
ar/0
s3
r/1
(c) Giovanni De Micheli
FSM-based models
Synchronous languages:
Esterel, Argos, Lustre, SDL
Graphical formalisms:
FSMs, hierarchical FSMs, concurrent FSMs
StateCharts
Program-state machines
SpecCharts
(c) Giovanni De Micheli
The synchronous approach
Precise mathematical formalism
Strict semantics
FSM theoretical model
Objectives
Support formal verification
Consider timing with behavior
(c) Giovanni De Micheli
Synchronous models
Perfect synchrony hypothesis
Instantaneous response
Zero-delay computation
Outputs synchronous with inputs
Discrete-time model
Sequence of tics
Environment driven
Inactivity between ticks
(c) Giovanni De Micheli
10
Event-controlled blocks
(in Esterel)
Do task watching event
Exit when event is present
Do task watching event timeout task
Extension to time-out
Trap and handle
Allow for exception handling
(c) Giovanni De Micheli
11
Example: speedometer design
module SPEED:
input SECOND, CM;
output SPEED: integer;
loop
var NB_CM :=0: integer in
do
every CM do
NB_CM := NB_CM + 1;
end every
watching SECOND;
emit SPEED (NB_CM);
end var
end loop
(c) Giovanni De Micheli
12
Example: jogging
do
loop
do RUN_SLOWLY watching 100 M;
do
every STEP do
JUMP || BREATHE
end
watching 15 S;
RUN_FAST
each LAP
watching 2 LAP
(c) Giovanni De Micheli
13
Example: jogging too much
trap HEART_ATTACK in
do
loop
do RUN_SLOWLY watching 100 M;
do
every STEP do
JUMP || BREATHE||CHECK_HEART
end
watching 15 S;
RUN_FAST
each LAP
watching 2 LAP
handle HEART_ATTACK
GO_TO_HOSPITAL
end
(c) Giovanni De Micheli
14
State Charts
Proposed by Harel
Graphic formalism to specify FSMs with:
Hierarchy
Concurrency
Communication
Tools for simulation, animation and synthesis
(c) Giovanni De Micheli
15
State Charts
States
Transitions
Hierarchy
OR (sequential) decomposition
State a sequence of states
AND (concurrent) decomposition
State a set of concurrent states
(c) Giovanni De Micheli
16
State charts
Top_level_uart
transmitter
receiver
tx_mode
rx_mode
csr(2)=1
idle
csr(3)=1
transmit
idle
receive
csr(2)=0
csr(3)=0
load_thr / load:=1;
tx_hold_reg;=data_in;
empty
loaded
empty
rd(tx_hold_reg)/load:=0
uart_mode
[read_enable=1] /
filoful:=1
loaded
read_fifo_cmd/filoful:=0
[csr(2..3)=11]
normal_tx_rx
echo_active
[csr(2..3)=11]
(c) Giovanni De Micheli
17
State Charts
Additional features
State transitions across multiple levels
Timeouts:
Notation on transition arcs denoting the max/min time in a given state
Communication:
Broadcast mechanism based on event generation and reception
History feature:
Keep track of visited states
(c) Giovanni De Micheli
18
StateCharts
Advantages:
Formal basis
Easy to learn
Support of hierarchy, concurrency and exceptions
Avoid exponential blow up of states
Disadvantages:
No description of data-flow computation
(c) Giovanni De Micheli
19
Program State Machines
Combining FSM formalism with program execution
In each state a specific program is active
Hierarchy:
Sequential states
Concurrent states
In a hierarchical state, several programs may be active
(c) Giovanni De Micheli
20
Program state machine example
variable A: array[1..20] of integers
A
D
variable i,max:integer;
B
max=0;
e1
for i=0 to 20 do
e2
if (A[i] > max) then
max = A[i];
end if;
end for
e3
(c) Giovanni De Micheli
21
Program State Machine Transitions
TOC - Transition on completion
Program terminates AND transition condition is true
TI - Transition immediate
Transition condition is true
(c) Giovanni De Micheli
22
SpecCharts
Based on Program State Machines
Introduced by Gajski et al.
Extension of VHDL:
Compilable into VHDL for simulation and synthesis
Behavioral hierarchy
Combining FSM and VHDL formalisms
Leaves of the hierarchy are VHDL models
(c) Giovanni De Micheli
23
State transitions
Sequencing between sub-behaviors are controlled by
transition arcs
A transition arc is labeled by a triple:
(transition type, triggering event, next behavior)
Transition types:
Transition on completion
Transition immediate
Timeout arcs
(c) Giovanni De Micheli
24
Example
E
port P,Q: in integer;
type int_array is array(natural range<>) of integer;
signal A: int_array( 15 downto 0 );
Z
variable i, max:integer;
x1
max-0;
z1
for i=1 to 20 do
e1
x2
if (A[i] > max) then
e4
max = A[i];
z2
end if;
e2
end for
e5
e3
TOC: e2, e3
TI: e1
(c) Giovanni De Micheli
25
SpecCharts semantics
Timing semantics similar to VHDL
Synchronization:
Use wait statement
Use TOC looping back to the top of the program
Communication:
Using variables and signals
Message passing (send/receive)
(c) Giovanni De Micheli
26
SpecCharts
Language
Graphic formalism
Similar to StateCharts
Tools for analysis:
Area, expected performance
Automatic conversion to VHDL
(c) Giovanni De Micheli
27
Example
entity E is
port ( P:in integer; Q: out integer );
end E
architecture A of E is
begin
behavior B type concurrent subbehaviors is
type int_array is array (natural range<>) of integer;
signal M: int_array (15 downto 0);
begin
X: (TOC, true, complete);
Y: (TOC, e3, complete);
Z: ;
behavior X type sequential subbehaviors is
begin
X1: (TI, e1, X2);
X2: (TOC, e2, complete);
behavior X1 type code is
behavior X2 type code is
end X;
behavior Y type code is
variable max: integer;
begin
max:=0;
for J in 0 to 15 loop
if (M(J) > max) then
max:=M(J);
end if;
end loop;
end Y
behavior Z type code is
end B;
end A;
(c) Giovanni De Micheli
28
Expression-based formalisms
Represent sequential behavior by expressions
Advantages:
Symbolic manipulation
Translation into FSM models
Disadvantages:
Loss of data-flow information
(c) Giovanni De Micheli
29
Regular expressions
Model sequential/concurrent behavior
Expressive power equivalent to FSMs
Known techniques for synthesis and analysis
Disadvantages:
No explicit way to express branching
No distinction between concurrent and alternative behavior
(c) Giovanni De Micheli
30
Control-flow expression formalism
Expressions capturing a high-level view of control-flow
while abstracting data-flow information
Expressions are extracted directly from HDL or
programming language specifications
Cycle-based semantics provides a formal interpretation
of HDLs
Based on the algebra of synchronous processes
(Process Algebra)
(c) Giovanni De Micheli
31
Example of design problem
Ethernet controller
Receive Unit
DMA-RCVD
RXE
Host CPU
DMA-FRAME
DMA-BUFFER
DMA-BIT
DMA-XMIT
XMIT-FRAME
XMIT-BIT
RXD
TXD
TXE
Transmit Unit
Memory
CRS
ENQUEUE
EXEC-UNIT
CDT
Execute Unit
System Bus
Network
Coprocessor
Problem
Avoid bus conflicts
(c) Giovanni De Micheli
32
Example of design problem
Ethernet controller
MEMORY
P1
P2
P3
always
always
always
begin
begin
begin
write bus
initialize
wait ( free bus )
receive data
wait ( tr ready )
read bus
end
read bus
end
end
p = p1 p2 p3
p1 = [a.0]
p2 = [0.(c:0)*.a]
p3 = [(x:0)*.a]
(c) Giovanni De Micheli
33
Control-Flow Expressions
Composition
HDL
CFE
Sequential
begin P; Q end
pq
Parallel
fork P; Q join
pq
if (c)
P;
Alternative
else
c:p+c:q
Q;
while (c)
Loop
P;
wait (!c)
(c: p)*
(c: 0)* .p
P;
Infinite
(c) Giovanni De Micheli
always
P;
34
Model properties
Fully deterministic model.
Non-determinism captured by decision variables affecting the
clauses
Design space modeled by decision variables
An implementation is an assignment to decision variables over
time
Constraints expressible by CFEs
Timing, synchronization, resource usage
AWAYS and NEVER sets
Set of actions that always/never execute simultaneously
(c) Giovanni De Micheli
35
Example
Control-Flow Expressions
MEMORY
P1
P2
P3
always
always
always
begin
begin
begin
write bus
initialize
wait ( free bus )
receive data
wait ( tr ready )
read bus
end
read bus
end
end
p = p1 p2 p3
p1 = [a.0]
p2 = [0.(c:0)*.a]
Decision variable x :
p3 = [(x:0)*.a]
Quantifies the synchronization for p3
x0 = 1 Wait because p1 is accessing the bus
x1 = c Use bus unless p2 does it
(c) Giovanni De Micheli
36
Example
Control-Flow Expressions
MEMORY
P2
P3
always
always
always
begin
begin
begin
P1
write bus
initialize
wait ( free bus )
receive data
wait ( tr ready )
read bus
end
read bus
end
end
p = p1 p2 p3
p1 = [a.0]
p2 = [0.(c:0)*.a]
p3 = [(x:0)*.a]
NEVER = {a,a}
Never access the bus twice simultaneously
(c) Giovanni De Micheli
37
Example
Synchronization
SENDER
RECEIVER
Synchronization between a sender and a receiver in a
blocking protocol
Sender = (x : r)*.a
Receiver = (y : k)*.a
ALWAYS = {{a; a}}
NEVER = {{r; k}}
(c) Giovanni De Micheli
38
Design with CFEs
Representation:
A CFE can be compiled into a specification automaton
Representing all feasible behaviors
Synthesis:
A control-unit implementation is a FSM
Derivable from a specification automaton by assigning values
to decision variables over time
Optimization:
Minimize a cost function defined over the decision variables
(c) Giovanni De Micheli
39
CFE Summary
Control-flow expression are a modeling tool
Formal semantic:
Support for synthesis and verification
Synthesis path from CFEs to control-unit
(c) Giovanni De Micheli
40
