VF Horizons:PAPER: SVA Alternative for Complex Assertions

SystemVerilog
,
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