Check signal stable with counter

SystemVerilog
,
1

I’m trying to write the property for the following assertion: after a rising edge of signal A, signal B can change for CNT number of cycles, but then it has to remain stable until the next rising edge of A. Or in other words, B can only change between two rising edges of A within the first cnt cycles after the rising edge. I tried implementing this using the following property. It works, but not for all combinations of toggling signals.
property pr1;
logic [15:0] cntp;
@(posedge clk) (rose(A), cntp = cnt) |-> (1, cntp=cntp-1)[*0:] ##1 (cntp == 0) |-> (stable(B)[*0:] ##1 $rose(A));
endproperty
Essentially, my thought was to use the local variable to count the number of cycles, and then check that the signal is stable.

2

In reply to Branex:

 
// only for: signal B DOES change for CNT CONTINUOUS number of cycles
@(posedge clk) ($rose(B), cntp = cnt) |-> 
first_match((1, cntp=cntp-1'b1)[*0:$] ##1 (cntp == 0)) 
  ##0 $stable(B)[*0:$] ##1 $rose(A);
// NOTE: the |-> is not needed, the first_match is
// could use my package 
/* https://verificationacademy.com/forums/systemverilog/sva-package-dynamic-and-range-delays-and-repeats

http://systemverilog.us/vf/sva_delay_repeat_range.sv
 */

import uvm_pkg::*; `include "uvm_macros.svh" 
import sva_delay_repeat_range_pkg::*;

@(posedge clk) ($rose(B), cntp = cnt) |-> 
 q_dynamic_repeat(D, cntp)
  ##0 $stable(B)[*0:$] ##1 $rose(A);

//... signal B change for CNT number of cycles
// the B's are not necessarily consecutive 
sequence q_d; D[->1]; endsequence 
@(posedge clk) ($rose(B), cntp = cnt) |-> 
 q_dynamic_repeat(q_d, cntp)
  ##0 $stable(B)[*0:$] ##1 $rose(A);

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

  • SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
  • A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
  • Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
  • Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 978-1539769712
  • Component Design by Example ", 2001 ISBN 0-9705394-0-1
  • VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
  • VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115
  1. SVA Alternative for Complex Assertions
    Verification Horizons - March 2018 Issue | Verification Academy
  2. SVA: Package for dynamic and range delays and repeats | Verification Academy
  3. SVA in a UVM Class-based Environment
    SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy
3

In reply to ben@SystemVerilog.us:

Above is an update.

4

Thanks, Ben. My main problem was that with the way I wrote the assertion above, it would fail if the sequence was not satisfied. But if the sequence was fine, assert would never complete, I would never get an OK from assert property and by adding display statements into the sequence, I noticed that the counter would simply continue counting below zero. Then it hit me to change (1, cntp=cntp-1) to (cntp > 0, cntp=cntp-1) and all of a sudden it started working as I expected it. Does that make sense to you?

5

In reply to Branex:
I think that you are talking about

(1, cntp=cntp-1)[*0:$] ##1 (cntp == 0) |-> (stable(B)[*0:] ##1 rose(A)); Here, you have for an antecedent a multi-threaded sequence, and for the assertion to pass, all possible threads must be tested. With the (1, cntp=cntp-1)[*0:] ##1 whatever_sequence, you have a successful attempt at every cycle (because of the (1,…). Thus, without a first_match, the assertion will never succeed since all possible threats must be tested. It can fail though.

With (cntp > 0, cntp=cntp-1)[*0:$] ##1 (cntp == 0) |-> (stable(B)[*0:] ##1 $rose(A));

A sequence of the form (v[*1:$]) is same as
v[*1] or v[*2]…or v[*n] Thus,
If v==0 in any cycle, you break the repeat possible chain of all possible repeats.

Ben systemverilog.us

6

Yes, that’s what I was talking about. Thanks, Ben!