Rosetta: Model-Centered Design Introduction This presentation overviews the basics of Rosetta specification You will learn Introduction to Model-centered design Rosetta types, variables, and functions Rosetta Facets, Packages and Domains Available domain types Specification composition You should be familiar with at least one HDL or high level programming language before attempting this tutorial 3/23/01 Rosetta Tutorial - IP/SoC 2001 2 Agenda History and Background Model-Centered Design Declarations, Types, and Functions Facets and Packages Domains and Domain Interactions Examples Advanced Topics 3/23/01 Rosetta Tutorial - IP/SoC 2001 3 Rosetta: Model-Centered Design Part 1 – Systems Level Design 3/23/01 Rosetta Tutorial - IP/SoC 2001 4 Why “Systems” on Chip? Increasing heterogeneity Increasing role of non-functional constraints Digital, analog, MEMs, optical on the same chip Timing, Power, Area, Packing Increasing complexity Dramatic increases in numbers of components We have seen this before in physically large systems… 3/23/01 Rosetta Tutorial - IP/SoC 2001 5 What is Systems Engineering? • Managing and integrating information from multiple domains when making design decisions • Managing constraints and performance requirements • Managing numerous large, complex systems models • Working at high levels of abstraction with incomplete information • …Over thousands of miles and many years “…the complexity of systems… have increased so much that production of modern systems demands the application of a wide range of engineering and manufacturing disciplines. The many engineering and manufacturing specialties that must cooperate on a project no longer understand the other specialties. They often use different names, notations and views of information even when describing the same concept. Yet, the products of the many disciplines must work together to meet the needs of users and buyers of systems. They must perform as desired when all components are integrated and operated.” D. Oliver, T. Kelliher, J. Keegan, Engineering Complex Systems, McGraw-Hill, 1997. 3/23/01 Rosetta Tutorial - IP/SoC 2001 6 The Systems Level Design Problem The cost of systems level information is too high… Design goals and system components interact in complex and currently unpredictable ways Interrelated system information may exist in different engineering domains (intellectually distant) Information may be spread across the system specification, in separate parts of the description Representation and analysis of high level systems models is difficult and not well supported Representation and analysis of interactions between system elements is not supported at all 3/23/01 Rosetta Tutorial - IP/SoC 2001 7 Multiple System Views P=10uW+5uW+... Architecture x of CPU is begin x <= fir(y); wait for x’event end x; Power X <= F(y) after 5us 3/23/01 Rosetta Tutorial - IP/SoC 2001 8 Multiple Semantic Models ??? 3/23/01 procedure FIR(x,z:T) begin z:= ... end FIR; Rosetta Tutorial - IP/SoC 2001 9 Component Centered Design Standard architectures for systems Systems designed by assembling components CPU Telecommunications Data book Descriptions Standard Cells Operational analysis techniques 3/23/01 Simulation Rosetta Tutorial - IP/SoC 2001 10 Model Centered Design Standard architectures for systems Systems designed by composing and analyzing models Higher level, more diversified architectures Horizontal composition for structural modeling Vertical composition for “behavioral” modeling Multiple analysis techniques 3/23/01 Operational, formal, symbolic Heterogeneous analysis Rosetta Tutorial - IP/SoC 2001 11 What is a model? A syntax for defining model elements A vocabulary of given definitions and truths An inference system for reasoning and decision making A semantics giving vocabulary and inference system meaning Engineering is applying modeling to predict system behavior… 3/23/01 Rosetta Tutorial - IP/SoC 2001 12 What is Systems Level Design? Engineering disciplines use heterogeneous modeling systems Systems level design requires information from multiple engineering disciplines Making systems level design decisions requires integrating heterogeneous models Successful systems on chip design depends on model integration 3/23/01 Rosetta Tutorial - IP/SoC 2001 13 Meta-Modeling vs Composable Models Meta-models are domain independent, high level systems models Composable models are domain specific, individual models Translate into specific tool formats for analysis One model fits all Analysis using domain specific tools Compose to define systems level descriptions Meta-modeling and composition are each necessary, but not sufficient 3/23/01 Rosetta Tutorial - IP/SoC 2001 14 Rosetta Design Goals Language and semantic support for systems level design Support for multi-facet modeling Support for multiple semantic domains Multiple views of the same component Representation of functional and constraint information Integrate components from multiple domains Integrate component views from multiple domains Support for complexity management 3/23/01 Verification condition representation Support for verification Rosetta Tutorial - IP/SoC 2001 15 Rosetta Approach Provide a means for defining and integrating systems models throughout the design lifecycle… Define facets of components and systems Provide domains for facet description Provide mechanisms for composing components and facets Specify interactions between domains reflected in facet composition 3/23/01 Rosetta Tutorial - IP/SoC 2001 16 Multi-Faceted Modeling Support for systems level analysis and decision making Rosetta domains provide modeling abstractions for developing facets and components Examples include: 3/23/01 Performance constraint modeling Discrete time modeling Continuous time modeling Finite state modeling Infinite state modeling Rosetta Tutorial - IP/SoC 2001 17 Multi-Faceted Modeling Support for modeling in heterogeneous domains Rosetta facets model different views of a system or component Power Packaging Function Safety Component 3/23/01 Rosetta Tutorial - IP/SoC 2001 18 A Simple Example… Construction of system involves multiple specialists Each specialist works from their set of plans Each specialist uses their own domain-specific information and language The systems engineer must manage overall system construction using information from all specialist domains Software EMI Electrical Power Sensor System 3/23/01 Rosetta Tutorial - IP/SoC 2001 19 Multi-Faceted Modeling Support for modeling facet interaction Rosetta interactions model when information from one domain impacts another P Performance I(x) Function ~I(x) 3/23/01 Rosetta Tutorial - IP/SoC 2001 20 A Simple Example… EMI specified at 20db Generates S/N ratio less than 5db Requirements for S/N greater than 10db EMI=20db Electrical S/N<5db Telecom S/N>10db 3/23/01 Rosetta Tutorial - IP/SoC 2001 21 Multi-Faceted Modeling Support for heterogeneous component assembly Support for interaction outside the interface Rosetta components model system structure System 3/23/01 Component Component Component Component Rosetta Tutorial - IP/SoC 2001 22 A Simple Example… Simple Satellite Downlink Each component is a Rosetta facet or component Each component may use its own domain for requirements specification Digitized Waveform Downlink System Carrier Recovery Decoding Unique Word Detect Message Recovery Message Message Parameters 3/23/01 Rosetta Tutorial - IP/SoC 2001 23 What Rosetta Provides A Language for model representation Simple syntax for parameterized model representation Language support for information hiding and component definition Representation of verification conditions and justifications A Semantics for system modeling 3/23/01 Representation of system models Representation of application domains Representation of interactions between domains Highly extensible and customizable Rosetta Tutorial - IP/SoC 2001 24 Rosetta Modeling Flow Model centered vs. component centered Choose domains of interest for the problem at hand Define facet models using domains as modeling vocabulary Assemble facet models into components and systems level models Assemble components into system specifications using structural assembly techniques Analyze components and systems using domain specific and cross-domain tools 3/23/01 Rosetta Tutorial - IP/SoC 2001 25 Anatomy of a specification Interaction System Component Facet Facet Facet Facet Domain Domain Domain Domain Interaction Component Facet Facet Facet Domain Domain Component Facet Facet Facet Domain Domain 3/23/01 Rosetta Tutorial - IP/SoC 2001 26 Rosetta Tool Architecture Front-end parser generating a semantic object model Back-end tools supporting various design capabilities MoML compatible XML interchange format Rosetta Source Rosetta Parser MATLAB Abstract Syntax Object Model Test Vectors Semantic Object Model Native Simulator Retrieval Engine Static Analysis Tools XML Interchange Format 3/23/01 Rosetta Tutorial - IP/SoC 2001 27 Rosetta: Model-Centered Design Part 2 – Types, Declarations and Functions 3/23/01 Rosetta Tutorial - IP/SoC 2001 28 Vocabulary Item – The basic unit of Rosetta semantics Type or Bunch – A collection of items Operation or Function – A mapping from an element of a domain bunch to a range bunch Variable – An item whose value is not explicitly specified Constant – An item whose value is explicitly specified Label – A name for an item Facet – An item specifying a system model 3/23/01 Rosetta Tutorial - IP/SoC 2001 29 Items Every Rosetta definition is parsed into an item Each item consists of three critical elements: For every item, M__value(I) :: M__type(I) A label naming the item A value associated with the item A type enumerating possible values The “::” relation is interpreted as “contained in” If an item’s value is fixed at parse time, it is a constant item otherwise, it is a variable item 3/23/01 Rosetta Tutorial - IP/SoC 2001 30 Bunches and Types The Rosetta type system is defined semantically using bunches The notation A::B is interpreted as “bunch A is contained in bunch B” A bunch is simply a collection of objects Any item A is a bunch as is any collection A,B,C Contained in is both “element of” and “subset” Type correctness is defined using the “contained in” concept The notation A++B is the bunch union of A and B Examples: 3/23/01 1::1++2 1++2::integers integers::numbers Rosetta Tutorial - IP/SoC 2001 31 Declarations Declarations create and associate types with items All Rosetta items must be declared before usage Declarations occur: 3/23/01 In parameter lists of functions and facets In the facet and package declaration sections In let constructs Rosetta Tutorial - IP/SoC 2001 32 Declarations Items are created using declarations having the form: label ::type [is value]; Label is the item’s name Type is a bunch defining the item’s type Value is an expression whose value is constraint to be an element of type 3/23/01 Rosetta Tutorial - IP/SoC 2001 33 Constant vs Variable Declaration Using the is construct, an item’s value is constant The following example defines an item and sets its value Value Label Pi::real is 3.14159; Type Omitting the is construct, an item’s value is variable The following example defines an item and leaves its value unspecified counter::natural; 3/23/01 Rosetta Tutorial - IP/SoC 2001 34 Example Declarations i::integer; // variable i of type integer bit_vector::sequence(bit); // variable bit_vector T::subtype(univ) // uninterpreted scalar type bit_vector8::subtype(sequence(bit)) is // 8-bit words sel(x::sequence(bit) | $x=8) natural::subtype(integer) is sel(x::integer | x >= 0); 3/23/01 // natural number definition Rosetta Tutorial - IP/SoC 2001 35 Types and Bunches Rosetta types are defined semantically as bunches The notation x::T used to declare items is the same as bunch inclusion Any bunch may serve as a type 3/23/01 Bunch operations are used to form new types from old Functions returning bunches define parameterized types Rosetta Tutorial - IP/SoC 2001 36 Predefined Scalar Types Rosetta provides a rich set of scalar types to choose from: number, real, rational, integer, natural boolean, bit character null The type element is a supertype of all scalars The types boolean and bit are subtypes of number 3/23/01 TRUE is the greatest and FALSE is the least number 0 and 1 are shared among bit and integer Rosetta Tutorial - IP/SoC 2001 37 Number Types Numerical types are all subtypes of number Standard operators on numbers are available: +,-,*,/ - Mathematical operations min, max – Minimum and maximum <,=<,>=,> - Relational operators abs, sqrt – Absolute value and square root sin,cos,tan – Trig functions exp,log – Exponentiation and log functions Subtype relationships between numbers are defined as anticipated 3/23/01 Rosetta Tutorial - IP/SoC 2001 38 The Boolean Type Booleans are the subtype of number that includes TRUE and FALSE Booleans are not bits Operations include: TRUE is a synonym for the maximum number FALSE is a synonym for the minimum number max, min and, or, not, xor implies Note that min and max are and and or respectively 3/23/01 X min Y = X and Y X max Y = X or Y Rosetta Tutorial - IP/SoC 2001 39 The Boolean Type The semantics of boolean operations follow easily from min and max TRUE and FALSE = TRUE min FALSE = FALSE TRUE or FALSE = TRUE max FALSE = TRUE TRUE and FALSE are not infinite, but use infinite mathematics: 3/23/01 TRUE+1 = TRUE TRUE = -FALSE FALSE = -TRUE Rosetta Tutorial - IP/SoC 2001 40 The Bit Type Bits are the subtype of natural numbers that include 0 and 1 Operations include similar operations as boolean: The operation % transforms between bits and booleans max, min and, or, not, xor Implies %TRUE = 1 %1 = TRUE For any bit or boolean, b, %(%b))=b The semantics of bit operations is defined by transforming arguments to booleans 3/23/01 1 and 0 = %1 and %0 = TRUE and FALSE = FALSE Rosetta Tutorial - IP/SoC 2001 41 Compound Types Compound types are formed from other types and include bunches, sets, sequences, and arrays Ordered compound types define ordering among elements Sequences and arrays are ordered Bunches and sets are not ordered Packaged types have distinct inclusion and union operators 3/23/01 Sets and arrays can contain other sets and arrays Bunches and sequences cannot contain sequences Rosetta Tutorial - IP/SoC 2001 42 Predefined Compound Types bunch(T) - The bunch of bunches formed from T set(T) – The bunch of sets formed from T sequence(T) – The bunch of sequences formed from T bitvector - Special sequence of bits string – Special sequence of characters array(T) 3/23/01 The bunch of arrays formed from T Rosetta Tutorial - IP/SoC 2001 43 The bunch Type Defined using bunch(T) or subtype(T) where T is a bunch Operations on bunch types include: 3/23/01 A++B – Bunch union A**B – Bunch intersection A--B – Bunch difference A::B – Bunch containment or inclusion $S – Size null – The empty bunch Rosetta Tutorial - IP/SoC 2001 44 The bunch Type Examples: 3/23/01 1++(2++3) = 1++2++3 1**(1++2++3) = 1 1++2::1++2++3 = TRUE 1++2::1++3 = FALSE Rosetta Tutorial - IP/SoC 2001 45 The set Type Defined using set(T) where T is a type Operations on set types include: {A} – The set containing elements of bunch A ~A – The bunch containing elements of set A A+B, A*B, A-B – Set union, intersection, difference A in B – Set membership A<B,A=<, A>=B, A>B – Proper Subset and Subset relations #A – Size empty – The empty set Sets are formed from bunches 3/23/01 The semantics of set operations is defined based on their associated bunches A+B = {~A ++ ~B} Rosetta Tutorial - IP/SoC 2001 46 The set Type Example set operations 3/23/01 {1++2} + {3} = {1++2++3} ~{1++2++3} = 1++2++3 {1++2} =< {1++2++3} (A < A) = FALSE (A =< A) = TRUE {null} = empty {1++2} = {2++1} Rosetta Tutorial - IP/SoC 2001 47 The sequence Type Defined using sequence(T) where T is a type Operations on sequence types include: 1;;2 – Concatenation head, tail – Accessors S(5) – Random access A<B, A=<B, A>=B, A>B – Containment $S – Size Sequences cannot contain sequences as elements 3/23/01 Rosetta Tutorial - IP/SoC 2001 48 The sequence Type Examples: head(1;;2;;3) = 1, tail(1;;2;;3) = 2;;3 1;;2;;3 < 1;;2;;3;;4 = TRUE 1;;3 < 1;;2;;3 = FALSE If s=4;;5;;3;;2;;1 then s(2)=3 Strings and bit vectors are special sequences 3/23/01 bitvector :: subtype(sequence(univ)) is sequence(bit); string :: subtype(sequence(univ)) is sequence(character); Rosetta Tutorial - IP/SoC 2001 49 The array Type Declared using array(T) where T is a type Operations on array types include: [1;;2;;3] – Forming an array from a sequence ~A – Extracting a sequence from an array A(1) – Random access #A – Size of array A Arrays are to sequences as sets are to bunches 3/23/01 Arrays are formed from sequences The semantics of array operations are defined based on sequences Rosetta Tutorial - IP/SoC 2001 50 The array Type Examples (assume A=[1;;2;;3]): 3/23/01 A(1) = 2 #A = 3 ~A = 1;;2;;3 A;;A = [~A;;~A] = [1;;2;;3;;1;;2;;3] Rosetta Tutorial - IP/SoC 2001 51 Aggregate Types Aggregate types are formed by grouping elements of potentially different types in the same structure Aggregate types include 3/23/01 Tuples – Structures indexed using an arbitrary type Records – Structures indexed using naturals Rosetta Tutorial - IP/SoC 2001 52 Predefined Aggregate Types Tuple [T1 | T2 | T3 | …] - The bunch of tuples formed from unlabled instances of specified types Example: Complex Numbers Tuple elements are accessed using position as in t(0) Specific tuples are formed using the notation tuple[v1 | v2 | v3 | …] c1::tuple[real | real] c1 = tuple[ 1.0 | 2.0 ] c1(0) = 1.0 Tuple declarations and formers have the same form 3/23/01 Rosetta Tutorial - IP/SoC 2001 53 Predefined Aggregate Types record [F1::T1 | F2::T2 | F3::T3 | …] - The bunch of records formed from labeled instances of types Example: Complex Numbers Record elements are accessed using field name as in R(F2) Specific records are formed using the notation record[f1 is v1 | f2 is v2 | f3 is v3 | …] c1::record[r::real | c::real] c1 = record[ r is 1.0 | c is 2.0 ] c1(r) = 1.0 Record declarations and formers have the same form 3/23/01 Rosetta Tutorial - IP/SoC 2001 54 Functions and Function Types Functions provide a means of defining and encapsulating expressions Functions are pure in that no side effects are defined No global variables No “call by reference” parameters A Rosetta function is an item whose 3/23/01 Type is a function type Value is an expression Rosetta Tutorial - IP/SoC 2001 55 Unnamed Functions and Types A unnamed functions support defining local functions and function types The notation: <* (d::D) :: R *> defines a function type that includes all mappings from D to R. The notation: <* (d::D) ::R is exp(d) *> defines a single function mapping d to exp(d) 3/23/01 Rosetta Tutorial - IP/SoC 2001 56 Formally Defining Functions A function of a particular type is defined like any other structure: f::<*(d::D)::R *> is <* (d::D)::R is exp(d) *> For example: inc::<*(j::integer)::integer*> is <*(j::integer)::integer is j+1*> This is somewhat strange and painful, so… 3/23/01 Rosetta Tutorial - IP/SoC 2001 57 Function Definition Syntax A convenient concrete syntax is defined as: f::<*(d::D)::R *> is <* (d::D)::R is exp(d) *>; == f(d::D)::R is exp(d); Increment can now be defined much more compactly as: inc(j::integer)::integer is j+1; 3/23/01 Rosetta Tutorial - IP/SoC 2001 58 Defining Functions Specific functions are defined using roughly the same mechanism as other items: F(d::D) :: R is value; where the type is a function type and value is a function type that interprets as an expression Example: increment 3/23/01 inc(n::natural)::natural is n+1; n names the input parameter n+1 defines the return value Rosetta Tutorial - IP/SoC 2001 59 Interpreting function definitions The function definition names parameters and defines a return value Function Name Function Type add(j::natural; k::natural)::natural is j+k; Parameter Names and Types 3/23/01 Return Expression Rosetta Tutorial - IP/SoC 2001 60 Basic Function Types Functions are declared using the notation: F(d::D) :: R; D is a type defining the function domain and R is an expression defining the function’s return type and ran(F) is the range of F dom(F) = D ret(F) = R ran(F) = {All possible return values} Example: Increment 3/23/01 inc(i::integer)::integer; ret(inc) = dom(inc) = integer ran(inc) = sel(i::integer | 0 < i) Rosetta Tutorial - IP/SoC 2001 61 Functions of Multiple Arguments Functions with multiple arguments are define by recursive application of the function definition: F(d1::D1; d2::D2; d3::D3 …)::R This defines a function that maps multiple values onto a single value Example: add 3/23/01 add(n1 :: natural; n2 :: natural) :: natural; dom(add) = natural;;natural; ret(add) = natural; ran(add) = natural; Rosetta Tutorial - IP/SoC 2001 62 Function Type Semantics Function types provide a means of defining signatures The semantics of a function type definition state: The function is defined only over elements of its domain The function must return an element of its range The increment example is a function that takes an integer as input and returns the integer bunch The add example is a function that 3/23/01 Takes an integer as input and returns a new function Applies the new function to the second integer argument 99.9% of the time, you can simply think of this as a two argument function Rosetta Tutorial - IP/SoC 2001 63 Examples sqrt(i::integer) :: integer; ord(c::character) :: natural; element(e1::E; s::set(E)) :: boolean; top(s1::stack) :: E; cat(s1::sequence(E); s2::sequence(E))::sequence(E); 3/23/01 Rosetta Tutorial - IP/SoC 2001 64 Example Functions // Simple 2-1 multiplexor mux(s::bit; i0::bitvector; i1::bitvector)::bitvector is if s=0 then i0 else i1 endif; // Hours increment function increment_time(m::integer)::integer is if m < 720 then minutes + 1 else 1 endif; 3/23/01 Rosetta Tutorial - IP/SoC 2001 65 Example Functions //Parameterized linear search function search(E::subtype(univ); s::sequence(E); p(e::E)::boolean)::E is if s/=null then if p(s(0)) then s(0) else search(E,tail(s),p) endif endif; search(integer,_,_) == <*(s::sequence(integer),p(e::integer)::boolean is if s/=null then if p(s(0)) then s(0) else search(integer,tail(s),p) endif; endif; *> 3/23/01 Rosetta Tutorial - IP/SoC 2001 66 Applying Functions Applying a function is a two step process Example: Replace formal parameters with actual parameters in the value expression Evaluate the value expression inc(5) = <*5+1*> = 6 add(5,2) = <*5+2*> = 7 add(5,_) = <*(m::natural) :: natural is 5+m*> add(5,_)(2) = <*(m::natural) :: natural is 5+m*>(2) = <* 5+2 *> = 7 Simply replace and simplify All parameters need not be instantiated!! 3/23/01 Rosetta Tutorial - IP/SoC 2001 67 Partial Evaluation Partial evaluation is achieved by instantiating only some of the variables Use “_” as a placeholder for uninstantiated parameters Consider the function definition: searchInt(s::sequence(integer); p::<*(e::integer)::boolean*>)::boolean; searchInt = search(integer,_,_); defines a new function that is a specialization of the general purpose search function 3/23/01 Rosetta Tutorial - IP/SoC 2001 68 Functions on Functions Many classical specification functions are defined as “functions on functions” 3/23/01 min, max - Minimum or maximum in a bunch forall and exits – Universal and existential quantification dom, ran - Domain and range over a function sel - Select or comprehension over a bunch Rosetta Tutorial - IP/SoC 2001 69 The Domain and Range Functions Domain is a simple extraction of the function domain Range is the bunch formed by application of the function to each defined domain value dom(<* (d::D)::R *>) = D dom(<* (d0::D0,d1::D1…) :: R *>) = D0;;D1;;… ran(<* (d::D)::R *>)= The bunch of the function applied to all domain values Frequently used to implement the image of a function over a bunch or set Examples: 3/23/01 dom(inc) = natural ran(inc) = natural –- 0; Rosetta Tutorial - IP/SoC 2001 70 The Minimum and Maximum Functions The min and max functions take the minimum and maximum values of a function’s range, respectively Examples: 3/23/01 min(inc)=1 max(inc)=MAXINT Rosetta Tutorial - IP/SoC 2001 71 The Quantifier Functions The forall and exists functions are shorthands for min and max respectively Both take arguments of boolean valued functions Both apply the function to each domain element The forall function takes the minimum value while exists takes the maximum value Examples 3/23/01 forall(<*(x::integer)::boolean is x>0 *>) = FALSE exists(<*(x::integer)::boolean is x>0 *>) = TRUE Rosetta Tutorial - IP/SoC 2001 72 The Quantifier Functions Because forall and exists are so common, we define a special syntax for their application: forall(x::integer | x>0) == forall(<*(x::integer)::boolean is x>0 *>) = FALSE exists(x::integer | x>0) == exists(<*(x::integer)::boolean is x>0 *>) = TRUE where the the “|” separates a variable declaration from a boolean expression defined over that variable. 3/23/01 Rosetta Tutorial - IP/SoC 2001 73 The Selection Function The sel function performs comprehension over the domain of a function Use the select function whenever comprehension or filtering is desired Examples: 3/23/01 sel(x::integer | x>=0)=natural sel(x::1++2++3++4) | 2*x=4) = 2 natural::bunch(integer) is sel(x::integer | x >= 0) Rosetta Tutorial - IP/SoC 2001 74 The Selection Function The sel function also uses a special syntax to aid comprehension sel(x::integer | x>=0) == sel(<* (x::integer)::boolean is x>=0 *>) natural::subtype(integer) is sel(<* (x::integer)::boolean is x >=0*>) == natural::subtype(integer) is sel(x::integer | x >= 0); 3/23/01 Rosetta Tutorial - IP/SoC 2001 75 Functions as Type Definitions Functions can be used to define parameterized types boundedBitvector(n::natural)::subtype(bitvector) is sel(b::bitvector | $b = n); The function can now be used to define new types because its return value is a bunch: bitvector8::subtype(bitvector) is boundedBitvector(8); bitvector8 is the type containing all bitvectors of length 8 3/23/01 Rosetta Tutorial - IP/SoC 2001 76 Rosetta: Model-Centered Design Part 3 – Facets, Packages and Components 3/23/01 Rosetta Tutorial - IP/SoC 2001 77 Facets, Packages and Components Facets define basic system and component models Packages group definitions Parameters provide communications and design specialization Declaration areas provide for local item definitions A domain identifies the vocabulary Terms provide for the semantics of the facet model Packages are special facets without terms Packages group definitions into parameterized modules Components provide a standard definition style for system components 3/23/01 Components record design assumptions Components record correctness assertions Rosetta Tutorial - IP/SoC 2001 78 Understanding Facet Definitions Facets and packages provide mechanisms for defining models and grouping definitions Facet Name Variables Terms 3/23/01 Parameter List facet trigger(x::in real; y::out bit) is s::bit; Domain begin continuous t1: if s=1 then if x>=0.4 then s’=1 else s’=0 endif else if x=<0.7 then s’=0 else s’=1 endif endif; t2: y@t+10ns=s; end trigger; Rosetta Tutorial - IP/SoC 2001 79 Facet Name and Parameters The facet name is a label used to reference the facet definition Facet parameters are formal parameters that represent an interface to the component Parameters provide a means for model specialization Parameters provide a means for model communication Parameters are instantiated by providing actual values when a facet is used trigger(input,output); 3/23/01 Rosetta Tutorial - IP/SoC 2001 80 Trigger Label and Parameters The label trigger names the facet The parameters x and y define inputs and outputs for the facet facet trigger(x::in real; y::out bit) is The direction indicators in and out define the behavior of parameters by asserting in(x) and out(x) as terms 3/23/01 Rosetta Tutorial - IP/SoC 2001 81 Facet Declarations Facet declarations are items defined within the scope of the facet When exported, declarations are referenced using the canonical “.” notation as in trigger.s When not exported, declarations cannot be referenced outside the facet Declarations are visible in all facet terms Items are declared in the manner defined previously 3/23/01 Item values may be declared constant Item types include all available Rosetta types including facets, functions and types Rosetta Tutorial - IP/SoC 2001 82 Trigger Facet Declarations The local variable s declares a bit visible throughout the facet No export clause is present, so all labels are visible facet trigger(x::in real; y::out bit) is s::bit; begin continuous In this specification, s defines the instantaneous state of the component 3/23/01 Rosetta Tutorial - IP/SoC 2001 83 Facet Domain The facet domain provides a base vocabulary and semantics for the specification Current domains include 3/23/01 Logic and mathematics Axiomatic state based Finite state Infinite state Discrete and continuous time Constraints Mechanical Rosetta Tutorial - IP/SoC 2001 84 Trigger Domain The trigger facet uses the continuous domain for a specification basis The continuous domain provides a definition of time as a continuous, real value facet trigger(x::in real; y::out bit) is s::bit; begin continuous 3/23/01 Rosetta Tutorial - IP/SoC 2001 85 Facet Terms A term is a labeled expression that defines a property for the facet Terms may be, but are not always executable structures Simple definition of factual truths Inclusion and renaming if existing facets Terms simply state truths Term visibility is managed like variable visibility 3/23/01 If exported, the term is referenced using the “.” notation If not exported, the term is not visible outside the facet Rosetta Tutorial - IP/SoC 2001 86 Trigger Terms Terms define the state value and the output value t1: if s=1 then if x>=0.4 then s’=1 else s’=0 endif else if x=<0.7 then s’=0 else s’=1 endif endif; t2: y@t+10ns=s; Term t1 defines the state in terms of the current state and the current inputs Term t2 defines that the output should be equal to the state value 10ns in the future The continuous domain provides the semantics for time and the semantics of the reference function @ 3/23/01 Rosetta Tutorial - IP/SoC 2001 87 Trigger Terms Both trigger terms are executable and state equalities T1 places constraints on the value of state with respect to the current inputs T2 places constraints on the value of output 10 nanoseconds in the future Other domains provide other mechanisms for specification semantics 3/23/01 Rosetta Tutorial - IP/SoC 2001 88 Packages A package is a special purpose facet used to collect, parameterize and reuse definitions Package Name Package Definitions 3/23/01 Package Parameters package wordTypes(w::natural) is begin logic Package Domain word::subtype(bitvector) is boundedBitvector(w); word2nat(w::word)::natural is … facet wordAdder(x,y::word)::word is … end wordTypes; Rosetta Tutorial - IP/SoC 2001 89 Package Semantics Packages are effectively facets without terms All elements of the package are treated as declarations All package definitions are implicitly exported The package domain works identically to a facet domain Instantiating the package replaces formal parameters with actual parameters 3/23/01 Rosetta Tutorial - IP/SoC 2001 90 The wordType Package The wordType package defines A type word A function for converting words to naturals A facet defining a word adder All definitions are parameterized over the word width specified by w 3/23/01 Using wordType(8) defines a package supporting 8 bit words Rosetta Tutorial - IP/SoC 2001 91 Rosetta: Model-Centered Design Part 4 – Domains 3/23/01 Rosetta Tutorial - IP/SoC 2001 92 Domains and Interactions Domains provide domain specific definition capabilities Design abstractions Design vocabulary Interactions define how specifications in one domain affect specifications in another 3/23/01 Rosetta Tutorial - IP/SoC 2001 93 The Logic Domain The logic domain provides a basic set of mathematical expressions, types and operations 3/23/01 Basic types and operations with little extension Best thought of as the domain used to provide basic mathematical structures Currently, all domains inherit from the logic domain Rosetta Tutorial - IP/SoC 2001 94 The State-Based Domain The state-based domain supports defining behavior by defining properties in the current and next state Basic additions in the state-based domain include: 3/23/01 S – The state type next(s1::S)::S; – Relates the current state to the next state x@s - Value of x in state s x’ – Standard shorthand for x@next(s) Rosetta Tutorial - IP/SoC 2001 95 Defining State Based Specifications Define important elements that define state Define properties in the current state that specify assumptions for correct operation Define properties in the next state that specify how the model changes it’s environment Frequently called a precondition Frequently called a postcondition Define properties that must hold for every state 3/23/01 Frequently called invariants Rosetta Tutorial - IP/SoC 2001 96 Example: Unique Word Detector facet unique_word(b::in bit; enable::in bit; word::in bitvector; clear::in bit; hit::out bit) is x::bitvector; begin state_based l1: %enable implies (x’=(b;;x)); // Update state l2: hit’ = %(x=word)*enable; // Generate output l3: %clear implies (x’=nil); // Reset indicated end unique_word; 3/23/01 Rosetta Tutorial - IP/SoC 2001 97 Understanding the Unique Word Detector State is the last n-bits seen by the detector Update the state by adding the most recent bit The output is ‘1’ if the stored word and the unique word match l1: %enable implies (x’=(b;;x)); l2: hit’ = %(x=word)*enable; If the reset signal is asserted, then reset the stored word 3/23/01 l3: %clear implies (x’=nil); // Reset indicated Rosetta Tutorial - IP/SoC 2001 98 When to Use the State-based Domain Use state-based specification when: When a generic input/output relation is known without detailed specifics When specifying software components Do not use state-based specification when: 3/23/01 Timing constraints and relationships are important Composing specifications is anticipated Rosetta Tutorial - IP/SoC 2001 99 The Finite State Domain The finite-state domain supports defining systems whose state space is known to be finite The finite-state domain is a simple extension of the state-based domain where: 3/23/01 S is defined to be or is provably finite Rosetta Tutorial - IP/SoC 2001 100 Example: Schmidt Trigger Specification facet trigger(i:: in real; o:: out bit) is S::subtype(natural) is 0++1; begin state_based L1: next(0) = if i>=0.7 then 1 else 0 endif; L2: next(1) = if i=<0.3 then 0 else 1 endif; L3: o’=S; end trigger; 3/23/01 Rosetta Tutorial - IP/SoC 2001 101 Understanding the Schmidt Trigger There are two states representing the current output value The next state is determined by the input and the current state S::subtype(integer) is 0++1; L1: next(0) = if i>=0.7 then 1 else 0 endif; L2: next(1) = if i=<0.3 then 0 else 1 endif; The output is the state 3/23/01 L3: o’=S; Rosetta Tutorial - IP/SoC 2001 102 When to Use the Finite State Domain Use the finite-state domain when: Specifying simple sequential machines When it is helpful to enumerate the state space Do not use the finite-state domain when 3/23/01 The state space cannot be proved finite The specification over specifies the properties of states and the next state function Rosetta Tutorial - IP/SoC 2001 103 The Infinite State Domain The infinite-state domain supports defining systems whose state spaces are infinite The infinite-state domain is an extension to the state-based domain and adds the following axiom: next(s) > s The infinite-state domain asserts a total ordering on the state space 3/23/01 A state can never be revisited Rosetta Tutorial - IP/SoC 2001 104 The Discrete Time Domain The discrete-time domain supports defining systems in discrete time The discrete-time domain is a special case of the infinite-state domain with the following definition next(t)=t+delta; The constant delta>=0 defines a single time step The state type T is the set of all multiples of delta All other definitions remain the same 3/23/01 next(t) satisfies next(t)>t Rosetta Tutorial - IP/SoC 2001 105 Example: Discrete Time Pulse Processor facet pp_function(inPulse::in PulseType; o::out command) is use pulseTypes; pulseTime :: T; pulse :: PulseType; begin discrete_time L1: if (pulse = none) then (pulseTime’ = t) and (pulse’ = inPulse) endif; L2: (pulse=A1) and (inPulse=A2) => (pulse@next(t)=none); L3: (pulse=A1) and (inPulse=A1) => (pulse@next(t)=none) and (o@t+2*delta=interpret(pulseTime,t)); end pp_function; 3/23/01 Rosetta Tutorial - IP/SoC 2001 106 Understanding the Pulse Processor Each state is associated with a discrete time value Event times are constrained Time properties account for preconditions and invariants The next function is defined as previously 3/23/01 Can reference arbitrary time spaces Rosetta Tutorial - IP/SoC 2001 107 Understanding the Pulse Processor State is the last pulse received and its arrival time or none If there is no stored pulse, store the pulse time and type L1: if (pulse = none) then (pulseTime’ = t) and (pulse’ = inPulse) endif; If the initial pulse is of type A1 and the arriving pulse is of type A2, reset and wait for another pulse L2: (pulse=A1) and (inPulse=A2) implies (pulse@next(t)=none); If the initial pulse is of type A1 and the arriving pulse if of type A1, then output command in under 2 time quanta L3: (pulse=A1) and (inPulse=A1) implies (pulse@next(t)=none) and (o@t+2*delta=interpret(pulseTime,t)); 3/23/01 Rosetta Tutorial - IP/SoC 2001 108 When to Use the Discrete Time Domain Use the discrete-time domain when: Specifying discrete time digital systems Specifying concrete instances of systems level specifications Do not use the discrete-time domain when: 3/23/01 Timing is not an issue More general state-based specifications work equally well Rosetta Tutorial - IP/SoC 2001 109 The Continuous Time Domain The continuous-time domain supports defining systems in continuous time The continuous-time domain has no notion of next state The time value is continuous – no next function The “@” operation is still defined 3/23/01 Alternatively define functions over t in the canonical fashion Derivative, indefinite and definite integrals are available Rosetta Tutorial - IP/SoC 2001 110 Example: Continuous Time Servovalve facet servovalve_fcn(U::real; P_S::posReal; Q_1, Q_2 :: real; U_max::design posReal; b::design posReal; rho::design posReal; c_d::design posReal) is P :: real is P_2-P_1; Q :: real is (Q_1+Q_2)/2; Q_max :: real is U_max * b * c_d * (P_s/rho)^0.5; sgn(x::real)::real is if (x /= 0) then x/abs(x) else 0.0 endif; begin continuous // Functional definition of a servovalve F1: Q/Q_max=U/U_max * ((1 - P/P_S) * sgn(U/U_max))^0.5; //Constraints - flow, spool disp, diff pressure cannot exceed max C1: abs(Q) =< abs(Q_max); C2: abs(U) =< abs(U_max); C3: abs(P) =< abs(P_S); end servovalve_fcn; 3/23/01 Rosetta Tutorial - IP/SoC 2001 111 Understanding the Servovalve Specification Parameters define: Internal parameters and functions define intermediate values and shorthand notations P defines differential pressure sgn defines a signum function Functional equations define behavior Instantaneous flows and pressures Servovalve design parameters F1: Q/Q_max=U/U_max * ((1 - P/P_S) * sgn(U/U_max))^0.5; Constraints define performance related requirements 3/23/01 C1: abs(Q) =< abs(Q_max); C2: abs(U) =< abs(U_max); Rosetta Tutorial - IP/SoC 2001 112 Using the Continuous Time Domain Use the continuous-time domain when Arbitrary time values must be specified Describing analog, continuous time subsystems Do not use the continuous-time domain when: 3/23/01 Describing discrete time systems State based specifications would be more appropriate Rosetta Tutorial - IP/SoC 2001 113 Specialized Domain Extensions The domain mechanical is a special extension of the logic and continuous time domains for specifying mechanical systems The domain constraints is a special extension of the logic domain for specifying performance constraints Other extensions of domains are anticipated to represent: 3/23/01 New specification styles New specification domains such as optical and MEMS subsystems Rosetta Tutorial - IP/SoC 2001 114 Rosetta: Model-Centered Design Part 5 – Composition and Interaction 3/23/01 Rosetta Tutorial - IP/SoC 2001 115 Specification Composition Compose facets to define multiple models of the same component Using the facet algebra Components Compose facets to define systems structurally 3/23/01 Including facets as terms Instantiating facets Channels and models of computation Rosetta Tutorial - IP/SoC 2001 116 Facet Semantics The semantics of a facet is defined by its domain and terms The domain defines the formal system associated with the facet The terms extend the formal system to define the facet An interaction defines when information from one domain effects another A Rosetta specification defines and composes a collection of interacting models 3/23/01 Rosetta Tutorial - IP/SoC 2001 117 Formal Systems A formal system consists of the following definitions: A formal language An inference mechanism A set of grammar rules A set of atomic symbols A set of axioms A set of inference rules A semantic basis In Rosetta, these elements are defined in the domain specification 3/23/01 Language and inference mechanism are relatively fixed Semantics varies widely from domain to domain Rosetta Tutorial - IP/SoC 2001 118 Semantic Notations The semantics of a facet F is defined as an ordered pair (DF,TF) where: DF defines the domain (formal system) of the specification TF defines the term set defining the specification A facet definition is consistent if TF extends DF conservatively 3/23/01 FALSE cannot be derived from TF using DF Rosetta Tutorial - IP/SoC 2001 119 Facet Conjunction Facet conjunction defines new facets with properties of both original facets F G F and G Facet F and G reflects the properties of both F and G simultaneously Formally, conjunction is defined as the co-product of the original facets 3/23/01 Rosetta Tutorial - IP/SoC 2001 120 Facet Conjunction Example facet pp_function(inPulse::in PulseType; o::out command) is use pulseTypes; pulseTime :: T; pulse :: PulseType; begin discrete_time L2: (pulse=A1) and (inPulse=A2) => (pulse’=none); L3:(pulse=A1) and (inPulse=A1) => (pulse’=none) and (o@t+2*delta=interpret(pulseTime,t)); end pp_function; facet pp_constraint is power::real; begin constraints c1: power=<10mW; c2: event(inPulse) <–> event(o) =< 10mS; end pp_constraint; 3/23/01 Rosetta Tutorial - IP/SoC 2001 121 Facet Conjunction Example Define a new pulse processor that exhibits both functional and constraint properties: facet::pp is pp_function and pp_constraints; The new pp facet must exhibit correct function and satisfy constraints 3/23/01 Functional properties and heat dissipation are independent Functional properties and timing constraints are not independent Rosetta Tutorial - IP/SoC 2001 122 When to Use Facet Conjunction When a component or system should exhibit two sets of properties When a component or system should exhibit two orthogonal functions 3/23/01 Rosetta Tutorial - IP/SoC 2001 123 Understanding Facet Conjunction Given two facets F and G the conjunction F and G might be defined formally as: F and G = {(DF,TF),(DG,TG)} The conjunction is literally a facet consisting of both models If F and G are orthogonal, this definition works fine F and G are rarely orthogonal Orthogonality makes things rather uninteresting Thus we define an interaction 3/23/01 Rosetta Tutorial - IP/SoC 2001 124 Understanding Facet Conjunction Given two facets F and G the conjunction F and G is defined formally as: F and G = {(DF,TF+M__I(G,F)),(DG,TG+M__I(F,G))} The interaction function, M__I, maps terms from one domain into terms from another An interaction defines the function M__I for a domain pair A projection extracts the model associated with a domain from a facet: M__proj((F and G),DG)=(DG, TG+M__I(F,G)) 3/23/01 Rosetta Tutorial - IP/SoC 2001 125 Domain Interaction Semantics Composition forms co-product F Interaction defines effects of information from domain Df on domain Dg defining F’ G F and G F’ Interaction defined using Rosetta’s reflective capabilities 3/23/01 G’ Projections form product Rosetta Tutorial - IP/SoC 2001 126 Understanding Facet Conjunction Composing facets from the same domain uses the same semantics as Z specification composition A and B – All terms from both facts are true A or B – Conjunctions of terms from facets are disjuncted If the conjunction of two facets does not generate new terms, then those facets are orthogonal with respect to conjunction 3/23/01 This is important as it can reduce analysis complexity stubstantially Rosetta Tutorial - IP/SoC 2001 127 Interaction Definitions An interaction is a special package that defines M__I for two domains: Interaction Operation Domains Interaction Function 3/23/01 interaction and(state_based,logic::domain) is begin interaction Interaction Domain M__I(f::logic,g::state_based)::set(term) is {ran(t::M__terms(f) | ran(s::g.S | t@s))} M__I(g::state_based,f::logic)::set(term) is {sel(t::M__terms(g) | forall(s::g.S | t@s))} end and; Rosetta Tutorial - IP/SoC 2001 128 Understanding Facet Conjunction After taking a deep breath… The interaction explains how domains affect each other The projection extracts a facet from a particular domain from another facet To understand how domains interact 3/23/01 Form the composition using interactions Project the result into the domain of interest The results of the interaction are presented in the domain of interest Rosetta Tutorial - IP/SoC 2001 129 Facet Disjunction Facet disjunction defines a new facet with properties of either original facet F G F or G Facet F or G reflects the properties of either F or G Formally, disjunction is defined as the product of the original facets 3/23/01 Rosetta Tutorial - IP/SoC 2001 130 Facet Disjunction Example facet pp_function(inPulse::in PulseType; o::out command) is use pulseTypes; pulseTime :: T; pulse :: PulseType; begin discrete_time L2: (pulse=A1) and (inPulse=A2) => (pulse’=none); L3:(pulse=A1) and (inPulse=A1) => (pulse’=none) and (o@t+2*delta=interpret(pulseTime,t)); end pp_function; facet pp_constraint is power::real; begin constraints c1: power=<10mW; c2: event(inPulse) <–> event(o) =< 10mS; end pp_constraint; 3/23/01 Rosetta Tutorial - IP/SoC 2001 131 Facet Disjunction Example facet pp_lp_constraint is power::real; begin constraints c1: power=<5mW; c2: event(inPulse) <–> event(o) =< 15mS; end pp_lp_constraint; A component that satisfies functional requirements and either constraint set is defined: pp::facet is pp_function and (pp_lp_constraint or pp_constraint) pp is a component that represents either the normal or low power device 3/23/01 Rosetta Tutorial - IP/SoC 2001 132 When to Use Facet Disjunction When a component may exhibit multiple sets of properties When representing a family of components 3/23/01 Rosetta Tutorial - IP/SoC 2001 133 Facet Declarations Facets may be defined in the same manner as other items: f::facet [is facet-expression]; The type facet is the bunch of all possible facets facet-expression is an expression of type facet Can also define a variable facet without a predefined value: f::facet; 3/23/01 Rosetta Tutorial - IP/SoC 2001 134 Component Aggregation System decomposition and architecture are represented using aggregation to represent structure Propagate system properties onto components Include and rename instances of components Interconnect components to facilitate communication Label distribution Aggregation approach 3/23/01 Include facets representing components Rename to preserve internal naming properties Communicate through sharing actual parameters Use label distribution to distribute properties among components Rosetta Tutorial - IP/SoC 2001 135 Facet Inclusion Include and rename facets to represent components rx:rx_function(i,p) includes rx_function and renames it rx Access labels in rx using rx.label not rx_function.label Achieves instance creation with little semantic effort Use internal variables to achieve perfect, instant communication facet iff_function(i::in signal; o::out signal) is p::pulseType; c::command; begin logic rx: rx_function(i,p); pp: pp_function(p,c); tx: tx_function(c,o); end iff_function; 3/23/01 Rosetta Tutorial - IP/SoC 2001 136 Facet Inclusion The same technique works for facets of any variety Consider a structural definition of component constraints facet iff_constraint is power::real; begin logic rx: rx_constraint; pp: pp_constraint; tx: tx_constraint; p: power = rx.power+pp.power+tx.power; end iff_constraint; 3/23/01 Rosetta Tutorial - IP/SoC 2001 137 Label Distribution Labels distribute over most logical and facet operators: L: L: L: L: term1 term1 term1 term1 and L:term2 == L: term1 and term2 or L:term2 == L: term1 or term2 => L:term2 == L: term1 => term2 = L:term2 == L: term1 = term2 Consequences when conjuncting structural definitions are interesting 3/23/01 Rosetta Tutorial - IP/SoC 2001 138 Conjuncting Structural Definitions facet iff_function(i::in signal; o::out signal) is p::pulseType; c::command; begin logic facet iff_constraint is rx: rx_function(i,p); power::real; pp: pp_function(p,c); begin logic tx: tx_function(c,o); rx: rx_constraint; end iff_function; pp: pp_constraint; tx: tx_constraint; p: power = rx.power+…; end iff_constraint; iff::facet is iff_function and iff_constraint 3/23/01 Rosetta Tutorial - IP/SoC 2001 139 Combining Terms facet iff_function(i::in signal; o::out signal) is p::pulseType; c::command; power::real; begin logic rx: rx_function(i,p); pp: pp_function(p,c); tx: tx_function(c,o); rx: rx_constraint; pp: pp_constraint; tx: tx_constraint; p: power = rx.power+…; end iff_function; 3/23/01 Rosetta Tutorial - IP/SoC 2001 140 Applying Label Distribution facet iff_function(i::in signal; o::out signal) is p::pulseType; c::command; power::real; begin logic rx: rx_function(i,p) and rx: rx_constraint; pp: pp_function(p,c) and pp: pp_constraint; tx: tx_function(c,o) and tx: tx_constraint; p: power = rx.power+…; end iff_function; facet iff_function(i::in signal; o::out signal) is p::pulseType; c::command; power::real; begin logic rx: rx_function(i,p) and rx_constraint; pp: pp_function(p,c) and pp_constraint; tx: tx_function(c,o) and tx_constraint; p: power = rx.power+…; end iff_function; 3/23/01 Rosetta Tutorial - IP/SoC 2001 141 Label Distribution Results In the final specification, component requirements coalesce based on common naming 3/23/01 Using common architectures causes components to behave in this way Systems level requirements are “automatically” associate with components Rosetta Tutorial - IP/SoC 2001 142 Component Families Parameters can be used to select from among component options when combined with if constructs Leaving the select parameter open forces both options to be considered. facet iff_constraint(lp::in boolean) is power::real; begin logic rx: rx_constraint; pp: if lp then pp_lp_constraint else pp_constraint endif; tx: tx_constraint; p: power = rx.power+…; end iff_constraint; 3/23/01 Rosetta Tutorial - IP/SoC 2001 143 Avoiding Information Hiding The use clause allows packages and facets to be included in the declaration section All exported labels in used packages and facets are added to the name space of the including facet The use clause must be used carefully: 3/23/01 All encapsulation is lost Includes at the item level rather than the facet level Used primarily to include definitions from standard packages and libraries Rosetta Tutorial - IP/SoC 2001 144 An Example Rosetta Specification Simple Alarm Clock synthesis benchmark We will define: 3/23/01 Requirements specifications with timing constraints Component specification and structure Power and clock speed constraints Composite, heterogeneous, systems-level specification Rosetta Tutorial - IP/SoC 2001 145 Rosetta: Model-Centered Design Part 6 – Alarm Clock Example 3/23/01 Rosetta Tutorial - IP/SoC 2001 146 Alarm Clock Representation setAlarm alarmToggle timeInHr timeInMin setTime Store alarmTime timeInMin timeInHr alarmOn clockTime setAlarm MUX Counter/Comparator setTime displayTimeHr displayTimeMin 3/23/01 alarm Rosetta Tutorial - IP/SoC 2001 clockTime 147 Alarm Clock Overview When the setTime bit is set, (timeInHr*60 + timeInMin) is stored as the clockTime; timeInHr & timeInMin are output as the display time. When the setAlarm bit is set, the (timeInHr*60 + timeInMin) is stored as the alarmTime timeInHr & timeInMin are output as the display time. When the alarmToggle bit is set, the alarmOn bit is toggled. When clockTime and alarmTime are equivalent and alarmOn is high, the alarm should be sounded. Otherwise it should not. When setTime is clear and setAlarm is clear, clockTime is output as the display time. The clock always increments its time value. 3/23/01 Rosetta Tutorial - IP/SoC 2001 148 Rosetta Specification Overview timeTypes defines basic types and functions alarmClockBeh defines real-time functional requirements Terms define functional requirements Hard real-time constraints specified using continuous time domain alarmClockStruct defines the structure of an implementation alarmClockConst defines a collection of constraints Individual facets describe separate constraints Conjunction used for facet assembly When alarmClockLP defines a low power alarm clock Behavioral description asserts function and real-time constraints Structural description asserts a structure Constraints force a low power model Conjunction asserts all requirements simultaneously 3/23/01 Rosetta Tutorial - IP/SoC 2001 149 Systems Level Alarm Clock (I) // Systems level specification of the overall alarm clock behavior package AlarmClockBeh is begin logic use TimeTypes; facet alarmclockbeh(timeInHr::in integer; timeInMin:: in integer; displayTimeHr::out integer; displayTimeMin::out integer; alarm::out bit; setAlarm::in bit; setTime::in bit; alarmToggle::in bit;reset::in bit) is alarmTime :: integer; clockTime :: integer; alarmOn :: bit; begin state_based setclock_label: if %setTime then (clockTime' = (timeInHr * 60 + timeInMin)) and (displayTimeHr' = timeInHr) and (displayTimeMin' = timeInMin) else clockTime' = increment_time(clockTime) endif; 3/23/01 Rosetta Tutorial - IP/SoC 2001 150 Systems Level Alarm Clock (II) // Behavioral model continued… setalarm_label: if %setAlarm then (alarmTime' = (timeInHr * 60 + timeInMin)) and (displayTimeHr' = timeInHr) and (displayTimeMin' = timeInMin) else alarmTime' = alarmTime endif; displayClockLabel: (setTime = 0) and (setAlarm = 0) => (displayTimeHr' = div(clockTime', 60)) and (displayTimeMin' = mod(clockTime', 60)); 3/23/01 Rosetta Tutorial - IP/SoC 2001 151 Systems Level Alarm Clock (III) // Behavioral model concluded armalarm_label: if (reset == 1) then (alarmOn' = 0) else if (alarmToggle = 1) then (alarmOn' = -alarmOn) else (alarmOn' = alarmOn) endif endif; sound_label: alarm' = if (alarmOn==1) and (alarmTime' = clockTime') then 1 else 0 endif; end alarmclockbeh; end AlarmClockBeh; 3/23/01 Rosetta Tutorial - IP/SoC 2001 152 Time Types Package // Basic times used for component and system specifications package TimeTypes is begin logic // Incrementing hours is modulo 12 arithmetic assuming minutes are // current 59 increment_time(minutes::integer)::integer is if minutes < 720 then minutes + 1 else 1 endif; export all; end TimeTypes; 3/23/01 Rosetta Tutorial - IP/SoC 2001 153 Display Multiplexer (I) // mux routes the proper value to the display output based on the // settings of the setAlarm and setTime inputs. package Mux is begin logic use TimeTypes; facet mux(timeInHr::in integer; timeInMin::in integer; displayTimeHr::out integer; displayTimeMin::out integer; clockTime::in integer; setAlarm::in bit; setTime::in bit) is begin state_based l1: %setAlarm => (displayTimeHr' = timeInHr) and (displayTimeMin' = timeInMin); 3/23/01 Rosetta Tutorial - IP/SoC 2001 154 Display Multiplexer (II) //mux continued l2: %setTime => (displayTimeHr' = timeInHr) and (displayTimeMin' = timeInMin); l3: (-(%setTime xor %setAlarm)) => (displayTimeHr' = div(clockTime, 60)) and (displayTimeMin' = mod(clockTime, 60)); end mux; export all; end Mux; 3/23/01 Rosetta Tutorial - IP/SoC 2001 155 Alarm State Storage (I) // store either updates the clock state or makes it invariant based // on the setAlarm and setTime inputs. Outputs are invariant if // their associated set bits are not high. package Store is begin logic use TimeTypes; facet store(timeInHr::in integer; timeInMin ::in integer; setAlarm::in bit; setTime::in bit; alarmToggle::in bit; clockTime::out integer; alarmTime::out integer; alarmOn::out bit) is begin state_based l1: if %setAlarm then alarmTime' = (timeInHr * 60 + timeInMin) else alarmTime' = alarmTime endif; 3/23/01 Rosetta Tutorial - IP/SoC 2001 156 Alarm State Storage (II) //Store continued l2: if %setTime then clockTime' = (timeInHr * 60 + timeInMin) else clockTime' = clockTime endif; l3: if %alarmToggle then alarmOn' = -alarmOn else alarmOn' = alarmOn endif; end store; export all; end Store; 3/23/01 Rosetta Tutorial - IP/SoC 2001 157 Counter/Comparator (I) // counter increments the current time package Counter_comparator is begin logic use TimeTypes; facet counter(clockTime :: inout integer) is begin state_based l4: clockTime' = increment_time (clockTime); end counter; 3/23/01 Rosetta Tutorial - IP/SoC 2001 158 Counter/Comparator (II) //Counter/comparator continued // comparator decides if the alarm should be sounded basedon the // setAlarm control input and if the alarmtime and clockTime are // equal. facet comparator(setAlarm:: in bit; alarmTime:: in integer; clockTime:: in integer; alarm:: out bit) is begin state_based l1: alarm = %((%setAlarm) and (alarmTime=clockTime)) ; end comparator; export all; end Counter_comparator; 3/23/01 Rosetta Tutorial - IP/SoC 2001 159 Structural Definition (I) // Structural definition combining store, comparator, and MUX definitions package AlarmClockStruct is begin logic use TimeTypes; use Store; use Counter_comparator; use Mux; facet alarmClockStruct(timeInHr::in integer; timeInMin::in integer; displayTimeHr::out integer; displayTimeMin::out integer; alarm::out bit; setAlarm::in bit; setTime::in bit; alarmToggle::in bit) is clockTime :: integer; alarmTime :: integer; alarmOn :: bit; begin logic store_1 : store(timeInHr, timeInMin, setAlarm, setTime, alarmToggle, clockTime, alarmTime, alarmOn); counter_1 : counter(clockTime); 3/23/01 Rosetta Tutorial - IP/SoC 2001 160 Structural Definition (II) //Structural definition continued comparator_1 : comparator(setAlarm, alarmTime, clockTime, alarm); mux_1 : mux(timeInHr, timeInMin, displayTimeHr, displayTimeMin, clockTime, setAlarm, setTime); end alarmClockStruct; end AlarmClockStruct; 3/23/01 Rosetta Tutorial - IP/SoC 2001 161 Constraints Definitions // Alarm clock power constraints facet alarmClockPower(lp::design boolean) is p::power; begin constraints pwr: if lp then p=<10mW else p=<40mW endif; end alarmClockPower; // Alarm clock clockspeed constraints facet alarmClockClkspd is clockspeed::frequency; begin constraints clk: clockspeek =< 1MHz; end alarmClockClkspd; // Combined constraints specifications alarmClockConst(lp::design boolean)::facet = alarmClockPower(lp) and alarmClockClkspd; 3/23/01 Rosetta Tutorial - IP/SoC 2001 162 Low Power and Mixed Specification // Low Power alarm clock alarmClockLP :: facet is alarmClockStruct and alarmClockBeh and alarmClockConst(TRUE); // Variable mode alarm clock alarmClock(pm::design boolean) :: facet is alarmClockStruct and alarmClockBeh and and alarmClockConst(pm); 3/23/01 Rosetta Tutorial - IP/SoC 2001 163 Rosetta: Model-Centered Design Part 7 – Advanced Topics 3/23/01 Rosetta Tutorial - IP/SoC 2001 164 Advanced Topics Reflection and meta-level operations Architecture definition Complex Communication Information to be provided at the tutorial based on student interest 3/23/01 Rosetta Tutorial - IP/SoC 2001 165 Meta-Level Operations Rosetta Meta-level operations allow specifications to reference specifications All Rosetta items have the following meta-level information: M__type(I) – Type of item I M__label(I) – Label of item I M__value(I) – Value of item I M__string(I) – Printed form of item I Specific items are defined using specialized operators 3/23/01 Rosetta Tutorial - IP/SoC 2001 166 Architecture Definition Facets parameterized over facets supply architecture definitions: Type parameter Internal connection 3/23/01 facet batch_seq(T::design subtype(univ); x::in T; z::out T; f1,f2::facet) is a::M__type(f1.z); begin logic Structure c1:f1(x,a); definition c2:f2(a,z); tc1:M__type(a) <= M__type(f2.x); tc2:T <= M__type(f1.x); Type constraints tc3:M__type(f2.z) <= T; end batch_seq; Rosetta Tutorial - IP/SoC 2001 167 Batch Sequential Architecture Graphical representation showing flow through the system architecture Type soundness conditions arise from architecture definition batch_seq x::T x::T f1 z::R a::R x::S f2 z::T z::Q R<=S – Flow from F1 to F2 Q<=T – Flow from F2 to system output T<=T – Flow from system input to F1 3/23/01 Rosetta Tutorial - IP/SoC 2001 168 Instantiating Architectures Search for an integer in a sequence by sorting followed by binary search find(x::in seqence(integer); k::integer; z::out boolean) :: facet is batch_seq(sequence(integer),sort,bin_search(_,k,_)); Instantiate the input type with sequence(integer) Instantiate the first component with sort Instantiate the second component with a bin-search Instantiate search key with component key input Do not instantiate input or output sequences explicitly 3/23/01 Rosetta Tutorial - IP/SoC 2001 169 Available Component Descriptions Sorting Component facet sort( x::in sequence(integer); z::out sequence(integer)) z::sequence(integer) Binary search component facet bin_search( x::in sequence(integer); k::in integer; z::out sequence(integer)) x::sequence(integer) sort bin_search x::sequence(integer) k::integer 3/23/01 Rosetta Tutorial - IP/SoC 2001 z::boolean 170 Instantiated Architecture find a::sequence(integer) z::sequence(integer) x::sequence(integer) k::integer x::sequence(integer) sort bin_search x::sequence(integer) k::integer z::boolean z::boolean R<=S == sequence(integer) <= sequence(integer) sort output is type compatible with bin-search input Q<=T == boolean <= boolean bin-search output is type compatible with component output T=T == sequence(integer)<=sequence(integer) Component input is type compatible with sort input 3/23/01 Rosetta Tutorial - IP/SoC 2001 171 Communications Channels Communications is achieved through shared variables Parameters with in and out modifiers represent directional channels similar to VHDL and are referred to as ports Parameters with no modifier represent directionless interfaces Parameters with design modifiers represent generic parameters Communications channels are modeled using shared items 3/23/01 Abstract data types provide behavior Timing model is taken from the component domain Rosetta Tutorial - IP/SoC 2001 172 Simple Mailbox Style Communication Achieved by constraining a port in the next state All constraints on a variable are applied in a given state Sharing between facets implies that constraints from both facets apply The following facet defines an and gate that uses simple mailbox communication facet andGate(x,y::in bit, z::out bit) is begin state_based l1: z’=x*y; end andGate; 3/23/01 Rosetta Tutorial - IP/SoC 2001 173 Buffered Channels Buffered communications is implemented using sequences A channel abstraction is provided for clarity in specification Predefined operations on channels include: read::<* (c::channel(T))::T *>; write::<* (t::T, c::channel(T))::channel(T) *>; check::<* (c::channel(T))::boolean *>; Simple LIFO buffer where 3/23/01 Read returns the next element if it is present and is undefined otherwise Write adds a new element to the end of the channel Check is true if there is something on the channel to read Rosetta Tutorial - IP/SoC 2001 174 Buffered Channel package buffer is begin logic channel(t::subtype(univ))::subtype(univ) is sequence(t); read(c::channel(t::subtype(univ)))::t is if –(c=empty) then head(c) endif; remove(c::channel(t::subtype(univ)))::channel(t::subtype(univ)) is if c=empty then empty else tail(c) endif; write(e::t, c::channel(t::type(universal)))::channel(t::type(universal)) is c;;e; end buffer; 3/23/01 Rosetta Tutorial - IP/SoC 2001 175 Producer / Consumer Example facet producer(c::out channel(bit)) is l::bit; begin state_based l1: write(l,c); // Always write to the channel end producer; facet consumer(c::in channel(bit)) is s::bit; begin state_based l1: s’ = if check(c) then read(c) else s endif; end consumer; facet system is c::channel(bit); begin logic proc: producer(c); // Produce bit values cons: consumer(c); // Consume bit values end system; 3/23/01 Rosetta Tutorial - IP/SoC 2001 176 Summary Tutorial provides a basic introduction to the nuts and bolts of Rosetta specification Defines types and functions available Defines facets and packages as specification units Defines domains available to specifiers Defines specification composition Examples and Exercises provided interactively 3/23/01 Please contact authors for hard copies Rosetta Tutorial - IP/SoC 2001 177 Where to Get More Information The Rosetta web page contains working documents and examples: http://www.sldl.org Working documents include Usage Guide Semantic Guide Domain and Interaction definition Tool downloads include 3/23/01 Java-Based Rosetta Parser Rosetta Tutorial - IP/SoC 2001 178

Descargar
# An Introduction to Rosetta