It is not possible to refer to a local variable from outside the property. Most people separate the data functionality checking from the protocol checking by using a scoreboard.
Scoreboard checks that the data that was pushed matches the data that was popped.
Assertion checks that pop comes between 5-10 clock cycles after push.
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
Could you please help me understand how will the assertion started @t2 will fail at the completion of @t0 at time t=4? Are they not two independent active threads?
For assertion @t2, is the consequent check suppose to happen in the duration #[5:10]? i.e, at t=6 onwards?
=== @t4, assertion started @t2 will fail if data0 != data2
This is because each of those 2 successfully attempted assertions will terminate.
On second thoughts, the problem with this assertion for the fifo is uniqueness.
Below is a way to fix this using tags to force uniqueness. What I mean here is that yoou
don’t want a pop to complete 2 separate threads, as shown in the simulation results for
ap_data_checker_bad where one pop terminates both threads. http://SystemVerilog.us/fifo_aa.png // simulation results http://SystemVerilog.us/fifo_aa.sv
Concept is similar to tags used at hardware stores (pint dpt) with “now serving ticket x”)
module fifo_aa;
bit clk, push, pop;
int tag_in, tag_out;
bit [7:0] in_data, out_data;
initial forever #5 clk=!clk;
property p_data_chk_bad; // problem is uniqueness <-------******
bit [7:0] push_data;
@(posedge clk) (push, push_data=in_data[7:0])
|-> ##[1:10] pop ##0 (out_data == push_data);
endproperty
ap_data_checker_bad: assert property(p_data_chk_bad);
function void inc_tag_in();
tag_in = tag_in + 1'b1;
endfunction
property p_data_unique; // ***** THE FIX
bit [7:0] push_data;
int v_tag;
@(posedge clk) (push, push_data=in_data[7:0], v_tag=tag_in, inc_tag_in())
|-> ##[1:10] pop && tag_out==v_tag ##0 (out_data == push_data);
endproperty
ap_data_unique: assert property(p_data_unique) tag_out =tag_out+1; else tag_out =tag_out+1;
initial begin
#15;if (!randomize(in_data)) $display("error");
@(posedge clk) push <=1'b1;
out_data <= in_data;
@(posedge clk) push <= 1'b0;
//if (!randomize(in_data)) $display("error");
@(posedge clk) push <=1'b1;
@(posedge clk) push <= 1'b0; pop <= 1'b1;
@(posedge clk) pop <= 1'b0; out_data <= in_data;
@(posedge clk) push <= 1'b0;
pop <= 1'b1;
@(posedge clk) pop <= 1'b0;
end
endmodule
Thank you for the explanation and the details. It is infact getting terminating only when both the push data are same as the 2nd consequent is matched immediately at first pop only.
Just to check my understanding, I think the same issue (in case WRITE → WRITE → READ, assuming the first two writes are writing same data) would be seen in the clock domain assertion specified in one of the recent posts. We need to take a similar care for this assertion too. Correct?
