Stats

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

  • 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


  • The suggestion for the conversion into a never {sequence} form is not quite right.
    There are problems with the first expression of the sequence and with
    the timing (repetition value).

    It should be:

        never {req && ! gnt; !gnt[*4]} @(posedge clk);

    The first expression needs to be extended to include " && !gnt"
    The timing needs to be shortened to "*4".
    Beware that the original property used a non-overlapping implication operator.


    Generally it is recommend to double check the converted version using the tool
    by using the following procedure:

    –
    1. put the original and derived property into a dummy module
    2. run the original as a constraint and the derived one as an assertion
    3. prove
    4. reset
    5. flip the original into an assertion and the derive into a constraint
    6. prove
    It is important to check it both ways. Otherwise the constraining of
    one property could mask a problem.

    This could be automated with scirpts

    In this particular case do the following:

    dummy.v:

    module dummy (input clk, output req, gnt);
    // psl P1_orig: assume (always (req) -> {!gnt[*0:4]; gnt}) @(posedge clk);
    // psl P1_derived: assert never {req && !gnt; !gnt[*4]} @(posedge clk);
    endmodule

    dummy.tcl:
    # run1
    prove
    constraint -show

    reset
    # flip it
    assertion  -del -all
    constraint -del -all
    assertion  -add *orig
    constraint -add *derived
    # run2
    prove
    constraint -show


    ifv dummy.v +tcl+dummy.tcl







    Originally posted in cdnusers.org by axels

  • Oops, Axels is right. I read the original sequence as if it used the non-overlapping implication operator |=>, while in fact it appears as if it was supposed to be using the overlapping form of that operator |->.


    Originally posted in cdnusers.org by TAM

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.