Models of Computation for Embedded System Design Alvise Bonivento Outline Goals MOCs Discrete Events Dataflow Process Networks Petri Nets Synchronous Reactive Communicating Synchronous FSM Labeled Transition Systems SDL Process Networks Hybrid Systems CFSM Conclusions Goals First step in embedded system design specification process Formal representation helps MOCs efficiency formal verification design refinement optimization and implementation TSM framework to compare MOCs MOCs A mathematical description that has a syntax and rules for computation of the behavior described by the syntax semantics Used to specify the semantics of computation and concurrency Characteristics compact description fidelity to design style synthesize and optimize behavior to an implementation Language MOCs MOC affects expressiveness trade off Discrete Event DE Totally ordered events Digital Hardware simulators Verilog VHDL Efficient for large systems but challenged by simultaneous events t t A t B C A B A B t C VHDL delta step solution t A B C t C t Dataflow Process Networks Directed graph actors streams and tokens Process sequence of firings Firings organized into a list and scheduled One cycle through the schedule back to original state DSP problems A C B D A B C D Petri Nets Process control asynchronous communication and scheduling avoids state explosion place transition token The state of a PN is the marking Transition fire when all the predecessors are marked When firing occurs the predecessors decrement their marking and the successors increase it p0 t1 t2 p1 p2 p3 p4 t3 t4 t5 t6 p5 p6 t0 Petri Nets example M 0 0 0 0 0 1 1 T t0 t1 t3 p0 1 1 1 0 0 0 0 0 1 0 1 0 0 0 0 1 0 0 1 0 0 I 0 0 1 0 0 1 0 0 0 1 0 0 0 1 1 0 0 1 0 1 0 1 0 0 0 1 0 1 f 1 1 0 1 0 0 0 t1 p1 p2 p3 p4 t3 t4 t5 t6 p5 p6 t0 T M 1 If M 0 0 1 0 0 1 0 t2 T If 0 M 1 M Synchronous Reactive All signals have events with identical tags synchronous All signals have events at every clock tick Cycle based models clocked synchronous circuit Esterel Synchronous Multirate WCDMA cell simulators User 1 Base Station User 2 DSP User N Communicating Synchronous FSM FSM consists of Set of input symbols Set of output symbols Finite set of states with an initial state Input symbols states output symbols Input symbols states next states Synchronous Sequential behavior vs state explosion Hierarchy concurrency non determinism Other models Labeled Transition Systems LTS SDL Process Networks CSP CCS Communication is based on rendevouz Single LTS is an interleaved asynchronous model Specification simulation and design of TLC protocols Hybrid Systems FA where each state is associated with a set of differential equations When inequalities are satisfied transition may fire Non linear dynamic systems Synchrony vs Asynchrony Basic operation at each clock tick each module reads inputs computes and produces outputs simultaneously Triggering Ordering all modules are triggered to compute at every clock tick System solution unique solution at each clock tick makes verification easier easier Implementation cost may be expensive expensive clock rate not optimized Basic operation events with a non zero amount of time between them each process may take an arbitrary time Triggering Ordering triggered to run only when inputs change System solution difficult to analyze analyze Implementation cost cheaper and more flexible flexible CFSM Globally asynchronous locally synchronous GALS POLIS CFSM has A finite state machine part inputs outputs states transition and output relation A data computation part reference in the transition relation to external combinational functions Locally synchronous behavior each CFSM executes a transition by producing a single output reaction in zero time Globally asynchronous behavior each CFSM reads inputs executes a transition and produces outputs in an unbounded but finite amount of time Asynchronous interaction from a system perspective CFSM Timing behavior a global scheduler controls the interaction of the CFSMs During an execution a CFSM reads its inputs performs a computation possibly changes states and writes its outputs Each input signal is read at most once each input event is cleared at every execution Input events are read atomically Functional behavior Determined by the specified transition relation TR CFSM example Inputs arrive at a regular rate of Ni time units Each CFSM process at a regular rate of Nr if no errors or 2Nr in case of errors No missed event constraint Ni 2 Nr A i i1 err B i2 C o Conclusions No single agreed upon standard MOC CFSM with initially unbounded FIFO buffers GALS Unbounded buffers allows static and quasi static scheduling whenever possible Keep buffers lossy in the formal model and give the designer tools to verify a priori if any loss occurs Enforce no loss for some buffers in the implementation Capture most of the features of the different MOCs Multiple languages with semantics in terms of CFSMs Multiple scheduling allocation partitioning HW SW synthesis algorithm can be applied Formal verification throughout the design process
View Full Document
Unlocking...