Read anywhere, anytime
Description
Subjects
Informations
Published by | Thoin |
Reads | 16 |
Language | English |
Exrait
g
f
Formal Veriﬁcation of Speciﬁcation 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 Veriﬁcation of Speciﬁcation 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 ﬁrst in series of reports
that demonstrate how we use this formal approach to reﬁne a given speciﬁcation down to its cycle accurate implementation.
We formally deﬁne models and develop theorems and proofs to show that our well deﬁned reﬁnement algorithms produce
functionally equivalent models. In this report, we speciﬁcally look at generation of an architecture level model by reﬁnement
of a speciﬁcation model. The reﬁnement process follows a well deﬁned system level partitioning algorithm. We prove that
executing the individual steps of the reﬁnement algorithm, in the predeﬁned order, leads to an equivalent model.
2Contents
1 Introduction 1
2 Model Algebra 2
2.1 Model Deﬁnition . ................................................ 3
2.1.1 Termsanddeﬁnitions............... 3
2.1.2 Axioms.................................................. 4
3 System Level Partitioning 5
3.1 Partitioning reﬁnement algorithm . . . . ..................................... 5
3.2 Theorems......................... 7
3.3 Formal Veriﬁcation of Speciﬁcation Partitioning ................................. 10
4 Conclusion and Future Work 11
iList of Figures
1 Thegradualreﬁnementproces.......................................... 1
2 Theuniversalsetofsystemmodels. ........... 2
3 Atwowayblockingchannel........................................... 2
4 Asimplemodel...................... 3
5 Asimplespeciﬁcationmodel............................................ 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 Veriﬁcation of Speciﬁcation 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 ﬁrst in series of
reports that demonstrate how we use this formal approach
to reﬁne a given speciﬁcation down to its cycle accurate im
Intermediate Model (level 1)
plementation. We formally deﬁne models and develop the
orems and proofs to show that our well deﬁned reﬁnement
algorithms produce functionally equivalent models. In this
report, we speciﬁcally look at generation of an architecture
Intermediate Model (level i-1)level model by reﬁnement of a speciﬁcation model. The re
ﬁnement process follows a well deﬁned system level parti-
tioning algorithm. We prove that executing the individual Refinement i
steps of the reﬁnement algorithm, in the predeﬁned 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 speciﬁcation. The common approach in system
design is to write models at different levels of abstraction.
However,with the size of these designs, traditional veriﬁ Figure 1. The gradual reﬁnement process.
cation and simulation based approaches for validation are
no longer practical. Besides, veriﬁcation 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 speciﬁcation 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 deﬁned sequence of reﬁne i
several implementations for the same speciﬁcation and theyments [2]. The output model is the product of gradual
would all belong to the same equivalence class. We mustreﬁnements to the input. Each gradual reﬁnement
ensure that when a model at abstraction level j is reﬁned 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 reﬁnement j 1
same equivalence class as m . In other words, theis broken into a sequence of gradual reﬁnement steps. We j
reﬁnement 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 ﬁnal output This report is a ﬁrst in series of reports on formal veri
model is equivalent to the input model. To achieve this, we ﬁcation of system level model reﬁnements. Here, we focus
develop formalisms to describes at different abstrac on the behavioral partitioning of a speciﬁcation model to
tion levels and perform reﬁnements 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 deﬁnition 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 reﬁnement algorithm in Section 3. Next, we
channels we consider for the purpose of this report are twoprove some useful theorems. The ﬁnal theorem uses the ax
way blocking channels as shown in ﬁgure 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 speciﬁcation model are
DAT A. The transfer semantics ensure that the receiving be equivalent. The model in this report has been simpliﬁed 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 deﬁned as:
2 Model Algebra A B C O R
B is the set of behaviors,
For proving correctness of model reﬁnements, we need
C is the set of channels,to deﬁne 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 predeﬁned 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.
ﬁned on elements in B.ThesetB is closed with respect toThe ﬁrst 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 predeﬁned1 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 deﬁne 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 deﬁne
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 Deﬁnition
v
b b ,where b b B B1 2 1 2 Based on the above algebra, a system model m can be
deﬁned 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 deﬁne 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 deﬁnitions
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 reﬁnements, 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 deﬁned on B 2.1.2 Axioms
as follows
Now that we have established the basic building blocks of
the system model, we need to deﬁne 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 reﬁne 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 ﬂattening.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
deﬁned 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 speciﬁcation 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 ﬁcation, once we have the partitioning decisions. This pro-
cess is known as partitioning reﬁnement [3]. In this section,
3. par b e
)= b
we present the partitioning reﬁnement 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 reﬁnement 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 ﬁrst step in deriving the architecture model p
iors PE through PE such thatfrom a given speciﬁcation [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 reﬁned 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 ﬁgure 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 reﬁnement process is demonstrated 1 3
b b to derive intermediate model m as shown in ﬁgureon a simple speciﬁcation model. The speciﬁcation, com 3 4 i
7.prising of four leaf behaviors viz. b b b and b is shown1 2 3 4
in ﬁgure 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 ﬁnal 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
Access to the YouScribe library is required to read this work in full.
Discover the services we offer to suit all your requirements!