Home > Community > Forums > Functional Verification > Property for when writes to a fifo stop

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 for when writes to a fifo stop 

Last post Wed, Feb 21 2007 8:27 AM by archive. 6 replies.
Started by archive 21 Feb 2007 08:27 AM. Topic has 6 replies and 1550 views
Page 1 of 1 (7 items)
Sort Posts:
  • Wed, Feb 21 2007 8:27 AM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,930
    Property for when writes to a fifo stop Reply

    I need a property for formal analysis that says when writes to a FIFO stop, the FIFO eventually empties.  The logic in the module I am verifying does the reading of the FIFO.  I'm trying to verify that the logic will always read everything out.  The write is an input to the module.

    I broke it up into an assumption and an assertion.  Let me know if you think this works or if you have a better idea.  Thanks.

    //psl assume_wr_stops: assume always(
    // eventually! ~write
    //)@(posedge clk);

    //psl assert_eventually_empty: assert always(
    // eventually! empty
    //)@(posedge clk);


    Originally posted in cdnusers.org by weberrm
    • Post Points: 0
  • Wed, Feb 21 2007 8:46 AM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,930
    RE: Property for when writes to a fifo stop Reply

    Hi,

    Unless the read signal was constant, IFV would fail this assertion as by simply alternating the value of write,

    i.e. write 0 1 0 1 0 1 0 1 etc...

    This would satisfy the assumption, but unless the FIFO was always being read, it would never reach an empty state.

    Can you clarify the requirement here, for example when the write stops, do you never expect it to start again?
    If this is the case then you would need another assumption, for example:

    //psl assume_wr_never_restarts: assume always(
    // {~write} |=> {~write}
    //)@(posedge clk);


    Vince.



    Originally posted in cdnusers.org by vincentr
    • Post Points: 0
  • Wed, Feb 21 2007 8:52 AM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,930
    RE: Property for when writes to a fifo stop Reply

    Not quite. I want to say that writes will eventually completely stop and when they do the fifo should eventually empty.  There could be many stops and starts of the writes along the way.


    Originally posted in cdnusers.org by weberrm
    • Post Points: 0
  • Thu, Feb 22 2007 6:58 AM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,930
    RE: Property for when writes to a fifo stop Reply

    I think the answer is to use an abort.

    //psl assert_eventually_empty: assert always(
    // {~empty} |-> {[*] ; empty}! abort (write)
    //)@(posedge clk);

    So, if writes stop, this assertion will check to make sure that the FIFO will evenutally become empty.


    Originally posted in cdnusers.org by weberrm
    • Post Points: 0
  • Thu, Feb 22 2007 12:47 PM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,930
    RE: Property for when writes to a fifo stop Reply

    I don't think you can do this without some verilog code.
    Look at this. I think it should work:


    `ifdef FORMAL_ON

    reg [SIZE-1:0] num_write;
    reg [SIZE-1:0] cnt_write;


    // Let the formal tool pick a value for num_write and keep it stable
    // psl assume_num_write_stable : assume always (stable(num_write));

    // Count numbers of write
    always @(posedge clk)
    begin
    if (reset)
    cnt_write <= 0;
    else if (write)
    cnt_write <= cnt_write+1'b1;
    else
    cnt_write <= cnt_write;
    end

    // if numbers of writes reaches num_write, don't generate any writes anymore
    //psl assume_max_write : assume always ((cnt_write == num_write) -> (~write) @(posedge clk);

    // Force number of write equal to num_write. This will force write to be asserted
    //psl assume_write: assume always (eventually! cnt_write == num_write) @(posedge clk);

    // force read to be asserted. If not, the fifo will never go empty
    // psl assume_read: assume always (eventually! read) @(posedge clk);

    // the fifo should eventually be empty
    //psl assert_empty: assert always (eventually! empty) @(posedge clk);

    `endif FORMAL_ON

    Claude


    Originally posted in cdnusers.org by cbeaureg
    • Post Points: 0
  • Thu, Feb 22 2007 1:58 PM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,930
    RE: Property for when writes to a fifo stop Reply

    Hi Claude,

    Thanks for the reply.  Did you see my last post?  Do you think there is still a problem doing it the way I mention?  If so, can you explain?  Thanks.

    Also, your code puts an assumption on the read.  However, my example was describing a case where the logic being verified is what is reading the fifo.  I am verifying that the logic does indeed empty the fifo if writes stop.

    Ross


    Originally posted in cdnusers.org by weberrm
    • Post Points: 0
  • Fri, Feb 23 2007 6:51 AM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,930
    RE: Property for when writes to a fifo stop Reply

    Ross,

    Yes your solution works fine and is much more elegant than mine!! I tried both solution on some fifo code I had. Both worked.
    I did have to add the constraint on read because I considered as an input to the fifo block.

    Thanks,

    Claude


    Originally posted in cdnusers.org by cbeaureg
    • Post Points: 0
Page 1 of 1 (7 items)
Sort Posts:
Started by archive at 21 Feb 2007 08:27 AM. Topic has 6 replies.