Provably correct hardware compilation

Jonathan Bowen

(University of Reading)

The availability of Field Programmable Gate Arrays (FPGA) now allows the fast generation of hardware by a purely software process. This enables the automatic compilation of a high level description of hardware into a "netlist" of individual digital hardware components. The compilation scheme may be verified, allowing an arbitrary number of circuits to be compiled with the same level of assurance, instead of needing to be checked individually. The compilation theorems may be rapid-prototyped very directly in a logic programming language such as Prolog. The high level language used for the circuit description is based on Occam, which includes parallel constructs, allowing algorithms for (naturally parallel) hardware to be coded conveniently and efficiently.
Tuesday 31st October 1995, 14:30
Seminar Room 322
Department of Computer Science