Any experience of Equivalence Checking tools?

[RCIngham]

Greetings all,

Has anyone hereabouts any experience with the use of Equivalence Checkin
tools in an FPGA context, for instance OneSpin EC-360 or Mentor FormalPro?

Thanks in anticipation,
Robert





---------------------------------------
Posted through http://www.FPGARelated.com

 

[HT-Lab]

On 09/05/2013 13:27, RCIngham wrote:

Greetings all,

Has anyone hereabouts any experience with the use of Equivalence Checking
tools in an FPGA context, for instance OneSpin EC-360 or Mentor FormalPro?

Thanks in anticipation,
Robert

---------------------------------------
Posted through http://www.FPGARelated.com

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
www.ht-lab.com

 

[Bart Fox]

Hello Robert!

Am 09.05.13 14:27, schrieb RCIngham:

Has anyone hereabouts any experience with the use of Equivalence Checking
tools in an FPGA context, for instance OneSpin EC-360 or Mentor FormalPro?

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