In reply to dave_59:
Dave is correct, but the assertion has issues anyways.
The issues
property data_chk;
bit [7:0] push_data;
@(posedge dram_clk) (push, push_data=in_data[7:0])
|-> ##[5:10] pop ##0 ((out_data == push_data);
endproperty
Suppose you have the sequence
PUSH @t0, PUSH @t2, POP @t4
@t0, the assertion will fire and save data0, waiting for a pop
@t2, The assertion will fire and save data2, waiting for a pop
@t4, assertion started @t0 will succeed
@t4, assertion started @t2 will fail if data0 != data2
This is because each of those 2 successfully attempted assertions will terminate.
// <<< The assertion as written is poorly written (even if I gave you that answer :)
// (am Human too :) )
One way to solve this is to use supporting code. For example:
1) Declare at the module level an associative array and an index (int type)
2) In the property, declare a local variable for the write index used in that attempt
3) In the assertion use the sequence_match_item to call a function that does 2 things:
a) save the data into the associative array at that index
b) increment the index
Also, save the index used in that attempt into the local variable of the property
4) in consequent, @ a pop, check that out_data==data_stored_in_associative_array @ saved index
Ben Cohen http://www.systemverilog.us/
- SystemVerilog Assertions Handbook, 3rd Edition, 2013
- A Pragmatic Approach to VMM Adoption
- Using PSL/SUGAR … 2nd Edition
- Real Chip Design and Verification
- Cmpt Design by Example
- VHDL books