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: [email protected]+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: [email protected]+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
[email protected] - Value of x in state s
x’ – Standard shorthand for [email protected](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) => ([email protected](t)=none);
L3: (pulse=A1) and (inPulse=A1) => ([email protected](t)=none) and
([email protected]+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
([email protected](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
([email protected](t)=none) and
([email protected]+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 [email protected] 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
([email protected]+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 | [email protected]))}
M__I(g::state_based,f::logic)::set(term) is
{sel(t::M__terms(g) | forall(s::g.S | [email protected]))}
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
([email protected]+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