The MARCO DARPA Gigascale Silicon Research Center for Design Test Part 3 Models of Computation FSMs Discrete Event Systems CFSMs Data Flow Models Petri Nets The Tagged Signal Model Synchronous Languages and De synchronization Heterogeneous Composition Hybrid Systems and Languages Interface Synthesis and Verification 1 Trace Algebra Trace Structure Algebra and Agent Algebra EE249Fall07 Design From an idea build something that performs a certain function Never done directly some aspects are not considered at the beginning of the development the designer wants to explore different possible implementations in order to maximize or minimize a cost function Models can be used to reason about the properties of an object 2 EE249Fall07 Page 1 The MARCO DARPA Gigascale Silicon Research Center for Design Test Formalization Model of a design with precise unambiguous semantics Implicit or explicit relations inputs outputs and possibly state variables Properties Cost functions Constraints Formalization of Design Environment closed system of equations and inequalities over some algebra 3 EE249Fall07 Models of Computation And There are More Continuous time ODEs Spatial temporal PDEs Discrete time Rendezvous Synchronous Reactive Dataflow Each of these provides a formal framework for reasoning about certain aspects of embedded systems Tower of Babel Bruegel 1563 4 EE249Fall07 Page 2 The MARCO DARPA Gigascale Silicon Research Center for Design Test Model Of Computation Definition 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 Examples Finite State Machine Turing Machine differential equation An MoC allows To capture unambiguously the required functionality To verify correctness of the functional specification wrt properties To synthesize part of the specification To use different tools all must understand the model MOC needs to be powerful enough for application domain have appropriate synthesis and validation algorithms 5 EE249Fall07 Usefulness of a Model of Computation Expressiveness Generality Simplicity Compilability Synthesizability Verifiability The Conclusion 6 One way to get all of these is to mix diverse simple models of computation while keeping compilation synthesis and verification separate for each MoC To do that we need to understand these MoCs relative to one another and understand their interaction when combined in a single system design EE249Fall07 Page 3 The MARCO DARPA Gigascale Silicon Research Center for Design Test Common Models of Computation Finite State Machines finite state no concurrency nor time Data Flow Partial Order Concurrent and Determinate Stream of computation Discrete Event Global Order embedded in time Continuous Time The behavior of a design in general is described by a composition 7 EE249Fall07 Control versus Data Flow Fuzzy distinction yet useful for specification language language model model synthesis scheduling optimization validation simulation formal verification Rough classification control don t know when data arrive quick reaction time of arrival often matters more than value data data arrive in regular streams samples value matters most 8 EE249Fall07 Page 4 The MARCO DARPA Gigascale Silicon Research Center for Design Test Control versus Data Flow Specification synthesis and validation methods emphasize for control event reaction relation response time Real Time scheduling for deadline satisfaction priority among events and processes for data functional dependency between input and output memory time efficiency Dataflow scheduling for efficient pipelining all events and processes are equal 9 EE249Fall07 The vending machine A machine that sells coffee Accepts one dollar d1 bills Maximum two dollars Quarters change Sells two products Small coffee for 1 Large coffee for 1 25 10 EE249Fall07 Page 5 The MARCO DARPA Gigascale Silicon Research Center for Design Test Denotational description basics Denotational descriptions are implicit in the sense that they describe the properties p p that the system y must have They y often are g given as a system y of equalities and inequalities that must be satisfied by the system The controller is denoted by a set of traces of symbols from an alphabet Non all capital letters names belong to the alphabet of a process Capital letters names denote processes CTRL is the controller process A process is a letter followed by a process P x Q SKIP is a processes that successfully completes execution it does nothing it just completes the execution If P and Q are processes then Z P Q is a process that behaves like P until it completes and then like Q If P and Q are processes then P Q denotes a choice between P and Q 11 EE249Fall07 Vending machine description Alphabet Quarter dollar bill 1 Small coffe Large coffee 12 EE249Fall07 Page 6 The MARCO DARPA Gigascale Silicon Research Center for Design Test Vending machine description Vending machine process Behaves as small choice large until successful completion and then like VM It It ss a recursive definition of the form For a large coffee 13 EE249Fall07 Vending machine FSM The encoding of the behaviors with a labeled directed graph No N iinputs outputs t t t yett as in i the th denotational description idle c1 1 c2 2 c3 c4 14 EE249Fall07 Page 7 The MARCO DARPA Gigascale Silicon Research Center for Design Test Vending machine I O description deterministic description State transition function Output function If waiting and one dollar is inserted change state to 1 credit Examples If 1 credit and small coffee is requested change state to idle and serve the coffee 15 EE249Fall07 Vending machine I O description Lables where input and output can both be empty idle c1 1 c2 2 c3 c4 16 EE249Fall07 Page 8 The MARCO DARPA Gigascale Silicon Research Center for Design Test Communication with the rest of the system Our state machine does not live in isolation What is the communication semantics The serving system and the change return are electromechanical system with their own evolution dynamics Serving system Change return system 17 EE249Fall07 The Nokia 3120 User Interface Keypad Events Controller Control software 18 EE249Fall07 Page 9 The MARCO DARPA Gigascale Silicon Research Center for Design Test Controller description Denotational The controller is denoted by a set of traces of symbols from an alphabet Non all capital letters names belong to the alphabet of
View Full Document
Unlocking...