PROCORSYS

PROCORSYS - KIT142

Keywords: hardware/software codesign, provably correct systems, embedded systems, safety critical systems, specification, verification, partitioning, term rewriting, transputers

Start Date: 1 October 94 / Duration: 36 months

[ participants / contact]

Objectivies and Approach

The aim is to design a partitioning algorithm based on a cost function, to determine hw/sw partitioning for embedded sytems. The approach is based on the provision of a set of transformation rules, which are provably correct in the semantics of the programming language. A further objective is to use a term-rewriting system to verify the transformation rules and to use the rules to carry out the partitioning task.

Progress and Results

The approach is based on an algorithm proposed by E. Barros (see KIT Action 128). This algorithm supports a detailed exploration of the design space, permitting the entire description to be analysed. Distinct implementation possibilities of the hardware components are considered. The first task is to formalise this algorithm. Occam has been used to express both the input and the output of the partitioning process. Occam obeys a large set of algebraic laws, allowing one to characterise a solution of the partitioning problem as a program transformation. These algebraic laws are used to transform an arbitrary source program into a program whose structure reflects the software and hardware components of the embedded system, and their interactions. At present a strategy for partitioning and a set of transformation rules have been adopted which reduce an arbitrary Occam program to a normal form suitable for partitioning. This normal form allows a flexible analysis of possible final partitions.

Information Dissemination Activities and/or Exploitation

Technical presentations on an overall strategy for provably correct hardware/software partitioning were provided in the course of the PROCOS workshop and the working group meeting at Oxford in January 1995. Further progress on this has been reported at the PROCOS working group meeting held in March 1996. Short courses on hardware/software codesign have been provided by the Federal University of Pernambuco. More recently, in August 1996, presentations were made of a complete set of rules to transform an Occam program into the normal form referred to above at the ProCoS-US Hardware Synthesis and Verification workshop, held at Cornell University in the USA.

Coordinator

Oxford University Computing Laboratory
Wolfson Building, Parks Road
Oxford OX1 3QD, UK

EU Partners

Oxford University, UK
Technical University of Denmark, DK
Christian-Albrechts-Universität, Kiel, D
Carl Von Ossietzky Universität, Oldenburg, D

Non-EU Partners

Federal University of Pernambuco, BRZ

CONTACT POINT

Mr. Augusto Sampaio
Tel: +55 81 271 8430
Fax: +55 81 271 8438
E-mail: acas@di.ufpe.br