SVA- How we can write property such that it will check the value which is getting generated either by increments or decrements as below

SystemVerilog
,
1

There are below Input signals- WE,WR,RD.
and output signal - USED
When WE = 1, WR = 1, RD = 0. on first clock cycle,
then till `depth-1 cycle , WE=0,WR=0,RD=1,
then finally on N cycle, WE should be 1.

But if in between WR = 0 and RD =1 then Depth should increase by 1 for every such clock.

Any lead …

2

In reply to ADITYA ABHISHEK:
I see two approaches to write such an assertion:

  1. Use the methodology that I address in my paper at
    PAPER: Understanding the SVA Engine + Simple alternate solutions - SystemVerilog - Verification Academy
    There, I use a task that I fire at every clock. The task eases the requirements in SVA to create a counter nd to use the first_match() function. I believe that for complex assertions, this approach is the preferred method. I added some events for debug.
  2. Use SVA with counters amd first_match() function.

Below is code that demonstrates thse 2 solutions, both of them yielding the same results.
// code http://systemverilog.us/vf/write_read.sv


import uvm_pkg::*; `include "uvm_macros.svh" 
module top; 
	bit clk, we, wr, rd;  
	bit[3:0] depth =2;
	event s, e, p; // for debug
	/* There are below Input signals- WE,WR,RD.
		and output signal - USED
		When WE = 1, WR = 1, RD = 0. on first clock cycle,
		then till `depth-1 cycle , WE=0,WR=0,RD=1,
		then finally on N cycle, WE should be 1.

		But if in between WR = 0 and RD =1 then Depth should increase by 1 for every such clock. */ 
	
	task automatic t_write();
		if($rose(we && wr && !rd)) begin : rose_we // attempt succeeds
			-> s; // start 
			repeat(depth-1'b1) begin : DEPTH_REPEAT
				@(posedge clk);
				a_we0_wr0_rd1: assert(we==0 && wr==0 && rd==1'b1); 
				if(we==1'b1 || wr==1'b1 || rd==1'b0) begin 
					-> e; // error 
				    return; 
				end
			end : DEPTH_REPEAT
			@(posedge clk);
		    a_we1: assert(we==1'b1); 
		    if(we==1'b1) -> p; // pass
		    else -> e; 
		end : rose_we
		else return; // not really needed statement 
	endtask
	
	property p_write; 
		bit[3:0] w; 
		($rose(we && wr && !rd), w=depth) |-> 
			first_match((##1 (we==0 && wr==0 && rd==1'b1), w=w-1) [*1:$] ##0 w==1) 
			##1 (we==1'b1);
	endproperty 
	ap_write: assert property(p_write);  		
				
		
	default clocking @(posedge clk); endclocking
	initial forever #10 clk=!clk; 
	always 	@(posedge clk) t_write();
		
 	initial begin 
		repeat(200) begin 
			@(posedge clk);   
			if (!randomize(we, wr, rd)	with 
					{ we dist {1'b1:=1, 1'b0:=1};
					  wr dist {1'b1:=1, 1'b0:=2};
					  rd dist {1'b1:=2, 1'b0:=1};
					}) `uvm_error("MYERR", "This is a randomize error")
					end 
			$stop; 
		end 
endmodule  

....
** Error: Assertion error.
#    Time: 2930 ns  Scope: top.t_write.rose_we.DEPTH_REPEAT.a_we0_wr0_rd1 File: test_r.sv Line: 19
# ** Error: Assertion error.
#    Time: 2930 ns Started: 2910 ns  Scope: top.ap_write File: test_r.sv Line: 39 Expr: we==0
#    Local vars : w = 2
# ** Error: Assertion error.
#    Time: 3410 ns  Scope: top.t_write.rose_we.a_we1 File: test_r.sv Line: 26
# ** Error: Assertion error.
#    Time: 3730 ns Started: 3690 ns  Scope: top.ap_write File: test_r.sv Line: 39 Expr: we
#    Local vars : w = 1
# ** Note: $stop    : test_r.sv(55)

988×354 8.19 KB

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home

3

Thanks ben.

Sorry for the typo actually scenario is like below-
There are below Input signals- WE,WR,RD.
and output signal - USED
When WE(Write Empty) = 1, WR(Write Request) = 1, RD(READ REQUEST) = 0 , USED == 0. on first clock cycle, // Need to start Assertion on this
then till `depth-1 cycle , WE=0,WR=1,RD=0, //Need to check in entire depth-1 cycle.
then finally on N cycle, USED should be equal to depth. //Need to check on the Nth Cycle
We need to check on the N Cycle.

But if in between WR = 0 and RD =1 then Depth should increase by 1 for every such clock.

Any lead …

4

In reply to ADITYA ABHISHEK:
Of the 2 solutions, I prefer the use of tasks instead of SVA for this particular problem.
(code could be made more compact)
In SVA, you need to counter, the first_match(), and the intersect.
code http://systemverilog.us/vf/read_wr2.sv


import uvm_pkg::*; `include "uvm_macros.svh" 
module top; 
	bit clk, we, wr, rd;  
	bit[3:0] depth =2;
	event s, e, p; // for debug
	string tID="RD_WR";
	/* There are below Input signals- WE,WR,RD.
		and output signal - USED
		When WE = 1, WR = 1, RD = 0. on first clock cycle,
		then till `depth-1 cycle , WE=0,WR=0,RD=1,
		then finally on N cycle, WE should be 1.

		But if in between WR = 0 and RD =1 then Depth should increase by 1 for every such clock. */ 
	
	task automatic t_write();
		automatic bit rtn;  
		if($rose(we && wr && !rd)) begin : rose_we // attempt succeeds
			-> s; // start 
			repeat(depth-1'b1) begin : DEPTH_REPEAT
				@(posedge clk);
				a_depth:  assert(depth == $past(depth) - 1'b1) else rtn=1'b1;  
				a_we0_wr0_rd1: assert(we==0 && wr==0 && rd==1'b1) else rtn=1'b1; 
				if(we==1'b1 || wr==1'b1 || rd==1'b0 || rtn==1'b1) begin 
					-> e; // error 
					`uvm_info(tID,$sformatf("%m : error in we %b or wr %b or rd %b or depth %b", we, wr, rd, depth), UVM_LOW);
				    return; 
				end
			end : DEPTH_REPEAT
			@(posedge clk); // last cycle
		    a_we1: assert(we==1'b1) else rtn=1'b1;  
		    a_depth:  assert(depth == $past(depth) - 1'b1) else
		    		begin 
		    			rtn=1'b1; 
		    		    `uvm_info(tID,$sformatf("%m : error in depth %b", depth), UVM_LOW);
		    		end 
		    if(we==1'b1  && depth == $past(depth) - 1'b1 && rtn==1'b0) -> p; // pass
		    else begin 
		    	`uvm_info(tID,$sformatf("%m : error in depth %b  or we %b", depth, we), UVM_LOW);
		    	-> e;
		    end 		    		    	 
		end : rose_we
		else return; // not really needed statement 
	endtask
	
	property p_write; 
		bit[3:0] w; 
		($rose(we && wr && !rd), w=depth) |-> 
			(first_match((##1 (we==0 && wr==0 && rd==1'b1), w=w-1) [*1:$] ##0 w==1) 
				intersect ((##1 depth== $past(depth) -1'b1) [*1:$]))			
			##1 (we==1'b1);
	endproperty 
	ap_write: assert property(p_write);  		
				
		
	default clocking @(posedge clk); endclocking
	initial forever #10 clk=!clk; 
	always 	@(posedge clk) t_write();
		
 	initial begin 
		repeat(200) begin 
			@(posedge clk); #2;   
			if (!randomize(we, wr, rd, depth)	with 
					{ we dist {1'b1:=1, 1'b0:=1};
					  wr dist {1'b1:=1, 1'b0:=2};
					  rd dist {1'b1:=2, 1'b0:=1};
					  depth dist {4'b0001:=1, 4'b0010:=1, 4'b0011};
					}) `uvm_error("MYERR", "This is a randomize error")
					end 
			$stop; 
		end 
endmodule  
UVM_INFO read_wr.sv(25) @ 730: reporter [RD_WR] top.t_write.rose_we.DEPTH_REPEAT : error in we 1 or wr 0 or rd 1 or depth 0010
# ** Error: Assertion error.
#    Time: 730 ns Started: 710 ns  Scope: top.ap_write File: read_wr.sv Line: 52 Expr: we==0
#    Local vars : w = 2
# UVM_INFO read_wr.sv(34) @ 810: reporter [RD_WR] top.t_write.rose_we.a_depth : error in depth 0010
# UVM_INFO read_wr.sv(38) @ 810: reporter [RD_WR] top.t_write.rose_we : error in depth 0010  or we 1
# ** Error: Assertion error.
#    Time: 810 ns Started: 790 ns  Scope: top.ap_write File: read_wr.sv Line: 52 Expr: we==0
#    Local vars : w = 1
# UVM_INFO read_wr.sv(25) @ 1250: reporter [RD_WR] top.t_write.rose_we.DEPTH_REPEAT : error in we 0 or wr 0 or rd 0 or depth 0011
# ** Error: Assertion error.
#    Time: 1250 ns Started: 1230 ns  Scope: top.ap_write File: read_wr.sv Line: 52 Expr: rd
#    Local vars : w = 3
# UVM_INFO read_wr.sv(25) @ 1730: reporter [RD_WR] top.t_write.rose_we.DEPTH_REPEAT : error in we 1 or wr 0 or rd 0 or depth 0001
# ** Error: Assertion error.
#    Time: 1730 ns Started: 1710 ns  Scope: top.ap_write File: read_wr.sv Line: 52 Expr: we==0
#    Local vars : w = 3
....

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