Home > Community > Forums > Functional Verification > Need help in assertion based connectivity checking

Email

* Required Fields

Recipients email * (separate multiple addresses with commas)

Your name *

Your email *

Message *

Contact Us

* Required Fields
First Name *

Last Name *

Email *

Company / Institution *

Comments: *

 Need help in assertion based connectivity checking 

Last post Tue, Jan 22 2013 10:41 PM by SnehalC. 7 replies.
Started by SnehalC 30 Dec 2012 10:20 PM. Topic has 7 replies and 1901 views
Page 1 of 1 (8 items)
Sort Posts:
  • Sun, Dec 30 2012 10:20 PM

    • SnehalC
    • Not Ranked
    • Joined on Wed, Dec 26 2012
    • Pune, Maharashtra
    • Posts 4
    • Points 65
    Need help in assertion based connectivity checking Reply

    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

    • Post Points: 35
  • Wed, Jan 2 2013 5:12 AM

    • JoergM
    • Top 500 Contributor
    • Joined on Thu, Jul 17 2008
    • Munich, Bavaria
    • Posts 28
    • Points 550
    Re: Need help in assertion based connectivity checking Reply

    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.

    • Post Points: 20
  • Wed, Jan 2 2013 9:40 PM

    • SnehalC
    • Not Ranked
    • Joined on Wed, Dec 26 2012
    • Pune, Maharashtra
    • Posts 4
    • Points 65
    Re: Need help in assertion based connectivity checking Reply

    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

    • Post Points: 20
  • Thu, Jan 3 2013 12:46 AM

    • JoergM
    • Top 500 Contributor
    • Joined on Thu, Jul 17 2008
    • Munich, Bavaria
    • Posts 28
    • Points 550
    Re: Need help in assertion based connectivity checking Reply

    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.

    • Post Points: 5
  • Mon, Jan 7 2013 2:35 AM

    • JoergM
    • Top 500 Contributor
    • Joined on Thu, Jul 17 2008
    • Munich, Bavaria
    • Posts 28
    • Points 550
    Re: Need help in assertion based connectivity checking Reply

    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.

    • Post Points: 20
  • Mon, Jan 7 2013 9:11 PM

    • SnehalC
    • Not Ranked
    • Joined on Wed, Dec 26 2012
    • Pune, Maharashtra
    • Posts 4
    • Points 65
    Re: Need help in assertion based connectivity checking 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?

    • Post Points: 5
  • Mon, Jan 7 2013 11:07 PM

    • nannasin28
    • Not Ranked
    • Joined on Mon, Jan 7 2013
    • <?xml version="1.0" encoding="utf-16"?><string>shenzhen, Guangdong</string>
    • Posts 10
    • Points 80
    Re: Need help in assertion based connectivity checking Reply
    shows that in 5 cranks all the assertions have toggled and also the duration of high and low signals.
    IRF3205
    http://www.hqew.net
    • Post Points: 5
  • Tue, Jan 22 2013 10:41 PM

    • SnehalC
    • Not Ranked
    • Joined on Wed, Dec 26 2012
    • Pune, Maharashtra
    • Posts 4
    • Points 65
    Re: Need help in assertion based connectivity checking (solved) Reply

    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

    • Post Points: 5
Page 1 of 1 (8 items)
Sort Posts:
Started by SnehalC at 30 Dec 2012 10:20 PM. Topic has 7 replies.