A technical paper titled “Datapath Verification via Word-Level E-Graph Rewriting” was published by researchers at Intel Corporation and Imperial College London.
“Formal verification of datapath circuits is challenging as they are subject to intense optimization effort in the design phase. Industrial vendors and design companies deploy equivalence checking against a golden or existing reference design to satisfy correctness concerns. State-of-the-art datapath equivalence checking tools deploy a suite of techniques, including rewriting. We propose a rewriting framework deploying bitwidth dependent rewrites based on the e-graph data structure, providing a powerful assistant to existing tools. The e-graph can generate a path of rewrites between the reference and implementation designs that can be checked by a trusted industry tool. We will demonstrate how the intermediate proofs generated by the assistant enable convergence in a state of the art tool, without which the industrial tool runs for 24 hours without making progress. The intermediate proofs automatically introduced by the assistant also reduce the total proof runtime by up to 6x.”
Find the technical paper here. Published August 2023 (preprint).
Coward, Samuel, Emiliano Morini, Bryan Tan, Theo Drane, and George Constantinides. “Datapath Verification via Word-Level E-Graph Rewriting.” arXiv preprint arXiv:2308.00431 (2023).
Related Reading
Design And Verification Methodologies Breaking Down
As chips become more complex, existing tools and methodologies are stretched to the breaking point.
Formal Verification Knowledge Center
Leave a Reply