Coordinators

Prof. C.A.R. Hoare
Oxford University Computing Laboratory
Wolfson Building, Parks Road
Oxford OX1 3QD, England
Tel: +44-1865-273838
Fax: +44-1865-273839
Email: Tony.Hoare@comlab.ox.ac.uk

Country
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 (Brazil)

Contact Point
Augusto Sampaio
Universidade Federal de Pernambuco
Departamento de Informatica
Caixa Postal 7851
CEP 50740-540 Cidade Universitaria
Recife-PE Brasil
Tel: +55-81-271-8430
Fax: +55-81-271-8438
Email: acas@di.ufpe.br

Keywords: hardware/software co-design, provably correct systems, embedded systems, safety-critical systems, specification, verification, partitioning algorithms, rewriting, Occam, Transputer

Start date: 1 October, 1994

Duration: 36 months

Objectives and Approach

The overall approach is to design the algorithm as a set of transformation rules which should be provably correct from the semantics of the programming language. The result of the partitioning is still be a program, but its structure reflects the software and hardware components, and how they interact to achieve the overall goal. It is possible to express this result as a program because the programming language used includes features to express parallelism and communication. Another objective of the co-operation is to use a term rewriting system both to verify the transformation rules and to use the rules to carry out the partitioning task.

Progress and Results

In spite of its flexibility, Barros' partitioning algorithm was originally developed in an informal way. While its input is a program (or specification) in a formal language (UNITY) its output is a set of tables which indicate the processes to be implemented in software and those to be implemented in hardware. Because the output is not expressed in a language with a well-defined semantics, it is not possible to verify that the algorithm is correct in the sense that the partitioned program preserves the semantics of the given input.

Our first task was to study how this output could be expressed in a formal language. We decided to use Occam both as the input and the output language. There are many reasons for choosing Occam. It was developed from CSP, and like CSP Occam obeys a large set of algebraic laws which can be used to carry out program transformation with the preservation of semantics.

In particular, using Occam it is possible to regard hardware/software partitioning as an application of program transformation. The algebraic laws can be used to transform an arbitrary source program (the input) into a program whose structure reflects the software and hardware components, and how they interact to achieve the overall goal. It is possible to express this in Occam because it includes features to express parallelism and communication.

At present we have a concrete proposal of the overall strategy to partitioning, including the necessary modifications to deal with Occam, and we have discovered a set of transformation rules to reduce an arbitrary Occam program to a normal form which is suitable for carrying out the partitioning. This form is basically the parallel combination of very simple processes; as parallelism in Occam is a commutative operator, this normal form allows a very flexible analysis of what should be the final clusters produced by the partitioning.

Information Dissemination Activities and Exploitation

Further progress on Sampaio's work has been reported at the ProCoS-WG Working Group meeting held in Oldenburg in March, 1996. The emphasis of his talk in this meeting was the partitioning (through algebraic transformations) of an matrix inverse algorithm.

Prof. Hans Rischel from the Technical University of Denmark (DTU) visited the Federal University of Pernambuco (UFPE) during the week from 29 September to 5 October, 1995. Apart from presenting a talk on a Codesign project carried out at DTU, He was an invited speaker of the IX Brazilian Symposium on Software Engineering held at UFPE.

Dr. Ian Page from the University of Oxford gave a short course at the First Brazilian Workshop on Hardware/Software Codesign; this was also held at UFPE. In particular, this workshop was organised in the context of a local project on codesign in which Augusto Sampaio is engaged.

As a result of the above two visits, this co-operation has been tightened in several ways. In particular, the interface has been discussed between the work on partitioning and the work on hardware implementation being carried out at Oxford and at the Technical University of Denmark. While both sites have developed advanced strategies for producing the final implementation, at present these sites perform the partitioning manually (based on intuition). Ways of integrating the partitioning approach under development at the non-EU site with these works on hardware implementation have been discussed; this will be carried out as soon as a prototype of the partitioning algorithm is available.

The more recent dissemination information activity was the participation of Augusto Sampaio in the ProCoS-US Hardware Synthesis and Verification workshop, held at Cornell University, Ithaca, USA, August 1996. At this meeting, Augusto Sampaio presented a paper (formally refereed and accepted by the programme committee) on "A Transformational Approach to Hardware Software Partitioning". In this talk, he presented a complete set of rules to transform an arbitrary (but finite) Occam program into the normal form briefly explained in the previous section.