An approach to the specification and verification of a hardware compilation scheme

The use of Field Programmable Gate Arrays (FPGA) to produce custom hardware circuits rapidly using a completely software-based process is becoming increasingly widespread. Specialized Hardware Description Languages (HDL) are used to describe and develop the required circuits. In this paper, we advocate using an even more general purpose programming language, based on Occam, for the automatic compilation of high-level programs to low-level circuits. The parallel constructs of Occam can map directly to hardware as conveniently as to software, with potentially dramatic speed-up of highly parallel algorithms. We demonstrate that the compilation process can be verified using algebraic refinement laws, increasing the confidence in its correctness. Verification is particularly important in high-integrity systems where safety or security is paramount. A prototype compiler has also been produced very directly from the theorems using the logic programming language Prolog.