Any experience of Equivalence Checking tools?

Hi Robert,

From my limited experience I can tell that EC tools are a great solution for RTL to RTL but RTL to gate could give you some grey hairs.

The problem with RTL to gate (or synthesis netlist) is that all synthesis tools complicate the EC process by adding/removing registers (register retiming, physical synthesis), choosing fsm encoding, inferring DSP's, convert gate clocks etc.

Luckily a high-end synthesis tool (like Precision/Synplify) can help the EC process by generating an EC guide file (e.g. Precision's FYI file) which basically tells the EC tool what it has done. However AFAIK this guide file is not produce by XST/QNS/Vivado(?) so you might have to budget in a high-end synthesis tool.

Hans

Hello Robert!

Am 09.05.13 14:27, schrieb RCIngham:

A while around I've take some action with OneSpin. The goal was to show that xst procuduce correct netlists. It was a bit tricky to get all running with scripts, but in the end it showed us some VHDL constructs that are problematic for the synthesizer.

regards, Bart