In reply to S.P.Rajkumar.V:
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