Assertion: Expected data check // A review from a user's question

SystemVerilog
,
4

In reply to davidct:
The following code may help you. You need to dig in to understand it.
The ticket, my_ticket, now_serving stuff emulates what happens in something you experienced in a hardware store, like the paint dpt where every customer wants service, but there is only one attendant. So the ticket system provides exclusivity.
In this model, @go, data → Q. @ rdy, out==1st element of the Q. Other assertions do ot respond to this rdy because they do not have the “right ticket”, i.e., one customer to each rdy.
// Model also at http://SystemVerilog.us/vf/question2.sv
Also, see my paper at
PAPER: Understanding the SVA Engine + Simple alternate solutions | Verification Academy
Abstract: Understanding the engine behind SVA provides not only a better appreciation and limitations of SVA, but in some situations provide features that cannot be simply implemented with the current definition of SVA. This paper first explains, by example, how a relatively simple assertion example can be written without SVA with the use of SystemVerilog tasks; this provides the basis for understanding the concepts of multithreading and exit of threads upon a condition, such as an error in the assertion. The paper then provides examples that uses computational variables within threads; those variables can cause, in some cases, errors in SVA. The strictly emulation model with tasks solves this issue.


import uvm_pkg::*; `include "uvm_macros.svh" 
module top; 
	bit clk, go, ready, rst=0;  
	int now_serving=1, ticket=0; 
	int q_data[$], data, pipe1, pipe2, out;
	initial forever #10 clk=!clk;  
	function automatic void push_data(int data); 
		q_data.push_back(data); 
	endfunction : push_data 
	function automatic int get_ticket(); 
	    ticket=ticket+1'b1;
		return ticket; 
	endfunction : get_ticket  	
	/* ap_go_ready: assert property(
	  @(posedge clk) disable iff (rst)
		($rose(go), push_data(data)) |-> 
		 ready[->1] ##0 out == q_data.pop_front());*/ 
	// * Error: question2.sv(11): The method 'pop_front' is not allowed in assertions as it has side effects.
	
	task automatic t_check_data(int my_ticket); 
		forever begin 
			@(posedge clk) if(ready && my_ticket==now_serving) begin : is_ready	
					a_data_check: assert(out == q_data.pop_front());
					$display("@ %t my_ticket", $time, my_ticket); 
					now_serving <= now_serving+1'b1;
					return;
				end 
				// ready[->1] ##0 out == q_data.pop_front());
		end 
	endtask 	
	
	property p_go_ready;
		int my_ticket;
		@(posedge clk) disable iff (rst)
		($rose(go), push_data(data), my_ticket=get_ticket()) |-> 
                      (1,t_check_data(my_ticket)); 
	endproperty
	
	ap_go_ready: assert property(p_go_ready);	
	always_ff  @(posedge clk)  begin 
		if(go) begin 
			pipe1 <= data; 
			pipe2 <= pipe1;
		end
	end 	
	/* So when $rose(go) occurred twice, the payload was also updated twice before ready == 1.
When ready ==1, the payload had 2nd data but ready==1 with out was expecting the 1st data.
So I got a FAIL in simulator.
How to update the assertion to add a pipeline or FIFO so that the payload data gets
properly matched up with corresponding ready ?
Also, maybe make the FIFO/pipeline generic enough to have an N-deep and store more levels.*/


	initial begin 
		repeat(200) begin 
			@(posedge clk);   
			if (!randomize(data, go, ready)  with 
					{ data inside {[1:200]};
					  go dist {1'b1:=1, 1'b0:=3};
					  ready dist {1'b1:=1, 1'b0:=7};

					}) `uvm_error("MYERR", "This is a randomize error")
					end 
					$stop; 
		end 
endmodule  
/* simulation 
** Error: Assertion error.
#    Time: 350 ns  Scope: top.t_check_data.is_ready.a_data_check File: question2.sv Line: 23
# @                  350 my_ticket          1
# ** Error: Assertion error.
#    Time: 370 ns  Scope: top.t_check_data.is_ready.a_data_check File: question2.sv Line: 23
# @                  370 my_ticket          2
# ** Error: Assertion error.
#    Time: 390 ns  Scope: top.t_check_data.is_ready.a_data_check File: question2.sv Line: 23
# @                  390 my_ticket          3
# ** Error: Assertion error.
#    Time: 550 ns  Scope: top.t_check_data.is_ready.a_data_check File: question2.sv Line: 23
# @                  550 my_ticket          4
# ** Error: Assertion error.
#    Time: 770 ns  Scope: top.t_check_data.is_ready.a_data_check File: question2.sv Line: 23
# @                  770 my_ticket          5
# ** Error: Assertion error.
#    Time: 790 ns  Scope: top.t_check_data.is_ready.a_data_check File: question2.sv Line: 23
# @                  790 my_ticket          6
# ** Error: Assertion error.
#    Time: 850 ns  Scope: top.t_check_data.is_ready.a_data_check File: question2.sv Line: 23
# @                  850 my_ticket          7
# ** Error: Assertion error.
#    Time: 870 ns  Scope: top.t_check_data.is_ready.a_data_check File: question2.sv Line: 23
# @                  870 my_ticket          8
# ** Error: Assertion error. */

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr