Assertion check for a signal which depends on 2 other signals

SystemVerilog
,
4

In reply to muralidar:

In reply to ben@SystemVerilog.us:
I have a common clk for all 3 signals(a,b,c) of same module.

[Ben] Thus, as you know, with a clock, SVA samples the signals in the Preponed region (i.e., a delta time just before the edge of the clock).

My requirement is that signal a repeats for 3 times but not for every clk then i need to wait for delay of value b then c signal should start rising from 0 to 1.

[Ben] I hope that you studied SVA, because, if you did, you will recall the The goto repetition operator (Boolean[->n]) allows a Boolean expression (and not a sequence) to be repeated in either consecutive or non-consecutive cycles, but the Boolean expression must hold on the last cycle of the expression being repeated. The number of repetitions can be a fixed constant or a fixed range.

The signal a sample on posedge clk but repetition of signal a is not dependent on clk.

[Ben] that part is ambiguous; how can “a” be both generated off of a clock, but yet not be dependent on a clock. Maybe what you mean is that “a” is synchronous to a clock, but can repeat at different cycles, or th repeat is not consecutive (e.g., 1 0 0 1 1 0 0 0 0 1).

the second/ occurrence of signal a may happen after more no of clks(ex: 4/5/6). basically we should not be dependent on clk while checking signal for repetition.

[Ben] Again the contradiction! SVA IS dependent on the clock and the sampling of the signals are in the Preponed Region. I think that what you mean is that the occurrences of “a” at not necessarily consecutive.

I have written something like this: But it results in below compilation Error.
Can you please correct me if iam doing some thing wrong.
property a_b_c_timing;
@(posedge clk)
@(posedge a)
(a[*4]) b |-> $rose(c)
endproperty
assert_a_b_c_timing_chk: assert property(a_b_c_timing)

[Ben] Your assertion is complex. I took a stab at it.
Full simulation model is at http://SystemVerilog.us/vf/repabc.sv
Pertinent code:

 
        function void setgo(bit x); 
		go=x; 
	endfunction : setgo
	
	property p_abc_timing;
		int vt; 
		@(posedge clk)
			(go && $rose(a), setgo(0), vt=0) ##1 a[->3] ##1 
			first_match((1, vt=vt+1'b1)[*1:$] ##0 b==vt) |-> ##[1:4] $rose(c);
	endproperty
	ap_abc_timing: assert property(p_abc_timing) setgo(1); else setgo(1);

Assertion says: if(rose(a), disable other starts of “a” with the go.
then wait for 3 occurrences of “a”, then start count variable vt until vt==b.
Then wait for 1 to 4 cycles for rose(c).
if assertion pass or fails, set go to 1 to enable other starts.
The first_match() is needed because of the ##[1:$]
Change what you need to match your requirements.
Simulation results

1100×604 39.8 KB

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