Verification Academy

Search form

My Account Menu

  • Register
  • Log In
  • Topics
  • Courses
  • Forums
  • Patterns Library
  • Cookbooks
  • Events
  • More
  • All Topics
    The Verification Academy offers users multiple entry points to find the information they need. One of these entry points is through Topic collections. These topics are industry standards that all design and verification engineers should recognize. While we continue to add new topics, users are encourage to further refine collection information to meet their specific interests.
    • Languages & Standards

      • Portable Test and Stimulus
      • Functional Safety
      • Design & Verification Languages
    • Methodologies

      • UVM - Universal Verification Methodology
      • UVM Framework
      • UVM Connect
      • FPGA Verification
      • Coverage
    • Techniques & Tools

      • Verification IP
      • Simulation-Based Techniques
      • Planning, Measurement, and Analysis
      • Formal-Based Techniques
      • Debug
      • Clock-Domain Crossing
      • Acceleration
  • All Courses
    The Verification Academy is organized into a collection of free online courses, focusing on various key aspects of advanced functional verification. Each course consists of multiple sessions—allowing the participant to pick and choose specific topics of interest, as well as revisit any specific topics for future reference. After completing a specific course, the participant should be armed with enough knowledge to then understand the necessary steps required for maturing their own organization’s skills and infrastructure on the specific topic of interest. The Verification Academy will provide you with a unique opportunity to develop an understanding of how to mature your organization’s processes so that you can then reap the benefits that advanced functional verification offers.
    • Universal Verification Methodology (UVM)

      • Advanced UVM
      • Basic UVM
      • Introduction to UVM
      • UVM Connect
      • UVM Debug
      • UVMF - One Bite at a Time
    • Featured Courses

      • Introduction to ISO 26262
      • Introduction to DO-254
      • Clock-Domain Crossing Verification
      • Portable Stimulus Basics
      • Power Aware CDC Verification
      • Power Aware Verification
      • SystemVerilog OOP for UVM Verification
    • Additional Courses

      • Assertion-Based Verification
      • An Introduction to Unit Testing with SVUnit
      • Evolving FPGA Verification Capabilities
      • Metrics in SoC Verification
      • SystemVerilog Testbench Acceleration
      • Testbench Co-Emulation: SystemC & TLM-2.0
      • Verification Planning and Management
      • VHDL-2008 Why It Matters
    • Formal-Based Techniques

      • Formal Assertion-Based Verification
      • Formal-Based Technology: Automatic Formal Solutions
      • Formal Coverage
      • Getting Started with Formal-Based Technology
      • Handling Inconclusive Assertions in Formal Verification
      • Sequential Logic Equivalence Checking
    • Analog/Mixed Signal

      • AMS Design Configuration Schemes
      • Improve AMS Verification Performance
      • Improve AMS Verification Quality
  • All Forum Topics
    The Verification Community is eager to answer your UVM, SystemVerilog and Coverage related questions. We encourage you to take an active role in the Forums by answering and commenting to any questions that you are able to.
    • UVM Forum

      • Active Questions
      • Solutions
      • Replies
      • No Replies
      • Search
      • UVM Forum
    • SystemVerilog Forum

      • Active Questions
      • Solutions
      • Replies
      • No Replies
      • Search
      • SystemVerilog Forum
    • Coverage Forum

      • Active Questions
      • Solutions
      • Replies
      • No Replies
      • Search
      • Coverage Forum
    • Additional Forums

      • Announcements
      • Downloads
      • OVM Forum
  • Patterns Library
    The Verification Academy Patterns Library contains a collection of solutions to many of today's verification problems. The patterns contained in the library span across the entire domain of verification (i.e., from specification to methodology to implementation—and across multiple verification engines such as formal, simulation, and emulation).
    • Implementation Patterns

      • Environment Patterns
      • Stimulus Patterns
      • Analysis Patterns
      • All Implementation Patterns
    • Specification Patterns

      • Occurrence Property Patterns
      • Order Property Patterns
      • All Specification Patterns
    • Pattern Resources

      • Start Here - Patterns Library Overview
      • Whitepaper - Taking Reuse to the Next Level
      • Verification Horizons - The Verification Academy Patterns Library
      • Contribute a Pattern to the Library
  • All Cookbooks
    Find all the methodology you need in this comprehensive and vast collection. The UVM and Coverage Cookbooks contain dozens of informative, executable articles covering all aspects of UVM and Coverage.
    • UVM Cookbook

      • UVM Basics
      • Testbench Architecture
      • DUT-Testbench Connections
      • Configuring a Test Environment
      • Analysis Components & Techniques
      • End Of Test Mechanisms
      • Sequences
      • The UVM Messaging System
      • Other Stimulus Techniques
      • Register Abstraction Layer
      • Testbench Acceleration through Co-Emulation
      • Debug of SV and UVM
      • UVM Connect - SV-SystemC interoperability
      • UVM Versions and Compatibility
      • UVM Cookbook
    • Coding Guidelines & Deployment

      • Code Examples
      • UVM Verification Component
      • Package/Organization
      • Questa/Compiling UVM
      • SystemVerilog Guidelines
      • SystemVerilog Performance Guidelines
      • UVM Guidelines
      • UVM Performance Guidelines
    • Coverage Cookbook

      • Introduction
      • What is Coverage?
      • Kinds of Coverage
      • Specification to Testplan
      • Testplan to Functional Coverage
      • Bus Protocol Coverage
      • Block Level Coverage
      • Datapath Coverage
      • SoC Coverage Example
      • Requirements Writing Guidelines
      • Coverage Cookbook
  • All Events
    No one argues that the challenges of verification are growing exponentially. What is needed to meet these challenges are tools, methodologies and processes that can help you transform your verification environment. These recorded seminars from Verification Academy trainers and users provide examples for adoption of new technologies and how to evolve your verification process.
    • Upcoming & Featured Events

      • U2U MARLUG - January 26th
      • Creating an Optimal Safety Architecture  - February 9th
      • The ABC of Formal Verification - February 11th
      • Events Calendar
    • On Demand Seminars

      • I'm Excited About Formal...
      • Visualizer Coverage
      • Formal-based ‘X’ Verification
      • 2020 Functional Verification Study
      • All On-Demand Seminars
    • Recording Archive

      • Improving Your SystemVerilog & UVM Skills
      • Should I Kill My Formal Run?
      • Visualizer Debug Environment
      • All Recordings
    • Mentor Training Center

      • SystemVerilog for Verification
      • SystemVerilog UVM
      • UVM Framework
      • Instructor-led Training
    • Mentor Learning Center

      • SystemVerilog Fundamentals
      • SystemVerilog UVM
      • Questa Simulation Coverage Acceleration Apps with inFact
      • View all Learning Paths
  • About Verification Academy
    The Verification Academy will provide you with a unique opportunity to develop an understanding of how to mature your organization's processes so that you can then reap the benefits that advanced functional verification offers.
    • Blog & News

      • Verification Horizons Blog
      • Academy News
      • Academy Newsletter
      • Technical Resources
    • Verification Horizons Publication

      • Verification Horizons - November 2020
      • Verification Horizons - July 2020
      • Verification Horizons - March 2020
      • Issue Archive
    • About Us

      • Verification Academy Overview
      • Subject Matter Experts
      • Contact Us
    • Training

      • Questa® & ModelSim®
      • Questa® inFact
      • Functional Verification Library
Ask a Question
SystemVerilog
  • Home /
  • Forums /
  • SystemVerilog /
  • VF Horizons:PAPER: SVA Alternative for Complex Assertions

VF Horizons:PAPER: SVA Alternative for Complex Assertions

SystemVerilog 4879
SVA assertions tasks... 1
ben@SystemVerilog.us
ben@SystemVerilog.us
Full Access
1904 posts
February 28, 2018 at 12:15 pm

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.

Replies

Log In to Reply

Solution

Solution

Tudor Timi
Tudor Timi
Full Access
333 posts
March 01, 2018 at 3:15 am

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.

Constrained random thoughts on SystemVerilog and e: http://blog.verificationgentleman.com/

ben@SystemVerilog.us
ben@SystemVerilog.us
Full Access
1904 posts
March 01, 2018 at 1:35 pm

In reply to Tudor Timi:

Quote:
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());  
  • Quote:
    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    

  • Quote:
    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!

  • Quote:
    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.
  • [*]
    Quote:
    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/
    For training, consulting, services: contact http://cvcblr.com/home
    * SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
    * Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 978-1539769712
    * 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
    * 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
    --------------------------------------------------------------------------
    Tudor Timi
    Tudor Timi
    Full Access
    333 posts
    March 02, 2018 at 2:07 am

    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).

    Constrained random thoughts on SystemVerilog and e: http://blog.verificationgentleman.com/

    ben@SystemVerilog.us
    ben@SystemVerilog.us
    Full Access
    1904 posts
    March 02, 2018 at 11:00 am

    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/
    For training, consulting, services: contact http://cvcblr.com/home
    * SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
    * Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 978-1539769712
    * 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
    * 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
    --------------------------------------------------------------------------
    ben@SystemVerilog.us
    ben@SystemVerilog.us
    Full Access
    1904 posts
    March 03, 2018 at 11:43 pm

    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

    © Mentor, a Siemens Business, All rights reserved www.mentor.com

    Footer Menu

    • Sitemap
    • Terms & Conditions
    • Verification Horizons Blog
    • LinkedIn Group
    SiteLock