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 inc reasingly widespread. Specialized Hardware Description Languages (HDL) are used to describe and develop the required circuits. In this paper, we advoc ate using an even more general purpose programming language, based on Occam , for the automatic compilation of high-level programs to low-level circuit s. The parallel constructs of Occam can map directly to hardware as conveni ently as to software, with potentially dramatic speed-up of highly parallel algorithms. We demonstrate that the compilation process can be verified us ing algebraic refinement laws, increasing the confidence in its correctness . Verification is particularly important in high-integrity systems where sa fety or security is paramount. A prototype compiler has also been produced very directly from the theorems using the logic programming language Prolog .