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 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 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 P i P N Given a process P S the projection j P S defined by N 1 is s 1 s j 1 s j 1 s N j P if there exists s j S such that s 1 s j 1 s j s j 1 s N P c o m pa r i n g f m 1996 p 18 of 61 U N I VERS ITY OF CALIF ORNIA AT BERKEL E Y An Example s5 s1 s2 P1 s6 C1 C2 s3 s4 s7 P2 Q s8 8 P 1 P 2 C 1 C 2 S Q P 1 P 2 C 1 C 2 Q 2 3 Q S 6 c o m pa r i n g f m 1996 p 19 of 61 U N I VERS ITY OF CALIF ORNIA AT BERKEL E Y Determinacy An input to a process is an externally imposed constraint N I S such that I P is the total set of acceptable behaviors The set of all possible inputs B 2 characterization of a process S N is a further N For example B I I S 1 I s s S means that the first signal is specified externally and can take any value in the set of signals A process is determinate if for all inputs I B I P 1 or I P 0 c o m pa r i n g f m 1996 p 20 of 61 U N I VERS ITY OF CALIF ORNIA AT BERKEL E Y Input Output Partitions m n N S S is a partition of S if N m n m A process P with m inputs n outputs is a subset of S S n A process with inputs and output is a relation between them A functional process is a single valued mapping a possibly m n partial function P S S A process that is functional with respect to some partition is n m determinate for B p q q S p S c o m pa r i n g f m 1996 p 21 of 61 U N I VERS ITY OF CALIF ORNIA AT BERKEL E Y Example Suppose s5 …
View Full Document
Unlocking...