Comparing Models of Computation Edward A Lee Alberto SangiovanniVincentelli UC Berkeley Dept of EECS Major Collaborators G Berry W T Chang S Edwards A Girault L Lavagno P Murthy c o m pa r i n g f m Copyright 1996 The Regents of the University of California All rights reserved U N I VERS ITY OF CALIF ORNIA AT BERKEL E Y Design Methodology design automation Henry Wolf Illustration for a book about Xerox Design is a human creative process CAD system designers are toolsmiths but They are not as much constrained by the laws of physics Can use instead the laws of logic or anything else A design environment is an artificial universe Its laws of physics are its semantics c o m pa r i n g f m 1996 p 2 of 61 U N I VERS ITY OF CALIF ORNIA AT BERKEL E Y Not so long ago electronic systems were literal expressions of the electromechanics within Today layers of abstraction hide the electromechanics and we design with metaphors Our metaphors are still too close to the physics c o m pa r i n g f m Giorgio de Chirico Melancholy and Mystery of a Street 1914 An Artificial Universe 1996 p 3 of 61 U N I VERS ITY OF CALIF ORNIA AT BERKEL E Y Abstraction Abstraction in system level design is the act of pulling away or withdrawing from the physical properties of the implementation getting closer to the problem domain avoiding overspecification Piet Mondrian Tableau I 1921 c o m pa r i n g f m 1996 p 4 of 61 U N I VERS ITY OF CALIF ORNIA AT BERKEL E Y Less Abstract Closer to the Physical Piet Mondrian The Grey Tree 1912 c o m pa r i n g f m 1996 p 5 of 61 U N I VERS ITY OF CALIF ORNIA AT BERKEL E Y Still Less Abstract Piet Mondrian The Red Tree 1908 c o m pa r i n g f m 1996 p 6 of 61 U N I VERS ITY OF CALIF ORNIA AT BERKEL E Y Validating Designs By construction property is inherent By verification property is provable syntactically By simulation check behavior for all inputs By intuition property is true I just know it is Meret Oppenheim Object 1936 By assertion property is true Wanna make something of it It is generally better to be higher in this list c o m pa r i n g f m 1996 p 7 of 61 U N I VERS ITY OF CALIF ORNIA AT BERKEL E Y Some Models of Computation Gears Imperative languages Petri nets Synchronous dataflow Dynamic dataflow Process networks Concrete data structures Discrete events Synchronous Reactive languages Communicating sequential processes Finite state machines Hierarchical communicating finite state machines c o m pa r i n g f m 1996 p 8 of 61 U N I VERS ITY OF CALIF ORNIA AT BERKEL E Y Semantics What does it Mean This well established field addresses many of the core problems in the specification and modeling of concurrent systems Issues Concurrency Synchronization A model of time Turing completeness Determinacy Finite state Redundancy Instascan MRI image of a brain responding to light stimulation c o m pa r i n g f m 1996 p 9 of 61 U N I VERS ITY OF CALIF ORNIA AT BERKEL E Y Usefulness of a Model of Computation Expressiveness Generality Simplicity Compilability Synthesizability Verifiability The Conclusion 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 c o m pa r i n g f m 1996 p 10 of 61 U N I VERS ITY OF CALIF ORNIA AT BERKEL E Y What is Time continuous time discrete time Salvador Dali The Persistence of Memory 1931 totally ordered discrete events multirate discrete time E1 E2 E3 E4 F1 F2 F3 F4 G1 G2 G3 G4 synchronous reactive partially ordered discrete events c o m pa r i n g f m 1996 p 11 of 61 U N I VERS ITY OF CALIF ORNIA AT BERKEL E Y Totally Ordered Discrete Event Models Examples of the sorts of problems that arise from a computerized model of physical time P2 P1 What if P1 is causal but not strictly causal f s1 What does this mean s2 s3 s1 s2 Merge What if s1 and s2 have synchronous events c o m pa r i n g f m 1996 p 12 of 61 U N I VERS ITY OF CALIF ORNIA AT BERKEL E Y The Tagged Signal Model A mathematical framework within which the essential properties of models of computation can be understood and compared A denotational framework c o m pa r i n g f m 1996 p 13 of 61 U N I VERS ITY OF CALIF ORNIA AT BERKEL E Y Events and Signals Abstractions of time give us tools to deal with these questions set of values V set of tags T an event e T V a signal is a set of events a functional signal is a partial function s T V T V the set of all signals S 2 the powerset N N tuples of signals s S c o m pa r i n g f m 1996 p 14 of 61 U N I VERS ITY OF CALIF ORNIA AT BERKEL E Y Possible Interpretations of Tags Universal time T Discrete time T is a totally ordered discrete set Precedences T is a partially ordered discrete set Why not always use the most physical model universal time In specifying systems avoid over specifying In modeling systems recognize the inherent difficulty of maintaining a globally consistent notion of time c o m pa r i n g f m 1996 p 15 of 61 U N I VERS ITY OF CALIF ORNIA AT BERKEL E Y Empty Signals and Events The empty signal The tuple of empty signals N Note S and S For any signal s s s For any tuple s s s pointwise union In some models of computation the set V of values includes a special value pronounced bottom which indicates the absence of a value c o m pa r i n g f m 1996 p 16 of 61 U N I VERS ITY OF CALIF ORNIA AT BERKEL E Y Processes and Connections Processes N a process P S for some N a behavior s P s satisfies the process a process is a set of possible behaviors Connections a type of process N a connection C S s s 1 s N C s i s j c o m pa r i n g f m 1996 p 17 of 61 U N I VERS ITY OF CALIF ORNIA AT BERKEL E Y Systems Given a tuple P of processes a system is another process Q P i …
View Full Document
Unlocking...