Advertisement
Published in:
01-10-2014
Verification of Galois field based circuits by formal reasoning based on computational algebraic geometry
Published in: Formal Methods in System Design | Issue 2/2014
Log inActivate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
Abstract
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 Gröbner 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.