A. Gill and A. Farmer, “Deriving an efficient FPGA implementation of a low density parity check forward error corrector,” in Proceedings of the 16th ACM SIGPLAN international conference on Functional programming, ICFP ’11, pp. 209–220, ACM, Sep 2011.



Creating correct hardware is hard. Though there is much talk of using formal and semi-formal methods to develop designs and implementations, in practice most implementations are written without the support of any formal or semi-formal methodology. Having such a methodology brings many benefits, including improved likelihood of a correct implementation, lowering the cost of design exploration and lowering the cost of certification. In this paper, we introduce a semi formal methodology for connecting executable specifications written in the functional language Haskell to efficient VHDL implementations. The connection is performed by manual edits, using semi-formal equational reasoning facilitated by the worker/wrapper transformation, and directed using commutable functors. We explain our methodology on a full-scale example, an efficient Low-Density Parity Check forward error correcting code, which has been implemented on a Virtex-5 FPGA.


  author = {Gill, Andy and Farmer, Andrew},
  title = {Deriving an Efficient {FPGA} Implementation of a Low Density Parity Check Forward Error Corrector},
  booktitle = {Proceedings of the 16th ACM SIGPLAN international conference on Functional programming},
  series = {ICFP '11},
  year = {2011},
  isbn = {978-1-4503-0865-6},
  location = {Tokyo, Japan},
  pages = {209--220},
  numpages = {12},
  doi = {10.1145/2034773.2034804},
  acmid = {2034804},
  publisher = {ACM},
  keywords = {dsl, error correction, lava, ldpc},
  month = {Sep},
  location = {Tokyo, Japan},