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 and reliability of equivalence checking for large designs.

• Type: Conference
• Year: 2008
• Where: FMCAD
• Authors: Alan Mishchenko, Robert K. Brayton
• Keywords: Equivalence Checking, FMCAD 2008, Formal Methods, Sequential Equivalence, Synthesis Information