"A Refinement-based Methodology for Implementation Design and Semi-automatic Verification on an FPGA"
University of Surrey
In this paper, we present a case study where an application is specified and implemented on an FPGA. Specification and development is conducted in Circus---a language combining the well-known formalisms Z and CSP--and the implementation is in Handel-C. Design decisions are based on testing, experimental evidence, and engineering intuition; are guided by the speed and area requirements of the application on the FPGA; and formally justified using a notion of refinement. High levels of assurance in the correctness of the implementation---including safety properties---are necessary. These assurances are formulated in terms of proof obligations concerning the behaviours present in the specification, and the correctness of the development process. Proof obligations are discharged automatically using a model-checker and a theorem prover. Scalability of these techniques are evidenced with the formal notion of data abstractions and properties of refinement. A pathological error in a previous implementation of the system is discovered by formal verification: this error was not identified in testing phases. The contribution of this paper can be summarised as a demonstration of how Circus and associated tools can be used in the design, development and verification of highly concurrent systems where high levels of assurance of behavioural and safety properties are necessary.
2006 MAPLD International Conference Home Page