partition

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 ...

Informations

• Publié par: Thoin
• Nombre de lectures: 16
• Langue: English

Extrait

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
[phone]
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
[phone]
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 use