Datapath Verification via Word-Level E-Graph Rewriting

TL;DR

This paper introduces a novel e-graph based rewriting framework for datapath verification that enhances existing equivalence checking tools by generating intermediate proofs, significantly reducing proof runtime and aiding convergence.

Contribution

The proposed framework leverages bitwidth-dependent rewrites with e-graphs to improve the efficiency and effectiveness of datapath equivalence checking in industrial verification workflows.

Findings

Intermediate proofs enable faster convergence of verification tools.

Proof runtime reduced by up to 6 times with the new framework.

Industrial tools benefit from the generated rewrite paths for verification.

Abstract

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.