Stefan Frehse, Gorschwin Fey, et al.
FMCAD 2012
Algebraic error correcting codes (ECC) are widely used to implement reliability features in modern servers and systems and pose a formidable verification challenge. We present a novel methodology and techniques for provably correct design of ECC logics. The methodology is comprised of a design specification method that directly exposes the ECC algorithm's underlying math to a verification layer, encapsulated in a tool 'BLUEVERI', which establishes the correctness of the design conclusively by using an apparatus of computational algebraic geometry (Buchberger's algorithm for Grobner basis construction). We present results from its application to example circuits to demonstrate the effectiveness of the approach. The methodology has been successfully applied to prove correctness of large error correcting circuits on IBM's POWER systems to protect memory storage and processor to memory communication, as well as a host of smaller error correcting circuits. © 2012 IEEE.
Stefan Frehse, Gorschwin Fey, et al.
FMCAD 2012
Jun Xie, Rogerio Schmidt Feris, et al.
ICIP 2014
Ritendra Datta, Jianying Hu, et al.
ICPR 2008
Eugene H. Ratzlaff
ICDAR 2001