IFV connectivity Check failure debug

If a signal is shown as X then its value isn't important for the proof result, so I assume that something else is gating the signal and allowing the property to fail regardless of the value of top_scanb. Fail (5) suggests that there is some sequential logic involved since for a combinational connection you should get a 1 cycle result. You haven't provided enough information to understand the root cause of the issue, and unless you want to share more details of your design on this forum, it might be better to open a support case at support.cadence.com so that you can connect with a formal expert who can guide you through debugging the issue.

Hi Stephen,

Thanks for the reply.

This is what I intend to do.

prove that <path1>:clk_out === <path2>:clk_in only when  (<path0>:top_scanb) == 0.

The assertion I wrote is as follows.

assertion -add -interactive { (<path1>:top_scanb == 0) -> ((<path2>:out_clk) === (<path3>:in_clk)) } -name test

Is this assertion correct as per intention?

Kindly help.

Thanks and Regards,

Rajratna

As  Stephen said, you may need to file a ticket with Cadence Customer Support as debugging a problem in these forums can be difficult.

What version of the software are you using? Try adding the "define word_level_reduction off" command to your TCL script before the prove command. It has resolved several problems with counter-examples recently in certain versions of the tool.

Tom

Hi, 

Thanks, I would raise a support ticket.

Thanks and Regards,

Rajratna