Certified Sequential Sweep Without Unrolling

From bibtex.

Abstract

Verifying retiming followed by additional sequential resynthesis steps remains challenging for existing tools, limiting aggressive optimizations. Commonly-used equivalence checking tools rely on internal resynthesis operations and error-prone orchestration of different model checkers, which makes certification difficult or even infeasible. We present an IC3-based technique that uses retiming as a preprocessing step and uses simulation to generate suspected invariants. Our technique efficiently verifies sequential equivalence problems under retiming and arbitrarily strong sequential resynthesis, and has the additional feature of producing certificates all the same. Our results on a selection of retimed and resynthesized open circuit designs show that our rather simple approach vastly outperforms the whole portfolio of the winner of the latest Hardware Model Checking Competition as a representative of general-purpose certifying model checkers. Compared to non-certifying approaches, like the mature equivalence checker of ABC, we are still competitive with additional complementary strengths.