VF Horizons:PAPER: SVA Alternative for Complex Assertions

SystemVerilog
,
1

https://verificationacademy.com/news/verification-horizons-march-2018-issue

Abstract:
Assertion-based verification has been an integral part of modern-day design verification. Concurrent SVA
is a powerful assertion language that expresses the definition of properties in a concise set of notations
and rules; its use is very wide spread and is definitely encouraged. However, SVA is designed for a static
world; it fails to easily address the use of delays and repetitions based on the values of unit variables
(module, checker, interface); it cannot reference non-static class properties or methods; care should
be taken when accessing large data structures, especially large dynamic data structures; sequence_
match_item cannot directly modify unit variables; there are very strict rules on how property local
variables are processed in the ORing and ANDing of sequences, and the flow through of those variables.
It is important to note that those restrictions should not be viewed as a discount of SVA because SVA
easily addresses most common cases of chip design requirements. In addition, the alternative presented
in this article is only applicable for simulation, but definitely not for formal verification, as that is only
supported by assertion languages (SVA, PSL).

This article first explains the concepts, and then by example, how a relatively simple assertion can be
written without SVA with the use of SystemVerilog tasks; this provides the basis for understanding
the concepts of multithreading and exit of threads upon a condition, such as vacuity or an error in the
assertion. The article then provides examples that demonstrate how some of the SVA limitations can
be overcome with the use of tasks, but yet maintain the spirit (but not vendor’s implementations) of SVA.
Another possibility to handle these issues is to use checker libraries such as OVL, Go2UVM2; those
checkers are not addressed in this article. Again, it is important to emphasize that this alternate solution
with tasks should only be used when those difficult situations arise.

2

In reply to ben@SystemVerilog.us:

The main advantage of SVA is that it separates the what (the properties/sequences/etc.) from the how (the SVA engine built into the simulator). What you are advocating is clumping the two together in a big monolithic and not so readable clump. Your two leading examples for delays/repeats based on variables are written in an “inline” style. Also, no idea why you packed the code in properties and not in sequences.

Dynamic delays and repeats can’t be achieved inside the language, that’s true, but their implementation can be encapsulated in a set of helper sequences that take the number of repetitions and the expression/sequence to be repeated:



package cool_sva_utils;

  sequence variable_delay(
      int unsigned min,
      int unsigned max = min);
    // ...
  endsequence

  sequence variable_repetition(
      untyped exp_or_seq,
      int unsigned min,
      int unsigned max) = min;
    // ...
  endsequence

endpackage



import cool_sva_utils::*;

// illegal: assert property($rose(a) ##dly1 b |-> ##dly2 c);
assert property($rose(a) ##0 variable_delay(dly1) ##0 b |-> variable_delay(dly2) ##0 c);

// illegal: assert property($rose(a) |=> b[*1:max] ##1 c)'
assert property($rose(a) |=> variable_repetition(b, 0, max) ##1 c);

I’d rather see the above than a task where the entire assertion is unrolled. One could also define variants that take an infinite max number of repetitions.

Regarding assertions in classes, yes it would be nice to be able to SVA stuff inside objects, but not necessarily checks. Rather, what is more interesting is reusing SVA definitions to generate procedural code for monitors/drivers. The code writer should still specify in SVA, to achieve the nice separation of what and how.

Regarding the last example, a complex assertion, I don’t see why one would need to use ‘or’. Why can’t something like the following work:


property matching_checksum;
  <type> computed_checksum;
  $rose(go) ##0 compute_checksum(vld, data, computed_checksum) |->
      $fell(go) [->1] checksum == computed_checksum;
endproperty


sequence compute_checksum(<type> vld, <type> data, untyped computed_checksum);
  (vld[->1], computed_checksum += data) [*1:$];
endsequence

I must admit I didn’t test it. There might be some tricky cases in there, but at first glance it seems reasonable.

Even if what I wrote there doesn’t work, a little bit of support code in a checker to compute the checksum that always increments on a valid and clears on a $rose(go) is far easier to read than a task that mixes intent with execution.

If you’d have told me that you have a library of building blocks (tasks) that one can compile to emualte an SVA I would be more inclined to use it.

3

In reply to Tudor Timi:

In reply to ben@SystemVerilog.us:
The main advantage of SVA is that it separates the what (the properties/sequences/etc.) from the how (the SVA engine built into the simulator). What you are advocating is clumping the two together in a big monolithic and not so readable clump. Your two leading examples for delays/repeats based on variables are written in an “inline” style. Also, no idea why you packed the code in properties and not in sequences.

Thank you very much for your great comments and suggestions.

  • Background

A quick history of how this paper came about. One of the problems that beginners of SVA have is this concept of threading upon a successful attempt; that is why many beginners forget to use the $rose in an antecedent. I also wanted to better understand and explain the simulation model (though not implementation) of assertions. After some work, it dawned on me to use tasks to represent properties and the fork/join_none as the assertion control.
[*] assertion with tasks: In my examples, I emulated a property as a task, and the assertion control with the fork/join_none. But that control can come from an assertion statement,

ap: assert property($rose(a) |-> (1, task_name());

[*]

Dynamic delays and repeats can’t be achieved inside the language, that’s true, but their implementation can be encapsulated in a set of helper sequences that take the number of repetitions and the expression/sequence to be repeated:

I really like your idea. Below is a model using this approach

   
// ****** ERROR SEE NEXT POST
/*package cool_sva_utils; // ERROR ********************************
    sequence variable_repeat(q_s, count); 
        int v; 
        (1, v=count) ##0 ((q_s, v=v-1'b1) [*0:$] ##1 v==0); 
    endsequence

    sequence variable_delay(count); 
        int v; 
        (1, v=count) ##0 first_match((1, v=v-1'b1) [*0:$] ##1 v<=0); 
    endsequence
endpackage*/ // ERROR, SEE NEXT POST 

import uvm_pkg::*; `include "uvm_macros.svh" 
import cool_sva_utils::*;
module top; 
    timeunit 1ns;     timeprecision 100ps;  
    bit clk, a, b;  
    int r=2; 
    default clocking @(posedge clk); 
    endclocking
    initial forever #10 clk=!clk;  
    
    sequence q1; 
        a ##4 b; 
    endsequence 

    ap_abr: assert property(a |-> variable_repeat(q1, r)); 
    ap_delay:assert property(a |-> variable_delay(r) ##1 b);   

    initial begin 
        repeat(200) begin 
            @(posedge clk);   
            if (!randomize(a, b)  with 
            { a dist {1'b1:=1, 1'b0:=1};
              b dist {1'b1:=1, 1'b0:=1};            
        }) `uvm_error("MYERR", "This is a randomize error")
    end 
    $stop; 
end 
endmodule

[*]

I’d rather see the above than a task where the entire assertion is unrolled. One could also define variants that take an infinite max number of repetitions.

Your idea is good. My paper offers another alternative. It can also be used as a teaching guide to better explain a conceptual (but not implementation) model of an SVA simulation approach. Through this forum, my paper initiated your response, which really is not bad!

[*]

Regarding assertions in classes, yes it would be nice to be able to SVA stuff inside objects, but not necessarily checks. Rather, what is more interesting is reusing SVA definitions to generate procedural code for monitors/drivers. The code writer should still specify in SVA, to achieve the nice separation of what and how.

Monitor/verification classes can make use of the tasks approach for verification or as a tool to tune the stimulus vectors. Anyway, it’s an idea, a tool.
[*]

Regarding the last example, a complex assertion, I don’t see why one would need to use ‘or’.

What I was trying to demonstrate is that SVA has rules on local variable with the ORing of sequences. Those rules can be confusing and challenging. Since tasks can make use of a richer vocabulary of SystemVerilog, they tend to be easier and more readable than SVA. My point was more of issues with SVA’s ORing and Anding, and the use of counts and first_matches.
Again, the purpose of the paper is SVA Alternative for Complex Assertions, it’s an option. Again, one result is your feedback that adds a very interesting alternative. I like it. Would it work in all cases? Most likely not if you start dealing with complex assertions with local variables, passing those variables to sequences, and with threads that include ORing and ANDing of sequences. But your suggestion does cover many common cases. ++4U !

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

4

In reply to ben@SystemVerilog.us:

Put the code for ‘cool_sva_utils’ on GitHub (under some meaningful name) and we’re one step in the direction of an SV(A) standard lib. Not sure if it’s not already covered by OVL already (never used it).

5

In reply to Tudor Timi:
Below is an update that works.
http://SystemVerilog.us/vf/sva_delay_repeat_pkg.sv
http://SystemVerilog.us/vf/sva_delay_repeat.sv


/*     */
   // SEE UPDATE BELOW 
package sva_delay_repeat_pkg; 
    sequence dynamic_repeat(q_s, count); 
        int v=count; 
        (1, v=count) ##0 first_match((q_s, v=v-1'b1) [*1:$] ##0 v<=0);
        // (v>0, v=count) ##0 ((q_s, v=v-1'b1) [*1:$] ##0 v==0); // Incorrect 
    endsequence
    
    sequence dynamic_delay(count); 
        int v; 
        (1, v=count) ##0 first_match((1, v=v-1'b1) [*0:$] ##1 v<=0); 
    endsequence
endpackage 


/*  The repeat value MUST BE > 0   
   
package sva_delay_repeat_pkg; 
    sequence dynamic_repeat(q_s, count); 
        int v=count; 
        (v>0, v=count) ##0 ((q_s, v=v-1'b1) [*1:$] ##0 v==0); 
    endsequence
    
    sequence dynamic_delay(count); 
        int v; 
        (1, v=count) ##0 first_match((1, v=v-1'b1) [*0:$] ##1 v<=0); 
    endsequence
endpackage */

import uvm_pkg::*; `include "uvm_macros.svh" 
import sva_delay_repeat_pkg::*;
module top; 
    timeunit 1ns;     timeprecision 100ps;  
    bit clk, a, b, c=1;  
    int r=2; 
    default clocking @(posedge clk); 
    endclocking
    initial forever #10 clk=!clk;  
    
    sequence q1; 
        a ##1 b; 
    endsequence 

    ap_abr: assert property(a |-> dynamic_repeat(q1, r) ##1 c); 
    ap_abr_fix2: assert property(a |-> q1[*2] ##1 c); 
    ap_abr_fix0: assert property(a |-> q1[*0] ##1 c); 

    ap_delay:assert property(a |-> dynamic_delay(r) ##0 b);  
    ap_delay_fix2:assert property(a |-> ##2 1'b1 ##0 b); 
    ap_delay_fix0:assert property(a |-> ##0 1'b1 ##0 b);   

    property p_or;
        int v; 
        ($rose(a), v=r) |-> (##1 (1,v=v+1'b1) ##1 dynamic_delay(v) ##0 c) or 
                            (dynamic_delay(v) ##0 c);
    endproperty 
    ap_or: assert property(p_or);  


    initial begin 
        repeat(100) begin 
            @(posedge clk); #2;   
            if (!randomize(a, b, c)  with 
            { a dist {1'b1:=1, 1'b0:=1};
              b dist {1'b1:=1, 1'b0:=1}; 
              c dist {1'b1:=1, 1'b0:=1};            
        }) `uvm_error("MYERR", "This is a randomize error")
        end 
        #1 r=0; 
        repeat(100) begin 
            @(posedge clk); #2;   
            if (!randomize(a, b, c)  with 
            { a dist {1'b1:=1, 1'b0:=1};
              b dist {1'b1:=1, 1'b0:=1}; 
              c dist {1'b1:=1, 1'b0:=1};            
        }) `uvm_error("MYERR", "This is a randomize error")
        end 
        $stop; 
    end 
endmodule

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

6

In reply to ben@SystemVerilog.us:

// An Update
http://SystemVerilog.us/vf/sva_delay_repeat_pkg.sv
http://SystemVerilog.us/vf/sva_delay_repeat.sv


package sva_delay_repeat_pkg; 
    sequence dynamic_repeat(q_s, count); 
        int v=count; 
        (1, v=count) ##0  first_match((q_s, v=v-1'b1) [*1:$] ##0 v<=0); 
    endsequence
 
    sequence dynamic_delay(count); 
        int v; 
        (1, v=count) ##0 first_match((1, v=v-1'b1) [*0:$] ##1 v<=0); 
    endsequence
endpackage

Ben systemverilog.us