Variable Repetition with "intersect" and [->1] doesn't work

SystemVerilog
, , ,
1

Diverting from Assertion to check variable distance of two signals , I tried creating a property for variable signal repetition with intersect and [->1].

// Waits for v_count == N
property p_variable_repeat_inter_2(s1, s2, N);
    int v_cnt = 0;
    ($rose(s1), v_cnt=0)) |-> ((s1, v_cnt++))[+] intersect (v_cnt == N)[->1]) ##1 $rose(s2) ;
endproperty

However, this doesn’t work. I applied this property to the following tests.

//  === TEST 1 : N = 5, PASS is expected
//                     ________________
// s1 : ______________|1 2 3 4 5  _____|__
// s2 : _________________________|     |__

//=== TEST 2 : N = 5, FAIL is expected
//                     ________________
// s1 :  _____________|1 2 3 4 5 6  ___|__
// s2 :  __________________________|   |__

// === TEST 3 : N = 5, FAIL is expected
//                     ________________
// s1 :  _____________|1 2 3 4  _______|__
// s2 :  ______________________|       |__

// === TEST 4 : N = 5 FAIL is expected
//                     ___________________
// s1 :  _____________|1 2 3 4 5       
// s2 :  _________________________________

PASS is expected in TEST 1 but all tests are FAIL.
Here is EDA Playground link, SVA Variable Repetition with intersect - EDA Playground.
When the debug message is enabled, it looks the internal counter is not stopped and continue counting over 14 in any tests.

Why doesn’t this property work?
Meanwhile, I confirmed the following property works except for TEST 4, no s2 signal return case.

// Waits For s2
property p_variable_repeat_inter_1(s1, s2, N);
    int v_cnt = 0;
    ($rose(s1), v_cnt=0) |-> ((s1, v_cnt+=!s2)[+] intersect s2[->1]) ##0 (v_cnt == N);
endproperty

Shouldn’t we use internal count value to wait for a specific cycle point??
That is, intersect (v_cnt == N)[->1] is not good? Why??

2

I changed the model to explain it better.
The issue is the lack of sharing of local variables in the “and” and "intersect operator, and the flow-out of local variables.
When two sequences are ANDed or INTERSECTed, each sequence produces its own thread. If the sequence makes assignments to local variables, then each of the sequence involved in the ANDing or INTERSECTing carries its own individual and separate copy of the local variables. However, only those local variables that are NOT assigned in both threads flow out of the sequence. Thus, it is illegal to have the same variables being assigned in each of the threads and have that variable flow out of the sequence because the outputs of these operators produce a single end point with updated values for the variables. In something like: SVA Variable Repetition with intersect(4) - EDA Playground // code
EPWave Waveform Viewer // wave
property p_variable_repeat_inter_2(s1, N);
int v_cnt=0;
($rose(s1)) |->
((s1, v_cnt++)[+] intersect (s2, dbg(v_cnt,"v_cnt==N "))[->1])
##0 (1, dbg(v_cnt,"v_cnt_end==N "));
endproperty
LHS sequence ((s1, v_cnt++)[+] increments its own copy of local variable RHS sequence (s2, dbg(v_cnt,"v_cnt==N "))[->1]) also carries
its own copy of the local variable, which is separate from the LHS sequence and remains at 0.Since only one of the 2 sequences updates the local variable, it flows out.

1 Like
3

Thanks, @ben2 .

I understand. So, we should not use dynamically changed local variables in the both side of intersect since the copied ones are used in each side. Signals should be referred to stop local variables counting in case of variable delays and repetition.

4

You are correct. No visibility. The flow out of the local vr is dependent on these of the “and”, intersect, or the “or”.
lack of sharing is also in ORing; there each thread ORs separately upon conclusion:
((s, v++) ##1 s2) or (s3, v=v+2) ) ##0 s4==v;
// same as
((s, v1++) ##1 s2 ##0 s4==v1) or
((s3, v0=v0+2) ##0 s4==v0);
// 2 separate copies of v