SVA: Counting and Comparing

Hi,
I have a signal “A” that has random pulses and another signal “B” that has random pulses.
I need to count the number of pulses that “A” has and “B” has in a certain period.
After that, compare them e.g. A has 30% more pulses than B.
The count has to be in real format.

Please assist on how to implement such a check using SVA.
I have read about using variables but I cannot pass the variable because it is local.

One method would be to use 3 assertions.
1st assertion to check for pulse at A and increase a global countA
2nd assertion to check for pulse at B and increase a global countB
3rd assertion to compare countA and countB

Please recommend if there is a more efficient way.

In reply to sonofthesand:
The easiest solution is to use plain SystemVerilog code, as shown below:
and in Edit code - EDA Playground

// import uvm_pkg::*; `include "uvm_macros.svh" 
module top; 
	bit clk, a, b, go, done;  // go and done are single pulses
	int acnt, bcnt, stats;
	default clocking @(posedge clk); endclocking
	initial forever #10 clk=!clk;  
	
	initial begin // signal generator 
		repeat(30) begin 
			@(posedge clk) go <= 1'b1; 
			@(posedge clk) go <= 1'b0; 
			repeat(27) @(posedge clk); 
			done <= 1'b1;
			@(posedge clk) done <=1'b0;
		end 
	end 	
	// verification ode 
	always_ff  @(posedge clk)  begin :ctab
		static int cta;
		static int ctb;
      if(go) begin cta=0; ctb=0; end 
		if(done) begin 
			$display("t=%t, cta=%d, ctb=%d", $time, cta, ctb);
          dostats(cta, ctb);
		end
      if(a) begin cta=cta+1'b1; end
      if(b) begin ctb=ctb+1'b1; end
	end 	
 
	
	function void dostats (int x, y); 
		 acnt=x; 
		 bcnt=y;
		 stats= 100*x/y;
      $display("@t= %t, acnt=%d, bcnt=%d, stats=%d percent", $time, acnt, bcnt, stats); 
	endfunction : dostats
	
	initial begin // signal generator
		repeat(1200) begin 
			@(posedge clk);   
			#1 if (!randomize(a, b)  with 
					{ a dist {1'b1:=1, 1'b0:=3};
					b dist {1'b1:=1, 1'b0:=2};
                    });
					end 
					$stop; 
		end 
endmodule    

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us


In reply to ben@SystemVerilog.us:
If you insist on writing the code in SVA, then consider the following


// SVA SOLUTION THAT WILL NOT WORK !!!! 
property WILL_NOT_WORK_countab;
  int va=0, vb=0;
     go |-> ##[1:$] (a || b, va=va+a, vb=vb+b) ##0 (done, dostats(va, vb)); 	
endproperty 		
ap_LOOKS_LIKE_IT_WILL_WORK_BUT_DOES_NOT_WORK: assert property( p_countab); 

​The property shown below fails to work because in SVA, if the sequence makes assignments to local variables, then each of the sequence involved in the ORing carries its own individual and separate copy of the local variables.
the (##[1:$] seq) is same as (##1 seq or ##2 seq or … ##n seq)

The following will work though because the property calls a task as a match item, and pass whatever values are needed. Thus,


	task do_calc(int va, vb, bit go, done); 
		static int cta;
		static int ctb; 
		if(go) begin cta=0; ctb=0; end
		if(done) begin 
			$display("t=%t, calc_cta=%d, calc_ctb=%d, stats=", $time, cta, ctb, 100*cta/ctb);
		end
		if(a) cta=cta+1'b1; 
		if(b) ctb=ctb+1'b1;
	endtask 	
	
	property p_countab_ok;
		int va=0, vb=0;
		(go, do_calc(va, vb, go, done)) |-> 
                     (##[1:$] (a || b, do_calc(va, vb, go, done)) ##0 done) or 
                     (done[->1], do_calc(0, 0, 0, done)); 	
	endproperty 	
	ap_countab_ok: assert property(p_countab_ok);  			 

Simulation file is at http://SystemVerilog.us/fv/countpulses.sv
sim results

# t=                 650, ctab_cta=          7, ctab_ctb=          6, stats=        116
# t=                 650, calc_cta=          7, calc_ctb=          6, stats=        116
# t=                1250, ctab_cta=         12, ctab_ctb=          9, stats=        133
# t=                1250, calc_cta=         12, calc_ctb=          9, stats=        133
# t=                1850, ctab_cta=         12, ctab_ctb=          8, stats=        150
# t=                1850, calc_cta=         12, calc_ctb=          8, stats=        150

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us


In reply to ben@SystemVerilog.us:

Hi Ben
Thank you for the explanation and solution. I have one question in the solution. For property which is working, I think we donot need local variables in the property. I have made some modifications below. Please let me know your views.

property p_countab_ok;
	//int va=0, vb=0;
	(go, do_calc(0, 0, go, done)) |-> 
                 (##[1:$] (a || b, do_calc(a, b, go, done)) ##0 done) or 
                 (done[->1], do_calc(0, 0, 0, done)); 	
endproperty 	
ap_countab_ok: assert property(p_countab_ok);

In reply to Sudarshan:
Agree, after more thought, you do not need local variables.
In my solution, the local variables kind of remained, as I started with that solution, and they were not optimized out. Yes, they do nothing here.
Ben