SVA: Counting and Comparing

SystemVerilog
, ,
3

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