Assertion to check variable distance of two signals

SystemVerilog
, , ,
8

There is a large number of experts who abhor the use of the first_match
because of efficiency; also, it is not used in PSL.
Below is another option without the first_match.
I like the v_cnt += !s2

//              ______________
// s1    :   __|<---------> __      
// s2    :      ___________|
// v_cnt :      0
//              + + + + + +
//              1 2 3 . .len len
//              ^............*
property p_inter_pos_length(s1, s2, len);
  int v_cnt = 0;
  // $rose(s1) ##0 first_match( (s1, v_cnt += !s2)[*1:$] ##0 s2 ) |-> (v_cnt == len);
  ($rose(s1) ##0 (s1, v_cnt += !s2)[*1:$]) intersect s2[->1] |-> (v_cnt == len);
endproperty

Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.

1 Like