Assertion for time between two signals

SystemVerilog
1

Hi all,

I have a question related to the SystemVerilog Assertions. Sorry if the question is stupid. I know that it can be done and I found the code in a book a few days ago but do not remember in which book.

I have two signals start and ready. If start is asserted it takes approx. 1000 clock cycles (exact number depends on hardware => I do this with a rand function) until the ready signal is asserted. It is not allowed that start is asserted once again as far as ready was not asserted. I think I remember that this can be done with eventually!, but I’m not sure.

Thank you very much for helping and once again sorry for this beginner question!
Kind regards
Sebastian

2

Taking a closer look at your requirements:

  1. If start then ~1000 clock cycles ready
  2. start should not be followed by another start until ready

The following assertion expresses these requirements:


ap_start_ready: assert property(@(posedge clk)
           start |=> !start[*1:1000] ##0 ready);  
You can substitute $ for the 1000
You can also make the consequent a strong (e.g., 
ap_start_ready2: assert property(@(posedge clk)
           start |=> strong(!start[*1:1000] ##0 ready));
Could also add a 2nd assertion: 
 ap_never_start_ready: assert property(@(posedge clk)
           not(start && ready));

The eventually is a property operator. (s_eventually p) almost equivalent to
(##0 1’b1 #-# p) or (##1 1’b1 #-# p). . . or (##n 1’b1 #-# p) // n== infinity
Thus, one could write the following, but that WOULD NOT BE CORRECT FOR YOUR CASE:


ap_INCORRECT: assert property(@(posedge clk)
           start |=> s_eventually !start ##0 ready);  
// The following sequence would not fail ap_INCORRECT because of the implied "or" operator 
let start=s; 
let ready=r;

s &&!r ##1 !s &&!r ##1 s &&!r##1 !s &&!r ##1 !s &&r would pass with the s_eventually
What is required in the consequent is !start (with a repeat operator) until ready

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us