Automatically Generated CSP Provides Verification for occam-derived Logic Circuits

Abstract — This paper reports on the creation of a new back-end for the authors ’ occam-to-FPGA compiler. The creation of Communicating Sequential Processes (CSP) models of compiler-generated logic circuits has thus re-cently been automated. These models are now being used to provide reference testing of the compiler as it undergoes further implementation and refinement, as well as to verify components of parallel application programs. This paper provides example programs and results to illustrate the utility of our approach. In addition, by monitoring specific channels within application programs, CSP verifications of their correctness will now be possible on a routine basis. I