Deriving an Efficient FPGA Implementation of a Low Density Parity Check Forward Error Corrector

作者：Gill Andy^*; Farmer Andrew

来源：ACM Sigplan Notices, 2011, 46(9): 209-220.

DOI：10.1145/2034574.2034804

• Design
• Performance
• Reliability
• Verification
• Lava
• DSL
• Error Correction
• LDPC

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.

• 出版日期2011-9