SVA: seq_a should not happen before seq b

SystemVerilog
,
1

Hi there,

what’s the best way to write assertions for following:

once seq_a is triggered, before seq_c triggered, seq_b should not happen. suppose seq_a, seq_b, and seq_c are all defined already.

Thanks,
Jeff

2

In reply to Jeff_Li_90:
I see 3 possible interpretations of this requirement:
// once seq_a is triggered, before seq_c triggered, seq_b should not happen.

  1. INTERPRETATION 2 OF REQUIREMENTS

// If seq_a starts and completes, then
//    * that same start time (e.g., the $rose(a))
//      the completion seq_b (i.e., its endpoint) followed by seq_c should not occur
/* seq_a                    |======>
seq_b                       <=====> // ERROR: seq_b before seq_c
seq_b.triggered      ^   |........^
seq_c                              <======>    */
  1. // INTERPRETATION 2 OF REQUIREMENTS
    // If seq_a starts and completes, then
//    * that same start time (e.g., the $rose(a))
//      the completion seq_b (i.e., its endpoint)
//           should not be inside the completon of seq_c
//      Note: seq_b and seq_c can start at any time
/* seq_a                    |======>
seq_b                       <=====> // ERROR: seq_b before seq_c
seq_b.triggered      ^   |........^
seq_c                          <======>
seq_c.triggered          |............^            */
  1. Interpretation 3
    // After seq_a then seq_b should be followed by seq_c

Below is my code.
I see interpretation 2 as the best intent.
Code also at http://systemverilog.us/vf/seqinnoseq.sv
Wave http://systemverilog.us/vf/m2_wave.png
Thread viewer http://systemverilog.us/vf/Seqm2.png


module top;
    timeunit 1ns;  timeprecision 100ps;    
    `include "uvm_macros.svh"   import uvm_pkg::*;
    bit clk, a, b, c, d, e, f, reset_n;     
    initial forever #10 clk = !clk;
     
    // once seq_a is triggered, before seq_c triggered, seq_b should not happen.
    // suppose seq_a, seq_b, and seq_c are all defined already.
    sequence seq_a; @(posedge clk) $rose(a) ##1 b; endsequence 
    sequence seq_b; @(posedge clk) $rose(a) ##1 c[->1] ##[1:3] d; endsequence 
    sequence seq_c; @(posedge clk) $rose(a) ##1 e[->1] ##[1:2] f; endsequence 
    // NOTE: The $rose(a) ##1 var[->1] is needed to avoid uneeded endpoints 
    //       that are used in the assertions. 
    // INTERPRETATION 1 OF REQUIREMENTS
    // If seq_a starts and completes, then 
    //    * that same start time (e.g., the $rose(a))
    //      the completion seq_b (i.e., its endpoint) followed by seq_c should not occur   
    /* seq_a                    |======> 
       seq_b                       <=====> // ERROR: seq_b before seq_c 
       seq_b.triggered      ^   |........^   
       seq_c                              <======>    */
    ap_a_no_bc_m: assert property(@(posedge clk) 
    seq_a implies  not(##1 seq_b.triggered[->1] ##1 seq_c));  

    // INTERPRETATION 2 OF REQUIREMENTS
    // If seq_a starts and completes, then 
    //    * that same start time (e.g., the $rose(a))
    //      the completion seq_b (i.e., its endpoint) 
    //           should not be inside the completon of seq_c   
    //      Note: seq_b and seq_c can start at any time  
    /* seq_a                    |======> 
       seq_b                       <=====> // ERROR: seq_b before seq_c 
       seq_b.triggered      ^   |........^            
       seq_c                          <======>    
       seq_c.triggered          |............^            */
    ap_a_no_bc_m2: assert property(@(posedge clk) 
         seq_a implies  not(##1 seq_b.triggered[->1] within seq_c.triggered[->1]));  

    // After seq_a then seq_b should be followed by seq_c 
    ap_a_no_bc: assert property(@(posedge clk) 
       seq_a |->  not(seq_b ##0 seq_c));  
  
    initial begin 
      repeat (200) begin
        @(posedge clk);
        if (!randomize(a, b, c, d, e, f)with {
            a  dist {1'b1 := 1, 1'b0 := 3};}) `uvm_error("MYERR", "This is a randomize error"); 
      end
      $finish;
    end
  endmodule

1860×823 168 KB

1865×823 137 KB

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 - SystemVerilog - Verification Academy
  2. Free books: Component Design by Example https://rb.gy/9tcbhl
    Real Chip Design and Verification Using Verilog and VHDL($3) https://rb.gy/cwy7nb
  3. 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:

Hi Ben,

Thank you as always for the solution!

Thanks,
Jeff

4

In reply to Jeff_Li_90:

You’re welcome :)
BTW, the following suggestion was made to me.


 ap_new: assert property(@ (posedge clk)  
       seq_a |-> (!seq_b.triggered throughout seq_c.triggered[->1]));

Possible issue: seq_a attempt at **rose(a)**can occur in the same cycle as seq_b.triggered. A requirement?
Use of the implies: My colleague is always searching for efficiency. In his opinion,
he prefers to stay away from using implies because it is more expensive than using |-> or |=> or just negation. Thus, instead of:

seq_a implies  not(##1 seq_b.triggered[->1] within seq_c.triggered[->1]));
// USE 
not( (seq_a and ##1 seq_b.triggered[->1] ) within seq_c.triggered[->1]));

Anyway, some tidbits to consider.
Ben SystemVerilog.us