Assertion check for a signal which depends on 2 other signals

SystemVerilog
,
6

In reply to muralidar:

In reply to ben@SystemVerilog.us:
Thanks for reply. It helped me a lot and i changed my assertion little to have proper checks as per my requirement.

:)

I have a question that how can we pass a variable inside a property.
ex: if i need to wait 4 repetitions of signal a I use a[->4], in the same way if i want to use a variable in place value 4 like a[->x]. so here x is configurable. I want to use variable because it is configurable from 0 to 7.

I explain another approach in my SVA Handbook 4th Edition, 2016 If the variable used to define the delay has values that are within a constraint range, such as between 0 and 7 (or 15, or at most 32) one can use the generate statement, which appears much simpler than the use of local variables and the sequence_match_item. Example:


generate for (genvar g_i=0; g_i<8; g_i++) begin
  ap_delay_gen: assert property (v==g_i && $rose(a) |-> ##g_i b);
end endgenerate

For your assertion, you can do the following, but keep in mind that with the generate statement and more variables, you have many assertions. The generate is used because it creates static values after elaboration. The full model is at
http://SystemVerilog.us/vf/repabc2.sv
the pertinent part is shown below:


module top; 
	bit clk, a, c, go=1;  
	bit[2:0] b=5, d=2; // delay variables for assertions
    generate for (genvar g_i=0; g_i<8; g_i++) begin // one variable 
		property p_abc_timing2; 
		   @(posedge clk)
		  (b==g_i && go && $rose(a), setgo(0)) ##1 a[->3] ##g_i 1'b1 
                       |-> ##[1:4] $rose(c);
		endproperty
		ap_abc_timing2: assert property(p_abc_timing2) setgo(1); else setgo(1);  
    end endgenerate  
		 
	generate for (genvar g_i1=0; g_i1<8; g_i1++) begin : t1// two variables
	   for (genvar g_i2=0; g_i2<8; g_i2++) begin : t2// two variables 
		property p_abc_timing3; 
		  @(posedge clk)
		   (b==g_i1 && d==g_i2 && go && $rose(a), setgo(0)) ##1
                      a[->g_i2] ##g_i1 1'b1 
                             |-> ##[1:4] $rose(c);
		endproperty
		ap_abc_timing3: assert property(p_abc_timing3) setgo(1); else setgo(1);  
	  end  // : t2
	end endgenerate // : t1

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