Sequential Equivalence Checking (RTL vs RTL)

[ESD_UNIVR]

Hi,
is there any tool for RTL equivalence checking?

Actually, I found only
SLEC of Calypto Design Systems
http://www.calypto.com/slecrtl.php

Is there any alternative, in particular under some form of Academic license?

Currently I am using Formality for RTL vs RTL equivalence checking but Formality has not been developed for this purpose:

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**.

Any suggestion?

Thanks

 

[jbeniston]

You can use Synopsys Formality or Cadence Conformal.

 

[ESD_UNIVR]

Ok, but I just said that their focus is not on RTL equivalence checking. Any other alternative?

 

[niko_zhang]

who can share the PowerPro?

thanks

 

[aravind]

please elaborate ur question.. WHy u want to do RTL Vs RTL equivalence checking?. Do u want verify functional equivalence of 2 RTL's.. ?..

Is formal verification tools like conformal, formality doesnt statisfy ur problem?.

Aravind