Automated Formal Equivalence Verification of Pipelined Nested Loops in Datapath Designs

TL;DR

This paper introduces a scalable formal method for verifying the equivalence of pipelined nested loop datapath designs against high-level specifications, significantly improving efficiency over existing SMT and SAT approaches.

Contribution

It proposes a modular, segment-based equivalence checking approach using M-HED, enabling scalable verification of complex pipelined designs with notable efficiency gains.

Findings

Achieves 16.7x reduction in memory usage

Achieves 111.9x reduction in runtime

Successfully verifies large, real-world designs

Abstract

In this paper, we present an efficient formal approach to check the equivalence of synthesized RTL against the high-level specification in the presence of pipelining transformations. To increase the scalability of our proposed method, we dynamically divide the designs into several smaller parts called segments by introducing cut-points. Then we employ Modular Horner Expansion Diagram (M-HED) to check whether the specification and implementation are equivalent or not. In an iterative manner, the equivalence checking for each segment is performed. At each step, the equivalent nodes and those nodes which have an impact on them are removed until the whole design is covered. Our proposed method enables us to deal with the equivalence checking problem for behaviorally synthesized designs even in the presence of pipelines for nested loops. The empirical results demonstrate the efficiency and scalability of our proposed method in terms of run-time and memory usage for several large designs synthesized by a commercial behavioral synthesis tool. Average improvements in terms of the memory usage and run time in comparison with SMT- and SAT-based equivalence checking are 16.7x and 111.9x, respectively.