The MARCO/DARPA Gigascale SiliconResearch Center for Design & TestPage 1Part 3: Models of Computation•FSMs• Discrete Event Systems •CFSMs• Data Flow Models•Petri Nets •The Tagged Signal ModelEE249Fall071The Tagged Signal Model• Synchronous Languages and De-synchronization • Heterogeneous Composition: Hybrid Systems and Languages • Interface Synthesis and Verification • Trace Algebra, Trace Structure Algebra and Agent Algebra 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 functionEE249Fall072order to maximize (or minimize) a cost function• Models can be used to reason about the properties of an objectThe MARCO/DARPA Gigascale SiliconResearch Center for Design & TestPage 2Formalization• Model of a design with precise unambiguous semantics:– Implicit or explicit relations: inputs, outputs and (possibly) state variables– Properties – “Cost” functions – ConstraintsEE249Fall073Formalization of Design + Environment =closed system of equations and inequalities over some algebra.Models of Computation: And There are More...• Continuous time (ODEs)• Spatial/temporal (PDEs)• Discrete time• Rendezvous• Synchronous/Reactive• Dataflow• ...Each of theseEE249Fall074Tower of Babel, Bruegel, 1563Each of these provides a formal framework for reasoning about certain aspects of embedded systems.The MARCO/DARPA Gigascale SiliconResearch Center for Design & TestPage 3Model Of ComputationDefinition: 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 equationAn MoC allows:– To capture unambiguously the required functionality– To verify correctness of the functional specification wrt properties–To synthesize part of the specificationEE249Fall075To 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 algorithmsUsefulness of a Model of Computation• Expressiveness• Generality• Simplicity• Compilability/ Synthesizability• VerifiabilityThe ConclusionEE249Fall076The ConclusionOne 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.The MARCO/DARPA Gigascale SiliconResearch Center for Design & TestPage 4Common Models of Computation• Finite State Machines– finite state– no concurrency nor time • Data-Flow– Partial Order– Concurrent and Determinate–Stream of computationEE249Fall077Stream of computation• Discrete-Event– Global Order (embedded in time)• Continuous TimeThe behavior of a design in general is described by a compositionControl versus Data Flow• Fuzzy distinction, yet useful for:–specification (language model )specification (language, model, ...)– synthesis (scheduling, optimization, ...)– validation (simulation, formal verification, ...)• Rough classification:– control:– don’t know when data arrive (quick reaction)EE249Fall078– time of arrival often matters more than value– data:– data arrive in regular streams (samples)– value matters mostThe MARCO/DARPA Gigascale SiliconResearch Center for Design & TestPage 5Control versus Data Flow•Specification, synthesis and validation methodsemphasize: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:EE249Fall079for data:– functional dependency between input and output– memory/time efficiency (Dataflow scheduling for efficient pipelining)– all events and processes are equalThe vending machine• A machine that sells coffee– Accepts one dollar (d1) bills – Maximum two dollars– Quarters change – Sells two products– Small coffee for $1EE249Fall0710– Large coffee for $1.25The MARCO/DARPA Gigascale SiliconResearch Center for Design & TestPage 6Denotational description basicsDenotational descriptions are “implicit” in the sense that they describe the properties that the system must have. They often are given as a system of pp y y g yequalities 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)EE249Fall0711just 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 QVending machine description• Alphabet$$QuarterQuarterEE249Fall0712Small coffeSmall coffe$1 dollar bill$1 dollar billLarge coffeeLarge coffeeQuarterQuarterThe MARCO/DARPA Gigascale SiliconResearch Center for Design & TestPage 7Vending machine description• Vending machine process•It’s a recursive definition of the formBehaves as ( small “choice” large) until successful completion and then like VMBehaves as ( small “choice” large) until successful completion and then like VMEE249Fall0713It s a recursive definition of the form• For a large coffee: Vending machine FSM• The encoding of the behaviors with a labeled directed graphNi t/tt t( ithidleidle$1$1c2c2c1c1•No inputs/outputs yet (as in the denotational description)EE249Fall0714$2$2c4c4c3c3The MARCO/DARPA Gigascale SiliconResearch Center for Design & TestPage 8Vending machine I/O descriptionState transition functionState transition functionOutput functionOutput function(deterministic description)(deterministic description)EE249Fall0715Output functionOutput
View Full Document
Unlocking...