Formal Verification of an Occam-to-FPGA Compiler and its Generated Logic Circuits
- When?
- Tuesday 21 July 2009, 11:00 to 12:00
- Where?
- 39 BB 02
- Open to:
- Staff, Students
As custom logic circuits (e.g. field-programmable gate arrays, or FPGAs) have become larger, the limitations of conventional design flows have become more apparent. For large designs, verification by simulation is now impractical.
One solution to this challenge is hardware/software co-design, in which the desired logic is specified using a high-level, or programming, approach. Here, the requirements are to incorporate the parallelism from the original specification, as well as to accommodate greater complexity through various abstraction techniques. Verification may be achieved by simulation at an algorithmic level, or by formal proofs. However, by a particular circuit runs into difficulties of state-space explosion in a state-based model-checking scheme.
The research that is reported in this thesis has addressed the formal verification of a compiler that generates FPGA circuits. Rather than proving the correctness of every circuit generated by a compiler, the approach has been to validate the behaviour of the compiler itself. The source language that has been used is a variant of OCCAM, which incorporates fine-grained parallelism and message-passing along channels between parallel processes. The syntax of an OCCAM program can be mapped onto an abstract syntax tree, and each component of this tree can then be mapped into hardware. It is then necessary to prove that the hardware for each component correctly implements its specification, which can be performed by specifying each in CSP and model-checking them to check for equivalence. The components must also be proved to compose correctly, so that they may be plugged together in any way that satisfies the syntax of the source language. Finally, the correct composition of components is enforced by the type-checking of the compiler itself, using Java classes and inheritance to ensure that the CSP for each of the components being checked is manufactured within the same Java methods that create the hardware circuits.
The thesis discusses the proof strategy and shows how correctness can be justified. It concludes with some examples of simple OCCAM programs that have been translated into hardware and executed on real FPGA devices, correctly at the first attempt.
