Stats

  • Locked Locked
  • Replies 2
  • Subscribers 64
  • Views 13394
  • 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

keeping rst asserted n clocks into the proof

archive

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

  • 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

  • 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

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.