Provably Correct Hardware Compilation


Keywords: provable correctness, hardware compilation, hardware/software codesign, real time, safety critical systems, embedded systems, customer silicon, FPGA

Start Date: 1 September 93 / Duration: 48 months

[ participants / contact]

Objectivies and Approach

The primary objective of this cooperative activity is to improve reliability of embedded systems that include special-purpose or customer silicon, together with a program-controlled element. This is to be achieved by a formal approach that intefrates reliable design methodology with automatic compilation by means of a provably correct tool.

A secondary objective is the reduction of design lead time, for electronic products, permitting rapid product development and test of semicustom ASICs and custom VLSI, especially using Field Programmable Gate Arrays (FPGA) as a prototyping or a delivery mechanism.

The scientific basis is the construction of uniform mathematical modelsof requirements, designs and implementations both in hardware and software. Similar models have been developed and implemented by the PROCOS project in Europe and by terms in the Electrical Engineering Department at Cornell. The approach of this working group is to combine the range and merit of the theories developed on the two continents, and to publish joint results.

European links: ESPRIT BRA projects PROCOS (3104) and PROCOS II (7071); WG ACiD (7225), COMPULOGNET (7230), HORN (7249), EXACT (643).

Information Dissemination Activities and/or Exploitation

The collaboration consists of exchange visits and workshops to aid the dissemination of the results of the project. A joint workshop took place at Cornell in August 1996.


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

EU Partners

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

Non-EU Partners

Cornell University, USA


Prof. C.A.R. Hoare FRS
Tel.: +44 1865 273 841
Fax:: +44 1865 273 839

INCO synopses home page INCO cooperation index INCO keyword index
INCO acronym index INCO number index INCO Working Groups index
synopses home page all keywords index all acronyms index all numbers index

PROCOS-US - EC-US027, May 1997

please address enquiries to the ESPRIT Information Desk

html version of synopsis by Nick Cook