partition
15 Pages
English
Downloading requires you to have access to the YouScribe library
Learn all about the services we offer

partition

Downloading requires you to have access to the YouScribe library
Learn all about the services we offer
15 Pages
English

Description

gfFormal Verification of Specification PartitioningSamar Abdi and Daniel GajskiTechnical Report CECS-03 06April 23, 2003Center for Embedded Computer SystemsUniversity of California, IrvineIrvine, CA 92697 3425, USA(949) 824 8059sabdi,gajski @cecs.uci.edu1gfFormal Verification of Specification PartitioningSamar Abdi and Daniel GajskiTechnical Report CECS-03 06April 23, 2003Center for Embedded Computer SystemsUniversity of California, IrvineIrvine, CA 92697 3425, USA(949) 824 8059sabdi,gajski @cecs.uci.eduAbstractThis report presents a formal approach to verify models in a system level design environment. It is a first in series of reportsthat demonstrate how we use this formal approach to refine a given specification down to its cycle accurate implementation.We formally define models and develop theorems and proofs to show that our well defined refinement algorithms producefunctionally equivalent models. In this report, we specifically look at generation of an architecture level model by refinementof a specification model. The refinement process follows a well defined system level partitioning algorithm. We prove thatexecuting the individual steps of the refinement algorithm, in the predefined order, leads to an equivalent model.2Contents1 Introduction 12 Model Algebra 22.1 Model Definition . ................................................ 32.1.1 Termsanddefinitions............... 32.1.2 Axioms.................................................. 43 System ...

Subjects

Informations

Published by
Reads 16
Language English

Exrait

g
f
Formal Verification of Specification Partitioning
Samar Abdi and Daniel Gajski
Technical Report CECS-03 06
April 23, 2003
Center for Embedded Computer Systems
University of California, Irvine
Irvine, CA 92697 3425, USA
(949) 824 8059
sabdi,gajski @cecs.uci.edu
1f
g
Formal Verification of Specification Partitioning
Samar Abdi and Daniel Gajski
Technical Report CECS-03 06
April 23, 2003
Center for Embedded Computer Systems
University of California, Irvine
Irvine, CA 92697 3425, USA
(949) 824 8059
sabdi,gajski @cecs.uci.edu
Abstract
This report presents a formal approach to verify models in a system level design environment. It is a first in series of reports
that demonstrate how we use this formal approach to refine a given specification down to its cycle accurate implementation.
We formally define models and develop theorems and proofs to show that our well defined refinement algorithms produce
functionally equivalent models. In this report, we specifically look at generation of an architecture level model by refinement
of a specification model. The refinement process follows a well defined system level partitioning algorithm. We prove that
executing the individual steps of the refinement algorithm, in the predefined order, leads to an equivalent model.
2Contents
1 Introduction 1
2 Model Algebra 2
2.1 Model Definition . ................................................ 3
2.1.1 Termsanddefinitions............... 3
2.1.2 Axioms.................................................. 4
3 System Level Partitioning 5
3.1 Partitioning refinement algorithm . . . . ..................................... 5
3.2 Theorems......................... 7
3.3 Formal Verification of Specification Partitioning ................................. 10
4 Conclusion and Future Work 11
iList of Figures
1 Thegradualrefinementproces.......................................... 1
2 Theuniversalsetofsystemmodels. ........... 2
3 Atwowayblockingchannel........................................... 2
4 Asimplemodel...................... 3
5 Asimplespecificationmodel............................................ 5
6 Intermediate model after step 1 of partitioning algorithm. . . . . . ....... 6
7 Intermediate model after step 2 of partitioning algorithm. . . . . . . ...................... 6
8 Final model after partitioning. . . . . . ..................... 7
ii+
+
Formal Verification of Specification Partitioning
Samar Abdi and Daniel Gajski
Center for Embedded Computer Systems
University of California, Irvine
Abstract
Specification Model (level 0)
This report presents a formal approach to verify models
Refinement 1in a system level design environment. It is a first in series of
reports that demonstrate how we use this formal approach
to refine a given specification down to its cycle accurate im
Intermediate Model (level 1)
plementation. We formally define models and develop the
orems and proofs to show that our well defined refinement
algorithms produce functionally equivalent models. In this
report, we specifically look at generation of an architecture
Intermediate Model (level i-1)level model by refinement of a specification model. The re
finement process follows a well defined system level parti-
tioning algorithm. We prove that executing the individual Refinement i
steps of the refinement algorithm, in the predefined order,
leads to an equivalent model.
Intermediate Model (level i)
1 Introduction
The continuous increase in behavioral and structural
complexity of SoC designs has raised the abstraction level Architecture Model (level N)
of system specification. The common approach in system
design is to write models at different levels of abstraction.
However,with the size of these designs, traditional verifi Figure 1. The gradual refinement process.
cation and simulation based approaches for validation are
no longer practical. Besides, verification by comparing
Figure 2 shows the universal set of system models. Thistwo separately written models is not tractable at the system
set is divided into classes of equivalent models. As shown,level.
a specification model m and its corresponding implementa-The only solution is to correctly generate one model s
tion m belong to the same equivalence class. There may befrom another using a well defined sequence of refine i
several implementations for the same specification and theyments [2]. The output model is the product of gradual
would all belong to the same equivalence class. We mustrefinements to the input. Each gradual refinement
ensure that when a model at abstraction level j is refined toproduces an output model that is functionally equivalent to
the one at level j 1, then model m must belong to thethe input model. Figure 1 shows how a model refinement j 1
same equivalence class as m . In other words, theis broken into a sequence of gradual refinement steps. We j
refinement must be contained in the equivalence class.must ensure that model at level i is equivalent to the one at
level i 1. By transitivity this ensures that the final output This report is a first in series of reports on formal veri
model is equivalent to the input model. To achieve this, we fication of system level model refinements. Here, we focus
develop formalisms to describes at different abstrac on the behavioral partitioning of a specification model to
tion levels and perform refinements on them. This report derive an architecture level model. The report is divided as
presents a limited set of formalisms useful in the context of follows. We begin by introducing the model algebra in the
system level design partitioning. next section. This includes a formal definition of a model in
1!g
;
=
:::
>
)
2
2
;
;
;
(
;
;
;
8
2
;
;
;
=
;
:::;
:::
f
:::;
g
;
f
;
;
)
(
:::;
)
;
:::
;
;
(
;
=
(
;
;
;
)
<
Channel cEquivalence Class
RecvSend
waitWrite DATA
b b1 2c=m ms p sender receiver
ready Read DATA
ack
wait
Figure 2. The universal set of system models.
Figure 3. A two way blocking channel
terms of the model algebra in Section 2. We also present the
basic axioms associated with this algebra. We then present
ferred and events to ensure the transfer semantics. Thethe partitioning refinement algorithm in Section 3. Next, we
channels we consider for the purpose of this report are twoprove some useful theorems. The final theorem uses the ax
way blocking channels as shown in figure 3. As we canioms of Model Algebra and these theorems to prove that the
see, the behaviors b and b use the channel c to exchange1 2partitioned architecture model and specification model are
DAT A. The transfer semantics ensure that the receiving be equivalent. The model in this report has been simplified to
havior will wait until the sender has written the data, anddemonstrate the concept. The methods used are completely
the sender behavior waits until the data item has been readscalable and can be used for large models as well. Finally,
by the receiver.we wind up with a summary and conclusion.
The Model Algebra is defined as:
2 Model Algebra A B C O R
B is the set of behaviors,
For proving correctness of model refinements, we need
C is the set of channels,to define a model algebra that can be used to formally repre
O = seq par (Set of Operations)sent system models. Generally speaking, a system is a set of v
R = (Set of Relations)tasks that are executed in a predefined partial order. These
tasks also talk to each other by exchanging data. In order
Operationsto develop an algebra for system models, we must intro
duce primitives to represent tasks and the data transactions
The operations mentioned in the above algebra are de amongst them.
fined on elements in B.ThesetB is closed with respect toThe first primitive is the unit of computation in a model,
both seq and par.referred to as a behavior. Behaviors that can either be leaf or
composite.Aleaf behavior is a sequence of operations be
b b b B1 2 3ing executed in a serial order. A composite behavior on the
other hand is formed by combination of leafors using
1. seq b b b B1 2 3operations of the model algebra. A model is constructed out
of these leaf behaviors by using the basic concept of hierar- 2. par b b b B1 2 3
chy and composition operations. Two or more leaf behav-
iors are put together to compose a composite behavior. The The seq operator implies that behaviors execute sequen
composite behaviors may also be combined with other leaf tially in time. Hence if b seq b b b ,thenb starts1 2 n 2
or composite behaviors to generate larger composite behav after b has completed, b starts after b has completed and1 3 2
iors. In the scope of this report, the composition may be so on. Behavior b is said to start when b starts and it com 1
sequential or parallel. Moreover, we need synchronization pletes when b completes. Note that the composite behaviorn
between behaviors to ensure the correct temporal order of b can be used to create more composite behaviors.
execution. The par operator creates a parallel composition of behav-
The other primitive is the unit of computation referred iors. If b par b b b , then there is no predefined1 2 n
to as a channel. It is used for communication between be order of execution between the behaviors b b b .Be-1 2 n
haviors. A channel encapsulates the data item to be trans- havior b is said to start when any behavior in b through b1 n
2(
f
;
;
g
!
(
;
;
!

;
f
!
;
g
;

2
())
f
2
:::;
g
;
;
8
;
:
))
=
;
g

)
2
)
)
f
=

;
)
(
g
(
;
)

;
!
(
(
)
:
;
;
!
(
(
(
;
)
)
(
2


=
!
f
(
;
starts. Behavior b is said to complete when all behaviors m
from b through b complete.1 n
Composite behaviors are essentially functions formed
using operators seq and par on behaviors. We will use the b23
notation f b b b to represent a composite behavior1 2 n
formed using behaviors b through b .1 n v 1
b c1 b2
Relations
We define the synchronization relation on B in the fol- vsync 2lowing way. b b B if b b then irrespective of1 2 1 2
the hierarchical composition, behavior b cannot start exe-2
cuting until behavior b completes.1
Data transfers in a system can take place either through b3
variables or channels. Sequentially composed behaviors
communicate through variables, while those composed in
parallel use channels. In the latter case, data from the sender
behavior is written to the channel. Subsequently, the re
ceiver behavior reads the data from the channel. We define
Figure 4. A simple modelthree kinds of data transfer relations as follows.
1. Data variable v sent from behavior b to behavior b1 1 2.1 Model Definition
v
b b ,where b b B B1 2 1 2 Based on the above algebra, a system model m can be
defined as a tuple
2. Data variable v sent from behavior b to channel c1 1
m B m R m wherev
b c ,where b c B C1 1 1 1
B(m) : the hierarchical composition of behaviors
3. Data variable v received by behavior b from channel1
representing the model m, and
c1
v R(m) : set of relations on thec b ,where c b C B1 1 1 1
behaviors used to compose B(m)
Class of Identity Behaviors
Figure 4 shows a simple model comprising of three leaf
behaviors b b and b.Behaviors b and b are sequen 1 2 3 2 3
We define the class of Identity Behaviors I to be a subset tially composed to create a composite behavior b 3, which2
of B such that all behaviors belonging to I output the input in turn is composed in parallel with behavior b . Channel1
data. The following behaviors belong to the class I : c is used to send data v from b to b .Variablev is sent1 1 2 2
directly from behavior b to b since they are in sequential2 3
Behavior(in var v , out var v )1 2 composition. Also note the synchronization edge from b1
v = v2 1 to b which guarantees that b cannot start executing before3 3
b completes, despite their parallel composition. The model1Behavior(in var v, out channel c)
m can be written as follows:
c.write(v)
B m par b seq b b1 2 3Behavior(in channel c, out var v)
v v v1 1 2
v = c.read() R m b b b c c b b b1 3 1 2 2 3
Behavior(in channel c , out channel c )1 2 2.1.1 Terms and definitions
c write c read2 1
For the purpose of explaining and formally proving correct-
Note that an identity behavior does not perform any other ness of model refinements, we need to introduce some no
operation except reading and writing a data item. tations.
3;

;

/
<
/
<
;
;
;
2
2
;
(
)
<
(
;
/
(

)
<
;
<
(
<
:::
)
(
<
;
^
8
<
)
<
8
)
;
;
;
/
;
^
;
<
;
8
;
<
(
)
f
;
(
/
;
^
;
2
;
<
;
;
;
<
(
)
[
)
(
/
2
(
(
2
)
;
(
;
;
;
=
<
/
)
:::;
)
(
(
;
/
;
)
;
;
(
::;
=
(
;
)
;
(
(
/
))
;
(
;
;
;
/
8
;
(
:::
(
)
;
;
)
)
;
;
;
;
:::
;
)
(
;
(
(
)
(
/
(
;
;
)
)
)
;
(
;
(
:::
;
)
)
;
/
(
;
)
(
[
)
;
:::;
=
f
(
j
+
/
;
;
+
;
=
;
;
)
:::
/
(
g
)
=
=
:::;
;
+
(
+
;
:::;
)
+
:::
+
;
:::;
(
;
;
(
+
f
;
)
(
(
+
g
:::
)
;
2
)
;
/
;
(
=
(
)
)
;
;
;
;
)
/
g
))
)
(
+
)
+
;
;
;
;
/
=
2
:::
(
+
(
+
)
=
)
:::;
;
+
[
+
)
:::;
;
+
)
+
(
:::;
(
;
)
=
(
)
2
2
;
;
;
Sub behavior The relation sub behavior is defined on B 2.1.2 Axioms
as follows
Now that we have established the basic building blocks of
the system model, we need to define a set of axioms that are
b b B if b b then1 2 1 2
associated with the model algebra. These axioms will be
used to construct theorems that will validate model refine b is a sub expression in the hierarchical expression of1
ments and transformations.b .2
Example from Figure 4: Axiom 1 (Synchronization) A sequential composition of
b seq b b , B m
)= par b seq b b ,23 2 3 1 2 3 behaviors b b in a model M may be replaced by a parallel1 2
therefore b B m .23 composition of b b by adding a synchronization relation1 2
b b in R(m).1 2
Leafs This is the set of all leaf level sub behaviors of a
f seq b b b3 b4 R m
)=behavior. 1 2
f par b b b3 b4 R m b b1 2 1 2
Lea f s b
)= x x b
69 y b s.t. y x
Axiom 2 (Flattening) If a behavior x, in model M, is com
posite and parent of x is the same composite type as x, andExample from Figure 4:
x does not have any synchronization constraints, then x may
be removed through flattening.1. Lea f s b 3
)= b b2 2 3
Sub Axiom 2.1 Fo r t h e seq behavior:2. Lea f s B m b b b1 2 3
if x seq b b bi 1 i 2 j
Predecessor Abehaviorb is said to be a predecessor of1
m b seq b b b x b b b B m and1 2 i j 1 j 2 kbehavior b in model m (denoted by b b ), if in the2 1 2
temporal order of execution b must complete before
69 a B m such that1
b begins. Formally, the predecessor relation can be2 a x R m or x a R m then
defined as:
b seq b b b b b b b b b1 2 i i 1 i 2 j j 1 j 2 kb b b B m1 2 3
Sub Axiom 2.2 The dual for par behavior is as follows:
m
1. seq b b
;:
: B m b b1 2 1 2
if x par b b bi 1 i 2 j
m
2. b b R m b b1 2 1 2 b par b b b x b b b B m and1 2 i j 1 j 2 k
m m
69 a B m such that3. b b b b b b1 2 3 2 1 3
m m a x R m or x a R m then4. b b b b b b1 2 3 1 3 2
m m m b par b b b b b b b b b1 2 i i 1 i 2 j j 1 j 2 k
5. b b b b b b1 2 2 3 1 3
Axiom 3 (Forward Substitution) Synchronization re
Example from Figure 4: lation for composite behaviors may be replaced by
synchronization relation(s) on their child behaviors.
m
1. b b1 3 Sub Axiom 3.1 If a behavior b is a sequential composition
m such that b seq b b b and if there exists a syn 1 2 n2. b b2 3
chronization constraint from a behavior a b, then the
constraint may be replaced by a synchronization constraintImmediate Predecessor Abehaviorb is said to be an im 1
a b . Similarly, a constraint b n may be replaced by1mediate predecessor of behavior b , in a model m (de 2
m b nnnoted by b b )if1 2
if b seq b b b B m thenm m 1 2 n
69 b B m b B such that b b b3 3 1 3 2
a B m if a b R m
Example from Figure 4: R m
)=
( R m a x a b1
m
1. b b1 3 a B m if b a R m
m
R m
)=( R m b a b a2. b b n2 3
4:::;
\
;
=
;
f
)
;
(

8
;
:

2
=
[
(
(
)
;
;
2
(
(
)
;
;
(
;
(
:::;
;
;
;
=
2
(
)
;
(
;
(
:::;
(
)
;
=
)

;
2
:::
f
;
;
)
:::;
)
g
;
!
8
;
;
!
;
f
;
=
)
g
)
;
;
f
8
=
/
S
;
(
;
=
;
=
/
;
)
(
;
g
)
:::;
(
(
(
!
;
)
)
;
(
!
;
))
;
f
;
=
[
g
;
;
(
;
;
;
(
!
;
f
)
2
/
2
;
;
;

;
^
;

;
g
)
!
:::;
;
;
!
(
f
;
=
(
!
;
)
)
(
/
/
;
;
(
;
)
;
:::;
(
;
;
=
(
:::
;
;
(
;
)
Sub Axiom 3.2 If a behavior x is a parallel composition m
such that b par b b b and if there exists a syn 1 2 n
chronization constraint from a behavior a b, then the
constraint may be replaced by synchronization constraints
a b a b2 a b . Similarly, a constraint b a1 n b1
may be replaced by constraints b a b a b a1 2 n v 1
if b par b b b B m then1 2 n
a B m if a b R m
v 2R m
)=
( R m a b a b a b a b1 2 n b c b2 3
a B m if b a R m
R m
)=( R m b a b a b a b a1 2 n
Axiom 4 (Commutativity) A parallel composition of the
vtype par b b is equivalent to par b b .1 2 2 1 3
b4par b b
)= par b b1 2 2 1
.
Figure 5. A simple specification model.Axiom 5 (Identity) Given a model m and behavior e I
such that e does not have any relations in R m , the follow
ing hold true b B m
correctness and suitability of our partition. For this pur-
pose, we need to generate an executable partitioned model.1. seq b e
)= b
The model may be generated automatically from the speci-
2. seq e b
)= b fication, once we have the partitioning decisions. This pro-
cess is known as partitioning refinement [3]. In this section,
3. par b e
)= b
we present the partitioning refinement algorithm using our
model algebra. Subsequently, we develop a theorem andAxiom 6 (Transitivity) Given a model m and b b b31 2
prove it to show that this algorithm indeed works correctly.B m
m mv v v 3.1 Partitioning refinement algorithmb b b b b b iff b b b b1 2 1 3 3 2 1 3 3 2
Given a model m B m R m,asetofnAxiom 7 (Channel creation) Given identity behaviors
components PE PE PE and n partitionse e I and channel c C 1 2 n1 2
partition partition partition . Each partition is1 2 n
Sub Axiom 7.1 a set of leaf behaviors in m. The partitions follow the
v v v following rules:
e e e e e c c e1 2 1 2 1 2
n1. partition Lea f s B m andii 1
Sub Axiom 7.2
2. partition partition 1 i j ni j0 0
e e e c c e1 2 1 2
3. partition is assigned to PEi i
3 System Level Partitioning The partitioned model m is generated as follows.p
1. Initialize B(m ) as a parallel composition of n behav This is the first step in deriving the architecture model p
iors PE through PE such thatfrom a given specification [1]. Once we have determined the 1 n
PE f b b i2 b ,wherecomponents in the proposed system architecture, we need i i1 i im
to divide the system tasks into suitable groups. Each of
b : b partitionj j ithese groups is assigned to a unique component in the ar- bij : otherwisechitecture. After this assignment, we need to evaluate the
5(
g
g
)
;
g
(
!
g
(
;
;
;
)
;
(
g
;
)
)
=
!
2
;
^
)
(
;
))
;
)
!
!
2
(
9
;
!
(
;
!
2
f
(
j
(
;
!
;
;
!
!
!
;
=
!
(
f
;
g
;
!
=
;
;
;
!
f
)
;
)
;
!
;
)
;
(
g
/
;
S
;
;
;
(
;
)
!
;
;
!
!
;
;
;
!
!
;
!
!
;
f

=
^
)
2
(
f
;
)
))
(
(
;
;
)
)
)
;
(
;
(
(
g
(
)
=
;
)
g
(
;
;
)
;
;

(

=
=
(
;
8
;
=
2
m iPE PE1 2
b b1 1
PE PE1 2
b b23 23
b1b b b b2 3 2 3
syncv 1
v 2
cb b2 3b b44
sync
Figure 6. Intermediate model after step 1 of partition- b v4 3ing algorithm.
2. Add following synchronization relations
mn Figure 7. Intermediate model after step 2 of partition-x y y partition x yii 1
ing algorithm.x Lea f s B m partitioni
3. Introduce identity behaviors for each synchronization
relation as follows The partitioning decision is as follows.
b b B m such that b b R m e e I1 2 1 2 1 2 partition b b b to PE1 1 2 4 1
replace behavior b with seq b e and b with1 1 1 2 partition b to PE2 3 2
seq e b and modify R(m) as follows2 2
After partitioning, the model is refined to a parallel com-v v
(a) if b b R m ,thenR m
)=( R m
f b1 2 1 position of PE and PE . After step 1 the intermediate1 2v v v v
b b b
[f b e e c c e e2 1 2 1 1 1 1 1 2 2 model is shown in figure 6. The relevant leaf behaviors
b2 are copied into each of the PEs in the original hierarchy.
0 After step 2 of the partitioning algorithm, we derive an in-
(b) else R m R m
f b b
[f e1 2 1
termediate model m . Synchronization constraints are addedi0
c c e1 1 2 across the partitions to maintain the original partial order of
m m
execution. b b and b b , are the only immediate1 3 3 44. Flatten redundant hierarchy.
predecessor relations across partitions. Therefore, we add
corresponding synchronization constraints i.e. b b andAn example of the refinement process is demonstrated 1 3
b b to derive intermediate model m as shown in figureon a simple specification model. The specification, com 3 4 i
7.prising of four leaf behaviors viz. b b b and b is shown1 2 3 4
in figure 5. Leaf behaviors b and b are composed in paral-2 3
B m par seq b b b seq bi 1 2 4 3lel to form a composite behavior. This cite behavior
v v v v31 2 2follows b and precedes b in a larger sequential composi- R m b b b c c b b b1 4 i 1 2 2 3 3 4
tion. Also note the data transactions between the behaviors. b b b b1 3 3 4
Data item v is sent from behaviors b to b . Similarly v1 1 2 3
is sent from b to b .Sinceb and b are composed in par- The final model m is shown in Figure 8. This model is3 4 2 3 p
allel, they talk using the channel c, which sends data item derived by executing step 3 and 4 of our algorithm on model
v from b to b . The model m may be expressed in our m . Identity behaviors e e e and e and channels c and2 2 3 i 1 2 3 4 1
algebra as follows: c are inserted corresponding to synchronization relations2
v3
b b and b b . The pair of relations b b b1 3 3 4 3 4 3
v v v vB m seq b par b b b 3 3 3 31 2 3 4 b in m is replaced by b e e c c e e4 i 3 3 3 2 2 4 4
v v v v1 2 2 3
R m b b b c c b b b b in m . Similarly, channel c is introduced to implement1 2 2 3 3 4 4 p 1
6