Home > Community > Forums > Functional Verification > keeping rst asserted n clocks into the proof

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: *

 keeping rst asserted n clocks into the proof 

Last post Sun, Nov 19 2006 12:34 PM by archive. 2 replies.
Started by archive 19 Nov 2006 12:34 PM. Topic has 2 replies and 1128 views
Page 1 of 1 (3 items)
Sort Posts:
  • Sun, Nov 19 2006 12:34 PM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,930
    keeping rst asserted n clocks into the proof Reply

    Anyone know how to keep rst_n asserted 16  clocks iinto the proof and then deassert forever  with SVA?  I can do this easily in PSL by using assume and omitting always as in the following PSL:

    // Assert rst_n for 16 clocks, then deassert for one clock. Note absense of "always"
    // It fires once only during the clock 1
    // psl assume_rst_n_low_16: assume {!rst_n[*16];rst_n} @ (posedge clk);
     
    // This property ensures rst_n stays high once it goes high from previous property.
    // psl assume_rst_n_high_rest_of_time: assume always {rst_n}|=> {rst_n};

    I am trying avoid auxilliary code with SVA but I have not come up with a clean way to avoid the aux code.  In fact the aux code I have requires an undriven signal to code a trigger for clock 1 to implement the equivalent of PSL assume_rst_n_low_16 property above.

    JB


    Originally posted in cdnusers.org by jb
    • Post Points: 0
  • Sun, Nov 19 2006 9:15 PM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,930
    RE: keeping rst asserted n clocks into the proof Reply

    I don't want to get too sophistical, but I look at SVA as just another kind of auxiliary verification logic, so I don't understand the motivation for the question. SVA as well as auxiliary logic should be encapsulated into ifdef pragmas anyway to avoid downstream problems in the flow.

    The reason I am saying this is because I don't see a way to write this without aux code in SVA (until IFV supports assertions inside procedural initial blocks, which probably no formal tool supports).


    Originally posted in cdnusers.org by foster
    • Post Points: 0
  • Mon, Nov 20 2006 8:47 AM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,930
    RE: keeping rst asserted n clocks into the proof Reply

    Foster,

    Thanks for confirming you see no other way than using axilliary code to implement this in SVA.  I agree that all this would be encapsulated within `ifdefs to eliminate the code from issues with downstream flow.

    I was simply trying to see if there was a way to implement the functionality in SVA that was possible in PSL.  I have dealt with requests before to keep rst_n asserted into a proof with PSL up till now.  As there are more and more SVA users I wanted to have an implementation in SVA handy for these users.

    jb


    Originally posted in cdnusers.org by jb
    • Post Points: 0
Page 1 of 1 (3 items)
Sort Posts:
Started by archive at 19 Nov 2006 12:34 PM. Topic has 2 replies.