Variable Delay or Repetition with "until/until_with"

SystemVerilog
, , ,
1

Diverting from Assertion to check variable distance of two signals, I tried implementing variable repetition with until and until_with.

I thought the following 4 properties properly work. However, p_variable_until_with/until don’t work while p_variable_first_match/intersect do.

//             _________
// s1    :  __|<-------> __
// s2    :     _________|
//             + + + + +
// v_cnt :     1 2 . .LEN LEN
//             ^..........*
property p_variable_first_match(s1, s2, LEN);
  int v_cnt = 0;
  ($rose(s1), v_cnt=0) |-> first_match((s1, v_cnt++)[+] ##1 s2) ##0 (v_cnt == LEN);
endproperty
    
property p_variable_intersect  (s1, s2, LEN);
  int v_cnt = 0;
  ($rose(s1), v_cnt=0) |-> ((s1, v_cnt += !s2)[+] intersect s2[->1]) ##0 (v_cnt == LEN);
endproperty
    
property p_variable_until      (s1, s2, LEN);
  int v_cnt = 0;
  ($rose(s1), v_cnt=0) |-> (s1, v_cnt++     ) until      s2 |-> (v_cnt == LEN);
endproperty

property p_variable_until_with (s1, s2, LEN);
  int v_cnt = 0;
  ($rose(s1), v_cnt=0) |-> (s1, v_cnt += !s2) until_with s2 |-> (v_cnt == LEN);
endproperty

These properties were applied to the following tests.

// LEN = 5

// TEST 1 : Expect Pass   ________________
// s1 :  ________________|1 2 3 4 5  _____
// s2 :  ___________________________|

// TEST 2 : Expect Fail   ________________
// s1 :  ________________|1 2 3 4 5 6  ___
// s2 :  _____________________________|

// TEST 3 : Expect Fail   ________________
// s1 :  ________________|1 2 3 4  _______
// s2 :  _________________________|

All properties are expected pass in TEST 1 and fail in TEST2 and TEST3. However, p_variable_until/until_with are pass in all TESTs unexpectedly.
Here is a link to EDA playground.

SVA Dynamic Variable until/until_with usage

Why don’t they work? Does anybody can explain this?

3

property_expr until property_expr | property_expr s_until property_expr | property_expr until_with property_expr | property_expr s_until_with property_expr
are property expressions. Each side of the until has its own copy of the local variables.
en Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.

1 Like
4

Hi @ben2 ,

Thanks.
I understand. I tried the following property with debug printing.

property p_variable_until_debug(s1, s2, LEN);
    int v_cnt = 0;
    ($rose(s1), v_cnt=0, dbg(v_cnt,"INIT")) |-> (s1, v_cnt++, dbg(v_cnt,"INC ")) until s2 ;//|-> ((v_cnt == LEN), dbg(v_cnt,"EVAL")));
endproperty

Then, I got the log message below.

# === TEST 1 : length = 5 Pass       ________________
# s1 : _____________________________|1 2 3 4 5  _____
# s2 : ________________________________________|     
# T:110 v_cnt = 1 INC 
# T:110 v_cnt = 0 INIT
# T:120 v_cnt = 1 INC 
# T:130 v_cnt = 1 INC 
# T:140 v_cnt = 1 INC 
# T:150 v_cnt = 1 INC 
# T:160  : PASS ap_until
# ===================================================
# 
# === TEST 2 : length = 5 Fail       ________________
# s1 : _____________________________|1 2 3 4 5 6  ___
# s2 : __________________________________________|   
# T:360 v_cnt = 1 INC 
# T:360 v_cnt = 0 INIT
# T:370 v_cnt = 1 INC 
# T:380 v_cnt = 1 INC 
# T:390 v_cnt = 1 INC 
# T:400 v_cnt = 1 INC 
# T:410 v_cnt = 1 INC 
# T:420  : PASS ap_until
# ===================================================
# 
# === TEST 3 : length = 5 Fail       ________________
# s1 : _____________________________|1 2 3 4  _______
# s2 : ______________________________________|       
# T:620 v_cnt = 1 INC 
# T:620 v_cnt = 0 INIT
# T:630 v_cnt = 1 INC 
# T:640 v_cnt = 1 INC 
# T:650 v_cnt = 1 INC 
# T:660  : PASS ap_until
# ===================================================

As you can see, v_cnt values are printed expected number of times but its value is not incremented and stays in 1.
This means, v_cnt is copied every time whenever left side property/sequence of until is evaluated.

That is, until/until_with should not be used with dynamically changed local variables.

5

Q: Why local var increment ONCE? (s1, v_cnt++, dbg(v_cnt,"INC ")) until s2
int v_cnt = 0;
($rose(s1), v_cnt++, dbg(v_cnt,“INIT”)) |->
(s1, v_cnt++, dbg(v_cnt,"INC ")) until s2 ;

Code: https://www.edaplayground.com/x/v9hH
wave: https://www.edaplayground.com/w/x/SEG
A: An until property of the non-overlapping form (i.e., until, s_until)
evaluates to true if property_expr1 evaluates to true at every clock tick
beginning with the starting clock tick of the evaluation attempt and
continuing until at least one tick before a clock tick where property_expr2
(called the terminating property) evaluates to true.

In the antecedent ($rose(s1), v_cnt++, dbg(v_cnt,“INIT”)), v_cnt is incremented to 1.
In the consequent ((s1, v_cnt++) until s2), at every clock tick s1 must be true
per the definition of the until, and v_cnt incremented its passed value of 1 by 1
at that clocktick. The process repeats at every clock tick and v_cnt is incremented to thevalue of 2.
Thus, @ t0, the($rose(s1), v_cnt==1 + 1 in the consequent
@ t1, the consequent is re-evaluated, v_cnt= 1+ 1
… process repeats until one tick before a clock tick where s2==1

Note: An until property of one of the weak forms evaluates to true (vacuously or non vacuously)
if property_expr1 evaluates to true at each clock tick, even if property_expr2 never holds.
For a fail, property_expr1 is true and the terminating property) evaluates to false.
Therefore, we can say that
(s1, v_cnt++, dbg(v_cnt,"INC ")) until s2 // isnequivalent to:
(s1, v_cnt++, dbg(v_cnt,"INC ")) |=> s2 ;
because it is an equivalent of the weak until, provided that s1 and s2 are booleans.
We should get the same count values and failures.

Question came from:
Variable Delay or Repetition with "until/until_with" - #3 by ben2

1 Like