Stats

  • Locked Locked
  • Replies 3
  • Subscribers 64
  • Views 13645
  • 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

Property transformations

archive

There are many ways of specifying the same behaviour by writing a variety of PSL/SVA assertions.
For example, a specification says that after req the grant should come within 5 clock cycles. I wrote it
like

// psl property P1:  (always ( req ) -> {!gnt[*0:4] ; gnt } ) @ (posedge clk);

how do I write this same property using the never form ?
Can this behaviour be written in any other form ? What are the advantages disadvantages of these
different forms.

TG


Originally posted in cdnusers.org by TG
Parents

  • You could write it in the "never" form by saying, "we'll never see grant low for more than 4 clock cycles after a request."

    // psl property P1: never { req; !gnt[*5] };

    What you lose with this form is the concept of a "trigger." When you use the implication operator, the tool will keep track of the number of times the check was triggered, in this instance the number of times a request was made. In the "never" form, there is no specific trigger for the assertion, it checks for the sequence at every cycle.


    Originally posted in cdnusers.org by TAM
Reply

  • You could write it in the "never" form by saying, "we'll never see grant low for more than 4 clock cycles after a request."

    // psl property P1: never { req; !gnt[*5] };

    What you lose with this form is the concept of a "trigger." When you use the implication operator, the tool will keep track of the number of times the check was triggered, in this instance the number of times a request was made. In the "never" form, there is no specific trigger for the assertion, it checks for the sequence at every cycle.


    Originally posted in cdnusers.org by TAM
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.