Stats

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

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