EECS222: Embedded System Modeling Lecture 9
EECS 222:
Embedded System Modeling
Lecture 9
Rainer Dömer
doemer@uci.edu
The Henry Samueli School of Engineering
Electrical Engineering and Computer Science
University of California, Irvine
Lecture 9: Overview
• SLDL Semantics
– Concepts and Goals
• Execution and Simulation Semantics
– Motivating Examples (SpecC)
– Motivating Examples (SystemC)
• Simulation Semantics
– Discrete Event Simulation (DES)
– DES Algorithm for SpecC
– DES Algorithm for SystemC
EECS222: Embedded System Modeling, Lecture 9 (c) 2019 R. Doemer 2
(c) 2019 R. Doemer 1
EECS222: Embedded System Modeling Lecture 9
SLDL Semantics
• Essential Concepts in Embedded System Models
– Behavioral hierarchy
• Concurrency, state transitions, exception handling
– Structural hierarchy and connectivity
– Synchronization and communication
– Timing
SLDL must support these concepts in syntax and semantics
• Language semantics define the meaning of constructs
– Execution semantics (for modeling, simulation, and synthesis)
– Deterministic vs. non-deterministic behavior
– Preemptive vs. non-preemptive concurrency
– Atomic operations
– Safe synchronization and communication
EECS222: Embedded System Modeling, Lecture 9 (c) 2019 R. Doemer 3
SLDL Semantics
• Language Semantics are needed for …
– System designer
• Description and modeling
– Electronic Design Automation (EDA) tools
• Validation (compilation, simulation, estimation)
• Analysis (verification, property checking)
• Synthesis (implementation)
– Documentation and standardization
• Objective
Clearly define the execution semantics of the SLDL
• Requirements and Goals
– Precision (no ambiguities)
– Abstraction (no implementation details)
– Formality (enable formal reasoning)
– Simplicity (easy understanding)
EECS222: Embedded System Modeling, Lecture 9 (c) 2019 R. Doemer 4
(c) 2019 R. Doemer 2
EECS222: Embedded System Modeling Lecture 9
SLDL Semantics
• Defining Artifacts Available (SpecC and SystemC)
– Documentation
• Language Reference Manual (LRM)
set of rules written in English (somewhat formal)
• Abstract simulation algorithm
set of valid implementations (abstract, but not general)
– Reference implementation
• SpecC Reference Compiler and Simulator,
SystemC Proof-of-Concept Implementation
one instance of a valid implementation (very specific)
• Compliance test bench
set of specific test cases (specific, but incomplete)
– Formal execution semantics
• Time-interval formalism (only exists for SpecC)
rule-based formalism (mathematical, but incomplete)
• Abstract State Machines
fully formal approach (algebraic notation, not easy to understand)
EECS222: Embedded System Modeling, Lecture 9 (c) 2019 R. Doemer 5
Execution and Simulation Semantics
• Motivating Example 1 (SpecC)
– Given:
behavior B1(int x) behavior B2(int x) behavior B
{ { {
void main(void) void main(void) int x;
{ { B1 b1(x);
x = 5; x = 6; B2 b2(x);
} }
}; }; void main(void)
{
b1;
b2;
}
};
– What is the value of x after the execution of B?
– Answer: x = 6
EECS222: Embedded System Modeling, Lecture 9 (c) 2019 R. Doemer 6
(c) 2019 R. Doemer 3
EECS222: Embedded System Modeling Lecture 9
Execution and Simulation Semantics
• Motivating Example 2 (SpecC)
– Given:
behavior B1(int x) behavior B2(int x) behavior B
{ { {
void main(void) void main(void) int x;
{ { B1 b1(x);
x = 5; x = 6; B2 b2(x);
} }
}; }; void main(void)
{
par{b1; b2;}
}
};
– What is the value of x after the execution of B?
– Answer: The model is non-deterministic
(x may be 5, or 6, or any other value!)
EECS222: Embedded System Modeling, Lecture 9 (c) 2019 R. Doemer 7
Execution and Simulation Semantics
• Motivating Example 3 (SpecC)
– Given:
behavior B1(int x) behavior B2(int x) behavior B
{ { {
void main(void) void main(void) int x;
{ { B1 b1(x);
waitfor 10; x = 6; B2 b2(x);
x = 5; }
} }; void main(void)
}; {
par{b1; b2;}
}
};
– What is the value of x after the execution of B?
– Answer: x = 5
EECS222: Embedded System Modeling, Lecture 9 (c) 2019 R. Doemer 8
(c) 2019 R. Doemer 4
EECS222: Embedded System Modeling Lecture 9
Execution and Simulation Semantics
• Motivating Example 4 (SpecC)
– Given:
behavior B1(int x) behavior B2(int x) behavior B
{ { {
void main(void) void main(void) int x;
{ { B1 b1(x);
waitfor 10; waitfor 10; B2 b2(x);
x = 5; x = 6;
} } void main(void)
}; }; {
par{b1; b2;}
}
};
– What is the value of x after the execution of B?
– Answer: The model is non-deterministic
(x may be 5, or 6, or any other value!)
EECS222: Embedded System Modeling, Lecture 9 (c) 2019 R. Doemer 9
Execution and Simulation Semantics
• Motivating Example 5 (SpecC)
– Given:
behavior B1( behavior B2( behavior B
int x, event e) int x, event e) {
{ { int x;
void main(void) void main(void) event e;
{ { B1 b1(x,e);
x = 5; wait e; B2 b2(x,e);
notify e; x = 6;
} } void main(void)
}; }; {
par{b1; b2;}
}
};
– What is the value of x after the execution of B?
– Answer: x = 6
EECS222: Embedded System Modeling, Lecture 9 (c) 2019 R. Doemer 10
(c) 2019 R. Doemer 5
EECS222: Embedded System Modeling Lecture 9
Execution and Simulation Semantics
• Motivating Example 6 (SpecC)
– Given:
behavior B1( behavior B2( behavior B
int x, event e) int x, event e) {
{ { int x;
void main(void) void main(void) event e;
{ { B1 b1(x,e);
notify e; wait e; B2 b2(x,e);
x = 5; x = 6;
} } void main(void)
}; }; {
par{b1; b2;}
}
};
– What is the value of x after the execution of B?
– Answer: x = 6
EECS222: Embedded System Modeling, Lecture 9 (c) 2019 R. Doemer 11
Execution and Simulation Semantics
• Motivating Example 7 (SpecC)
– Given:
behavior B1( behavior B2( behavior B
int x, event e) int x, event e) {
{ { int x;
void main(void) void main(void) event e;
{ { B1 b1(x,e);
waitfor 10; wait e; B2 b2(x,e);
x = 5; x = 6;
notify e; } void main(void)
} }; {
}; par{b1; b2;}
}
};
– What is the value of x after the execution of B?
– Answer: x = 6
EECS222: Embedded System Modeling, Lecture 9 (c) 2019 R. Doemer 12
(c) 2019 R. Doemer 6
EECS222: Embedded System Modeling Lecture 9
Execution and Simulation Semantics
• Motivating Example 8 (SpecC)
– Given:
behavior B1( behavior B2( behavior B
int x, event e) int x, event e) {
{ { int x;
void main(void) void main(void) event e;
{ { B1 b1(x,e);
x = 5; waitfor 10; B2 b2(x,e);
notify e; wait e;
} x = 6; void main(void)
}; } {
}; par{b1; b2;}
}
};
– What is the value of x after the execution of B?
– Answer: B never terminates
(the event is lost!)
EECS222: Embedded System Modeling, Lecture 9 (c) 2019 R. Doemer 13
Execution and Simulation Semantics
• Motivating Example 9: SystemC Difference
– Given:
SC_MODULE(Top) void Top::th1(void) void Top::th2(void)
{ { {
int x; x = 5; x = 6;
}; };
void th1(void);
void th2(void);
SC_CTOR(Top)
{ SC_THREAD(th1);
SC_THREAD(th2);
}
};
– What is the value of x at the end of simulation?
– Answer: The model is non-deterministic!
x may have the value 5 or 6,
but not any other value!
EECS222: Embedded System Modeling, Lecture 9 (c) 2019 R. Doemer 14
(c) 2019 R. Doemer 7
EECS222: Embedded System Modeling Lecture 9
Execution and Simulation Semantics
• Motivating Example 10: SystemC Difference
– Given:
SC_MODULE(Top) void Top::th1(void) void Top::th2(void)
{ { {
int x; x = 5; wait(e);
sc_event e; e.notify(); x = 6;
void th1(void); }; };
void th2(void);
SC_CTOR(Top)
{ SC_THREAD(th1);
SC_THREAD(th2);
}
};
– What is the value of x at the end of simulation?
– Answer: The model is non-deterministic!
x may have the value 5 or 6.
The immediate notification may get lost!
EECS222: Embedded System Modeling, Lecture 9 (c) 2019 R. Doemer 15
Execution and Simulation Semantics
• Motivating Example 11: SystemC Difference
– Given:
SC_MODULE(Top) void Top::th1(void) void Top::th2(void)
{ { {
int x; x = 5; wait(e);
sc_event e; e.notify( x = 6;
void th1(void); SC_ZERO_TIME); };
void th2(void); };
SC_CTOR(Top)
{ SC_THREAD(th1);
SC_THREAD(th2);
}
};
– What is the value of x at the end of simulation?
– Answer: x = 6
Delta notification is safe!
EECS222: Embedded System Modeling, Lecture 9 (c) 2019 R. Doemer 16
(c) 2019 R. Doemer 8
EECS222: Embedded System Modeling Lecture 9
Simulation Semantics
• Discrete Event Simulation (DES) Algorithm for SpecC
– available in LRM (appendix), good for documentation
abstract definition (defines a set of valid implementations)
not general (possibly incomplete)
• Definitions:
– At any time, each thread t is in one of the following sets:
• READY: set of threads ready to execute (initially root thread)
• WAIT: set of threads suspended by wait (initially Ø)
• WAITFOR: set of threads suspended by waitfor (initially Ø)
– Notified events are stored in a set N
• notify e1 adds event e1 to N
• wait e1 will wakeup when e1 is in N
• Consumption of event e means event e is taken out of N
• Expiration of notified events means N is set to Ø
EECS222: Embedded System Modeling, Lecture 9 (c) 2019 R. Doemer 17
Simulation Semantics
• Discrete Event Simulation (DES) Algorithm for SpecC
Start
Select thread tREADY, execute t
YES
notify Add notified events to N
YES
wait Move tREADY to WAIT
YES
waitfor Move tREADY to WAITFOR
NO
NO
READY=Ø
YES
Move all tWAIT waiting for events eN to READY
Set N=Ø
NO
READY=Ø
YES
Update simulation time, move earliest tWAITFOR to READY
NO
READY=Ø
YES
EECS222: Embedded System Modeling, Lecture 9 Stop (c) 2019 R. Doemer 18
(c) 2019 R. Doemer 9
EECS222: Embedded System Modeling Lecture 9
Simulation Semantics
• Discrete Event Simulation (DES) Algorithm for SpecC
– Conforms to general Discrete Event (DE) Simulation
• utilizes delta-cycle mechanism (i.e. inner event loop)
• closely matches execution semantics of other languages
– SystemC
– VHDL
– Verilog
– Features
• clearly specifies the simulation semantics
• is easy to understand
• is straight-forward to implement
– Generality
• is one valid implementation of the semantics
• other valid implementations may exist as well
EECS222: Embedded System Modeling, Lecture 9 (c) 2019 R. Doemer 19
Simulation Semantics
• Discrete Event Simulation (DES) Algorithm for SystemC
EECS222: Embedded System Modeling, Lecture 9 (c) 2019 R. Doemer 20
(c) 2019 R. Doemer 10
EECS222: Embedded System Modeling Lecture 9
Simulation Semantics
• Discrete Event Simulation (DES) Algorithm for SystemC
EECS222: Embedded System Modeling, Lecture 9 (c) 2019 R. Doemer 21
(c) 2019 R. Doemer 11