Back to list of 2005/06 seminars
At Surrey, we have developed an occam-to-FPGA compiler that has a number of different design philosophies from products such as Handel-C. In addition, access to all of the compiler source code allows us to experiment with additional facilities. Recently, we have implemented a compiler back-end that represents compiler-generated logic circuits as Communicating Sequential Processes (CSP) models.
We are now using FDR with these models to provide reference testing of the compiler as it undergoes further implementation and refinement, as well as to verify components of parallel application programs. In addition, by monitoring specific channels within application programs, CSP verifications of their correctness will now be possible on a routine basis.
The seminar will show example programs and results that illustrate the utility of our approach, and will indicate how we intend to overcome some of the limitations of modelling circuits at such a low level.