Sequential Equivalence Checking (RTL vs RTL)

Retiming Verification Using Sequential Equivalence Checking, Brian Kahne, Magdy Abadir, MTV 2005

One possibility for accomplishing this task (nota GDG: Equivalence Checking
RTL vs RTL) would be the use of equivalence checkers which were
traditionally oriented towards combinational equivalence checking but have
some sequential capabilities [2][3]. The advantage is that these tools are
well known to designers and are fairly mature. However, the tools are still
primarily oriented towards verifying the output of a synthesis tool. These
tools are able to deal with some changes in state encoding, allowing a
synthesis tool to perform some retiming operations. However, the debug
environment is not ideally suited to RTL designers: The user is presented
with a schematic displaying gate-level differences between the two designs,
without benefit of a waveform or stimulus.

[2] Cadence, “Conformal-Ultra Product Information.”
http://www.cadence.com/products/digital_ic/conformal.
[3] Synopsys, “Formality Product Information.”
**broken link removed**.

Click to expand...