Certified Sequential Sweep Without Unrolling

Tobias Seufert, Christoph Scholl

Verifying retiming followed by additional sequential resynthesis steps remains challenging for existing tools, limiting aggressive optimizations. Commonly-used equivalence checking…