Home > Community > Forums > Functional Verification > Property transformations

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

 Property transformations 

Last post Tue, Nov 7 2006 5:06 AM by archive. 3 replies.
Started by archive 07 Nov 2006 05:06 AM. Topic has 3 replies and 1227 views
Page 1 of 1 (4 items)
Sort Posts:
  • Tue, Nov 7 2006 5:06 AM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,930
    Property transformations Reply

    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
    • Post Points: 0
  • Tue, Nov 7 2006 7:28 AM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,930
    RE: Property transformations 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
    • Post Points: 0
  • Tue, Nov 7 2006 12:47 PM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,930
    RE: Property transformations Reply


    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
    • Post Points: 0
  • Tue, Nov 7 2006 12:54 PM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,930
    RE: Property transformations Reply

    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
    • Post Points: 0
Page 1 of 1 (4 items)
Sort Posts:
Started by archive at 07 Nov 2006 05:06 AM. Topic has 3 replies.