Formal Verification of Hardware Synthesis

Thomas Braibant, Adam Chlipala. Formal Verification of Hardware Synthesis. Proceedings of the 25th International Conference on Computer Aided Verification (CAV'13). July 2013.

Paper as PDF

We report on the implementation of a certified compiler for a high-level hardware description language (HDL) called Fe-Si (FEath-erweight SynthesIs). Fe-Si is a simplified version of Bluespec, an HDL based on a notion of guarded atomic actions. Fe-Si is defined as a dependently typed deep embedding in Coq. The target language of the compiler corresponds to a synthesisable subset of Verilog or VHDL. A key aspect of our approach is that input programs to the compiler can be defined and proved correct inside Coq. Then, we use extraction and a Verilog back-end (written in OCaml) to get a certified version of a hardware design.

Public source-code repository