SVA - Repeat pattern until_with

SystemVerilog
1

How would I write the following assertion?

  • start signal is asserted for one cycle
  • finish signal is asserted for one cycle
  • valid is asserted for 10 cycles and de-asserted for 20 cycles (this pattern repeats when start is asserted and until finish is asserted

Would it look like something below?

($rose(start) |-> ($rose(valid) |-> valid[*:10] -|> $fell(valid) |-> valid[*:20])[*1:$] until finish
2

In reply to DVCoder:
DO not use multiple implication operators; each antecedent can cause vacuity.
See my paper Reflections on Users’ Experiences with SVA, Part II | Verification Horizons - July 2022 | Verification Academy
usage of these four relationship operators: throughout, until, intersect, implies.

Needs more clarity on your requirements.

  • start signal is asserted for one cycle
  • finish signal is asserted for one cycle
  • Following start after 0 to 3 cycles valid is asserted
    and remains active (1) for 10 cycles and de-asserted for 20 cycles
  • (this pattern repeats when start is asserted and until finish is assert/
    (start==1 then 0, … valid==1 for 10 cycles the 0 for 20 cycles…) repeats until the_finish

initial // Only one occurrence of the assertion 
  begin 
 ap: assert property(@ (posedge clk) $rose(start)[->1] |-> 
        ($rose(start) ##[1:3]valid[*10] ##1 !valid[*20])[*1:$])[*1:$] s_until thefinish);  
// Also OK 
ap: assert property(@ (posedge clk) $rose(start)[->1] |-> 
       strong( ($rose(start) ##[1:3]valid[*10] ##1 !valid[*20])[*1:$])[*1:$] intersect 
        thefinish[->1]));  
end

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats | Verification Academy
  2. Free books: * Component Design by Example FREE BOOK: Component Design by Example … A Step-by-Step Process Using VHDL with UART as Vehicle | Verification Academy
  1. Papers:

Udemy courses by Srinivasan Venkataramanan (http://cvcblr.com/home.html)
https://www.udemy.com/course/sva-basic/
https://www.udemy.com/course/sv-pre-uvm/

3

In reply to ben@SystemVerilog.us:

Thanks for the reply. The first valid signal will be asserted when start is asserted. Between start and finish there will be multiple times valid (10 cycles on/20 cycles off) will occur.

Why are there (2) [*1:$] at the end of the first property ?

4

In reply to DVCoder:

The first valid signal will be asserted when start is asserted. Between start and finish there will be multiple times valid (10 cycles on/20 cycles off) will occur.

use ##[0:3] (see below)

Why are there (2) [*1:$] at the end of the first property ?

typo, sorry!


initial // Only one occurrence of the assertion 
  begin 
 ap: assert property(@ (posedge clk) $rose(start)[->1] |-> 
        ($rose(start) ##[0:3]valid[*10] ##1 !valid[*20])[*1:$] s_until thefinish);  
// Also OK 
ap: assert property(@ (posedge clk) $rose(start)[->1] |-> 
       strong( ($rose(start) ##[0:3]valid[*10] ##1 !valid[*20])[*1:$]) intersect 
        thefinish[->1]));  
end