If I want to perform logical equivalence checking on a large design, which is the best option?

[leeway64]

I am running abc to perform retiming on a large design, and I want to make sure that the circuit pre-retiming and post-retiming are logically equivalent. Note that retiming might move and/or remove D flip-flops. The design in question has combinational and sequential elements.

If I want to perform logical equivalence checking on a large design, which is the best option?

1. Using Yosys's equiv_simple, equiv_induct, and equiv_make commands
2. Using Yosys's miter and sat commands
3. Using EQY
   • If EQY is the best option, is there an engine and a solver that is well-suited for large designs?

I'm open to any and all suggestions. Thank you! 😄