Stats

  • Locked Locked
  • Replies 7
  • Subscribers 66
  • Views 16326
  • Members are here 0
This discussion has been locked.
You can no longer post new replies to this discussion. If you have a question you can start a new discussion

Need help in assertion based connectivity checking

SnehalC

Hi,

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.

Regards,

Snehal

Parents

  • 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?

Reply

  • 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?

Children
No Data

Community Guidelines

The Cadence Design Communities support Cadence users and technologists interacting to exchange ideas, news, technical information, and best practices to solve problems and get the most from Cadence technology. The community is open to everyone, and to provide the most value, we require participants to follow our Community Guidelines that facilitate a quality exchange of ideas and information. By accessing, contributing, using or downloading any materials from the site, you agree to be bound by the full Community Guidelines.