Recording Synthesis History for Sequential Verification

Performing synthesis and verification in isolation has two undesirable consequences: (1) verification runs the risk of becoming intractable, and (2) strong sequential optimizations are not applied because they are hard to verify. This paper develops a methodology for sequential equivalence checking using feedback from synthesis. A format for recording synthesis information is proposed. An implementation is described and experimentally compared against an efficient general-purpose sequential equivalence checker that does not use synthesis information. Experimental results confirm expected substantial savings in runtime of equivalence checking for large designs.