I am new to the formal verification process and I am trying to use it for verifying the connectivity between some modules in a SoC. I am using Incisive Formal SoC Connectivity Solution (V2.01) speadsheet to create the property file for the specified connections.
While verifying the connections I am finding certian issues:
1. The connection status is passed and the connection is visible in schematic but when I view waveform for the same, I get only 0 is driven on both the pins. How can I assure that the connection is verified if only 0 or only 1 is driven for entire simulation cycle? Is there any way to toggle the input on pins with the help of connectivity spreadsheet?
2. When the top file language is specified as verilog in the excel sheet, then the property file created by using the CSV file contains a clock, ifv_connectivity_clk. Where does this clock comes from? I have not specified any such clock in the spreadsheet. At the same time when the top file language is changed to vhdl, no such clock is generated. Why is this so?
I am using PSL assertion language in the excel sheet.
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.
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?