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.

Links

• http://doi.acm.org/10.1145/2034773.2034804

Abstract

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.

BibTeX

@inproceedings{Gill:11:DerivingLDPC,
  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},
}