Presentation
Formally Validating Industry Standard BCH‑ECC/CRC Codes – A Step by Step Recipe
DescriptionFormal verification of CRC and ECC hardware does not scale with conventional techniques due to large Datapath's, extensive lookup tables, and complex Galois-field arithmetic. Existing approaches rely on monolithic end-to-end properties, bounded proofs, or coarse linearity abstractions, and even then, they typically break down beyond ~512-bit widths.
This paper introduces a theorem-guided formal verification methodology that scales to production-class CRC and ECC designs. The key novelty is a systematic decomposition of functional correctness into reusable, mathematically grounded theorems capturing structural and algebraic invariants—such as linearity, syndrome correctness and consistency, and error-propagation properties of locator polynomials. These theorems are proved independently, and proof is composed of incrementally using assume–guarantee reasoning within an industry-standard formal tool (VC Formal).
We have validated the approach on two industrial designs: an IEEE 802.3 CRC with a 5120-bit pipelined Datapath, and a BCH DECTED ECC with m = 2047 and t = 2. Prior methods time out, whereas our methodology achieves complete functional verification.
To our knowledge, this is the first demonstration of scalable and complete formal verification of CRC/ECC designs at this scale using a production-ready formal tool, making the approach directly applicable to industrial verification flows.
This paper introduces a theorem-guided formal verification methodology that scales to production-class CRC and ECC designs. The key novelty is a systematic decomposition of functional correctness into reusable, mathematically grounded theorems capturing structural and algebraic invariants—such as linearity, syndrome correctness and consistency, and error-propagation properties of locator polynomials. These theorems are proved independently, and proof is composed of incrementally using assume–guarantee reasoning within an industry-standard formal tool (VC Formal).
We have validated the approach on two industrial designs: an IEEE 802.3 CRC with a 5120-bit pipelined Datapath, and a BCH DECTED ECC with m = 2047 and t = 2. Prior methods time out, whereas our methodology achieves complete functional verification.
To our knowledge, this is the first demonstration of scalable and complete formal verification of CRC/ECC designs at this scale using a production-ready formal tool, making the approach directly applicable to industrial verification flows.
Event Type
Engineering Poster
TimeTuesday, July 285:00pm - 6:00pm PDT
LocationDAC Pavilion, Exhibit Floor