partition

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