--
-- A data driven pipeline example.
--
-- Three pipelines are implemented, p1, p2 and p3. Each has three phases.
-- The execution times and periods are described at the beginning of each
-- phase. By commenting out/uncommenting lines in the main module the
-- example can be made data driven or synchronized. A data driven pipeline
-- is one in which the next phase is ready to execute when the previous
-- one finishes. In the synchronized one all phases only execute according
-- to their periodicity, independent of data availability.
--
-- Sergio Campos -- 07/94
--
---
--- Pipeline 1. Period 20ms, exec time: p11: 3ms, p12: 3ms, p13: 4ms.
---
-- period 20ms, execution time 3ms
MODULE pipe11(timeout, processor_granted)
VAR
state: 0..3; -- program counter.
DEFINE
start := state = 0 & timeout;
finish := state = 3;
request := case -- Tells the scheduler that this
state = 0: FALSE; -- process wants to execute.
TRUE: TRUE;
esac;
ASSIGN
init(state) := 0;
next(state) := case
start: 1;
finish: 0;
!(processor_granted = p11): state;
state = 0: 0;
TRUE: (state + 1) mod 4;
esac;
-- period 20ms, execution time 3ms
MODULE pipe12(timeout, processor_granted)
VAR
state: 0..3;
DEFINE
start := state = 0 & timeout;
finish := state = 3;
request := case
state = 0: FALSE;
TRUE: TRUE;
esac;
ASSIGN
init(state) := 0;
next(state) := case
start: 1;
finish: 0;
!(processor_granted = p12): state;
state = 0: 0;
TRUE: (state + 1) mod 4;
esac;
-- period 20ms, execution time 4ms
MODULE pipe13(timeout, processor_granted)
VAR
state: 0..4;
DEFINE
start := state = 0 & timeout;
finish := state = 4;
request := case
state = 0: FALSE;
TRUE: TRUE;
esac;
ASSIGN
init(state) := 0;
next(state) := case
start: 1;
finish: 0;
!(processor_granted = p13): state;
state = 0: 0;
TRUE: (state + 1) mod 5;
esac;
---
--- Pipeline 2. Period 50ms, exec time: p21: 6ms, p22: 4ms, p23: 5ms.
---
-- period 50ms, execution time 6ms
MODULE pipe21(timeout, processor_granted)
VAR
state: 0..6;
DEFINE
start := state = 0 & timeout;
finish := state = 6;
request := case
state = 0: FALSE;
TRUE: TRUE;
esac;
ASSIGN
init(state) := 0;
next(state) := case
start: 1;
finish: 0;
!(processor_granted = p21): state;
state = 0: 0;
TRUE: (state + 1) mod 7;
esac;
-- period 50ms, execution time 6ms
MODULE pipe22(timeout, processor_granted)
VAR
state: 0..4;
DEFINE
start := state = 0 & timeout;
finish := state = 4;
request := case
state = 0: FALSE;
TRUE: TRUE;
esac;
ASSIGN
init(state) := 0;
next(state) := case
start: 1;
finish: 0;
!(processor_granted = p22): state;
state = 0: 0;
TRUE: (state + 1) mod 5;
esac;
-- period 50ms, execution time 5ms
MODULE pipe23(timeout, processor_granted)
VAR
state: 0..5;
DEFINE
start := state = 0 & timeout;
finish := state = 5;
request := case
state = 0: FALSE;
TRUE: TRUE;
esac;
ASSIGN
init(state) := 0;
next(state) := case
start: 1;
finish: 0;
!(processor_granted = p23): state;
state = 0: 0;
TRUE: (state + 1) mod 6;
esac;
---
--- Pipeline 3. Period 100ms, exec time: p31: 5ms, p32: 6ms, p33: 5ms.
---
-- period 100ms, execution time 5ms
MODULE pipe31(timeout, processor_granted)
VAR
state: 0..5;
DEFINE
start := state = 0 & timeout;
finish := state = 5;
request := case
state = 0: FALSE;
TRUE: TRUE;
esac;
ASSIGN
init(state) := 0;
next(state) := case
start: 1;
finish: 0;
!(processor_granted = p31): state;
state = 0: 0;
TRUE: (state + 1) mod 6;
esac;
-- period 100ms, execution time 6ms
MODULE pipe32(timeout, processor_granted)
VAR
state: 0..6;
DEFINE
start := state = 0 & timeout;
finish := state = 6;
request := case
state = 0: FALSE;
TRUE: TRUE;
esac;
ASSIGN
init(state) := 0;
next(state) := case
start: 1;
finish: 0;
!(processor_granted = p32): state;
state = 0: 0;
TRUE: (state + 1) mod 7;
esac;
-- period 100ms, execution time 5ms
MODULE pipe33(timeout, processor_granted)
VAR
state: 0..5;
DEFINE
start := state = 0 & timeout;
finish := state = 5;
request := case
state = 0: FALSE;
TRUE: TRUE;
esac;
ASSIGN
init(state) := 0;
next(state) := case
start: 1;
finish: 0;
!(processor_granted = p33): state;
state = 0: 0;
TRUE: (state + 1) mod 6;
esac;
MODULE main
VAR
timer: 0..100; -- Global timer, defines start times.
ASSIGN
init(timer) := 0;
next(timer) := (timer + 1) mod 100;
DEFINE
timeout100 := timer mod 100 = 0;
timeout50 := timer mod 50 = 0;
timeout20 := timer mod 20 = 0;
VAR
-- data driven pipeline. Each phase is awoken by the end of the
-- previous phase:
-- P11: pipe11(timeout20, processor_granted);
-- P12: pipe12(P11.finish, processor_granted);
-- P13: pipe13(P12.finish, processor_granted);
-- P21: pipe21(timeout50, processor_granted);
-- P22: pipe22(P21.finish, processor_granted);
-- P23: pipe23(P22.finish, processor_granted);
-- P31: pipe31(timeout100, processor_granted);
-- P32: pipe32(P31.finish, processor_granted);
-- P33: pipe33(P32.finish, processor_granted);
-- synchronized pipeline. Each phase has its own period:
P11: pipe11(timeout20, processor_granted);
P12: pipe12(timeout20, processor_granted);
P13: pipe13(timeout20, processor_granted);
P21: pipe21(timeout50, processor_granted);
P22: pipe22(timeout50, processor_granted);
P23: pipe23(timeout50, processor_granted);
P31: pipe31(timeout100,processor_granted);
P32: pipe32(timeout100,processor_granted);
P33: pipe33(timeout100,processor_granted);
-- used just to make SMV recognize the symbols idle and p*.
aux: {idle, p11, p12, p13, p21, p22, p23, p31, p32, p33};
--
-- Simple priority driven scheduler. The processor is given to the
-- highest process in the list below that is requesting execution.
-- Notice that if a higher priority process requests execution, the
-- currently executing process can be preempted.
--
DEFINE
processor_granted := case
P11.request: p11;
P12.request: p12;
P13.request: p13;
P21.request: p21;
P22.request: p22;
P23.request: p23;
P31.request: p31;
P32.request: p32;
P33.request: p33;
TRUE: idle;
esac;
-- error would occur if a timeout occurs and the process hasn't finished
-- the previous execution yet. This model does not handle this properly.
error := timeout20 & !(P11.state = 0) |
timeout20 & !(P12.state = 0) |
timeout20 & !(P13.state = 0) |
timeout50 & !(P21.state = 0) |
timeout50 & !(P22.state = 0) |
timeout50 & !(P23.state = 0) |
timeout100 & !(P31.state = 0) |
timeout100 & !(P32.state = 0) |
timeout100 & !(P33.state = 0);
SPEC AG !error
-- compute each pipeline execution time
COMPUTE MIN[P11.start, P13.finish]
COMPUTE MAX[P11.start, P13.finish]
COMPUTE MIN[P21.start, P23.finish]
COMPUTE MAX[P21.start, P23.finish]
COMPUTE MIN[P31.start, P33.finish]
COMPUTE MAX[P31.start, P33.finish]
-- Compute each pipeline execution time
COMPUTE MIN[timeout20, P13.finish]
COMPUTE MAX[timeout20, P13.finish]
COMPUTE MIN[timeout50, P23.finish]
COMPUTE MAX[timeout50, P23.finish]
COMPUTE MIN[timeout100, P33.finish]
COMPUTE MAX[timeout100, P33.finish]