# Assertion protocol checker

**URL:** <https://verificationacademy.com/forums/t/assertion-protocol-checker/36192>\
**Category:** SystemVerilog\
**Tags:** SystemVerilog\
**Created:** [June 17, 2019, 7:39pm UTC](https://verificationacademy.com/forums/t/assertion-protocol-checker/36192 "2019-06-17T19:39:30Z")\
**Posts on this page:** 1\
**Showing post:** 2

<div class="post-metadata">

**Author:** ![user49](https://verificationacademy.com/forums/user_avatar/verificationacademy.com/user49/32/1084_2.png) [@user49](https://verificationacademy.com/forums/u/user49)\
**Post date:** [June 18, 2019, 12:30am UTC](https://verificationacademy.com/forums/t/assertion-protocol-checker/36192/2 "2019-06-18T00:30:58Z")

</div>

_In reply to [Rocketfingers](https://verificationacademy.com/forums/t/assertion-protocol-checker/36192):_  
You need a supporting logic for the never cases that you identified.  
I added the “started” flag that gets set when started, and reset when stop or done (_end is a reserved word)_. For the never sequences, here is an example

```verilog
ap_start_start: assert property(not(start ##1 (start && started[->1])) );

```

That states that there should never be sequence start followed by an occurrence of start and the started flag. Come to think of it, could that be replaced with just:

```verilog
ap_start_start: assert property(not( (start && started)) );

```

Below is my code with a testbench

```verilog

/* I want assertions that check
1 - every start ( // 1 cycle)is followed by an end or a stop (start to start back to back cannot occur)
2 - every stop ( // 1 cycle ) or end (done // 1 cycle)is followed by a start ( no back to back stops or ends)

So valid sequences are
Start stop start
Start end start

Examples of invalid sequences are
Start start
Start end end
Start stop stop
Start stop end */
import uvm_pkg::*; `include "uvm_macros.svh" 
module top; 
    timeunit 1ns; timeprecision 100ps;    
    bit clk,start, stop, done, started; 
    default clocking @(posedge clk); 
    endclocking
    initial forever #10 clk=!clk;  
    
    function void set_started(bit a); 
        started = a; 
    endfunction : set_started   
    // 1 - every start is followed by an end or a stop (start to start back to back cannot occur)
    ap_start_stopr_or_done: assert property( 
      (start, set_started(1)) |=> stop[->1] or done[->1]) 
      set_started(0); else set_started(0);  
    
    // every stop ( // 1 cycle ) or end (done // 1 cycle)is followed by a start ( no back to back stops or ends)
    ap_stop_done_to_start: assert property((stop || done) |=> start[->1] );
    
    //Start .. start with NO done or stop, i.e, when in the started state
    
    ap_start_start: assert property(not(start ##1 (start && started[->1])) );  
    // Start end end
    ap_start_end_end: assert property(not(done && started==1'b0));  
    
    // Start stop stop
    ap_start_stop_stop: assert property(not(stop && started==1'b0));  
    
    // Start stop end 
    ap_start_stop_end: assert property(not(done && started==1'b0) );  
       
    initial begin 
        bit va, vb, vc; 
        repeat(200) begin 
            @(posedge clk);   
            if (!randomize(va, vb, vc) with 
            { va dist {1'b1:=1, 1'b0:=3};
            vb dist {1'b1:=1, 1'b0:=2};   
            vc dist {1'b1:=1, 1'b0:=2};      
        }) `uvm_error("MYERR", "This is a randomize error")
        start <= va; 
        stop <= vb;
        done <= vc;
    end 
    $stop; 
end 
endmodule   
 

```

Ben Cohen  
[http://www.systemverilog.us/](http://www.systemverilog.us/) [ben@systemverilog.us](mailto:ben@systemverilog.us)  
For training, consulting, services: contact [Home - My cvcblr](http://cvcblr.com/home)

- [SVA Handbook 4th Edition, 2016 ISBN 978-1518681448](http://goo.gl/JOfuEB)
- 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
- [Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 978-1539769712](https://goo.gl/d10QHh)
- 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

* * *

1. SVA Alternative for Complex Assertions  
[Verification Horizons - March 2018 Issue | Verification Academy](https://verificationacademy.com/news/verification-horizons-march-2018-issue)
2. [SVA: Package for dynamic and range delays and repeats | Verification Academy](https://verificationacademy.com/forums/systemverilog/sva-package-dynamic-and-range-delays-and-repeats)
3. SVA in a UVM Class-based Environment  
[SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy](https://verificationacademy.com/verification-horizons/february-2013-volume-9-issue-1/SVA-in-a-UVM-Class-based-Environment)

---

_[View the full topic](https://verificationacademy.com/forums/t/assertion-protocol-checker/36192)._