Need help in assertion based connectivity checking

Hi Snehal,

1) IEV verifies the connection using all possible values within one single proof. The witness you see when opening the waveform browser is only 1 example of a scenario that fulfils the property. You can assume that the fomal engine considers all values, not only the one displayed in the witness example waveform. There is one caveat: Usually we cutpoint the drivers of the source of the connection so IEV has the freedom to consider any possible value. If for some reason your environment keeps logic driving the source pin, it may cause incomplete analysis with a restricted set of values. There are a few options to obtain the coverage in that case:

  a) write a cover on the signal and prove (e.g. using an interactive property like "assert -add -interactive {my.sig == 1'b1} -cover"
  b) use the builtin toggle coverage and enable it for the signal in question

2) The ifv_connectivity_clk is only generated with SVA in my trials, not with PSL. The reason is that SVA requires a clocking statement for any property, even if they describe combinational behavior like connectivity. PSL does not. Can you confirm you observe this with PSL?

Jörg.

Hi Joerg,

When I ran the same script with PSL, clock was not generated. I previously though that it was due to the HDL language (VHDL/Verilog).

I had one more question: How do we enable the builtin toggle coverage? I was not able to find any such option in the tool.

Your information was really useful for me. Thanks a lot.

Regards,

Snehal

Hi Snehal,

you need to add "+enable_togglecheck" to the iev commandline in order to infer the automatic toggle checks. please refer to chapter 10 of the Formal Verifier User Guide for details on "Toggle Checks".

Jörg.

Hi Snehal,

I would like to add that in the next release 13.1 we will add covers to the connectivity checks that make sure we do not validate a stuck connection.

Thanks again for your query.
Jörg.

Hi Joerg,

Thanks a lot for the help you provided. I could find out coverage now.

It is good to hear that covers are being added to connectivity checks.

While I was trying some more options in IFV, I found the option for the debug solver waveform. I added searchpoints and ran the search command for 5 cranks. The debug -solver command gave me a waveform which shows that in 5 cranks all the assertions have toggled and also the duration of high and low signals.

I wanted to confirm if these results are relevant to the proofs I got? They are much easy and less time consuming to get too.

Thanks a lot again.

Snehal

I found that when I run only search N command, the status of assertion is "Explored". [I tried with high effort and N as large as 1000] But when I issue Pass command, the status is "Pass". What might be the reason of his happening?

Hi,

Got this doubt cleared. The sarch command will never show a pass result it will always show explored for the assertions that are passing. This is because search command runs a simulation .It will not run exhausively. We need to issue prove command to thorougly verify the design.

Thanks a lot for help.

Regards,

Snehal