How to create a Systemverilog assertion for a watchdog timer module

I’m trying to create a systemverilog assertion to check a simple watchdog timer module where the user can input the terminal count, pet the watchdog (to reset the counter), and outputs an expire signal if the count is exceeded.

I’m having some trouble getting the logic right but I was thinking something like this:


// Check expire doesn't occur if pet happens before terminal count
assert property(@(posedge clk) ~expire ##1 pet [*1:terminal_count] |-> ~expire); 

//Check expire occurs if pet doesn't happen sometime before terminal count
assert property(@(posedge clk) ~expire ##1 ~pet [*1:terminal_count] |-> expire);

It also doesn’t seem to let me set a range if the terminal count isn’t fixed, I was hoping to generate it with $urandom_range().

Any help is appreciated!

Thanks,
-mike

In reply to mchen76:

Use my package
https://verificationacademy.com/forums/systemverilog/sva-package-dynamic-and-range-delays-and-repeats

It addresses the use of dynamic delays and repeats.

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

  • SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
  • 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
  • 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
  2. SVA: Package for dynamic and range delays and repeats | Verification Academy
  3. SVA in a UVM Class-based Environment
    SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy

In reply to ben@SystemVerilog.us:

Ben, thanks for the response. I tried doing this:


sequence q_dynamic_delay(count);
  int v;
  (1, v=count) ##0 first_match((1, v=v-1'b1) [*0:$] ##1 v<=0);
endsequence 

// Checks that expire occurs without any expire occurring before delay or that pet occurs sometime between that period
assert property (@(posedge clk) $fall(pet)  |-> 
                                (1 [*0:$] ##0 pet) or 
                                (~expire throughout q_dynamic_delay(terminal_count) ##1 expire)) else $error("WDT failure");

But I can’t seem to get it to fail when the dynamic delay value is purposefully set lower which leads me to think maybe one of the sequences are evaluating to true all the time. I also wonder if vivado reacts properly to this sequence definition, I put something like


assert property (@(posedge clk) 1 |=> 0) else $error("Checking error works");

after the sequence definition and it wouldn’t give any errors unless it was pasted before the sequence def. Very odd.

Thanks!,
-mike

In reply to mchen76:
If I uderstand the design, you have a “keep_alive” (or refresh) signal and a timer count that gets reset at every occurrence of keep_alive.
You call the keep_alive signal “pet” Thus upon a $fell(pet) you expect pet==1 within that count period (teminal_count value)
The way I see it, your assertion has an accept_on($rose(pet, @(posedge clk), which is the refresh or keep_alive signal On an accept_on the assertion is vacuous

For a failure, you expect a keep_alive within that timeout cout, or
*keep_alive within (1, v=count) ##0 first_match((1, v=v-1’b1) [0:$] ##1 v<=0);
Thus, your main assertion looks like

// Checks that expire occurs before delay or that pet occurs sometime between that period

    sequence q_dynamic_delay_or_keep_alive(count, keep_alive);
        int v;
        keep_alive within (1, v=count) ##0 first_match((1, v=v-1'b1) [*0:$] ##1 v<=0);
    endsequence 
    // SEE EDIT in next post 
    ap_accept_OK: assert property (accept_on($rose(pet, @(posedge clk) )) @(posedge clk) $fell(pet)  |-> 
     //  ****************** USE "pet" instead of "expire"  ************
    (q_dynamic_delay_or_keep_alive(terminal_count, expire))) else $error("WDT failure");

This is my testbench


import uvm_pkg::*; `include "uvm_macros.svh" 
module top; 
    timeunit 1ns;     timeprecision 100ps;    
    bit clk, a, b, pet, expire;  
    bit[3:0] terminal_count=3;
    default clocking @(posedge clk); 
    endclocking
    initial forever #10 clk=!clk;  
    
    sequence q_dynamic_delay(count);
        int v;
        (1, v=count) ##0 first_match((1, v=v-1'b1) [*0:$] ##1 v<=0);
      endsequence 

    sequence q_dynamic_delay_or_keep_alive(count, keep_alive);
        int v;
        keep_alive within (1, v=count) ##0 first_match((1, v=v-1'b1) [*0:$] ##1 v<=0);
    endsequence 
    
    // Checks that expire occurs without any expire occurring before delay or that pet occurs sometime between that period
    // ************* DO NOT USE ************* xxxxxxxxxxxxxxxx
    ap_pet_tc_BAD: assert property (@(posedge clk) $fell(pet)  |-> // BAD ASSERTION 
    (1 [*0:$] ##0 pet) or 
    (!expire throughout q_dynamic_delay(terminal_count) ##1 expire)) else $error("WDT failure");

    // *************** OK Assertion ******************
    // Checks that expire occurs before delay or that pet occurs sometime between that period
    ap_accept_OK: assert property (accept_on($rose(pet, @(posedge clk) )) @(posedge clk) $fell(pet)  |-> 
     // (1 [*0:$] ##0 pet) or 
    (q_dynamic_delay_or_keep_alive(terminal_count, expire))) else $error("WDT failure");

    /*But I can't seem to get it to fail when the dynamic delay value is purposefully set lower 
    which leads me to think maybe one of the sequences are evaluating to true all the time.
    I also wonder if vivado reacts properly to this sequence definition, I put something like
    
    assert property (@(posedge clk) 1 |=> 0) else $error("Checking error works");
    after the sequence definition and it wouldn't give any errors unless it was pasted before the sequence def. Very odd.*/ 
    
    initial begin 
        bit vpet, vexpire; 
        repeat(200) begin 
            @(posedge clk);   
            if (!randomize(vpet, vexpire)  with 
            { vpet dist {1'b1:=1, 1'b0:=7};
             vexpire dist {1'b1:=1, 1'b0:=5};      
        }) `uvm_error("MYERR", "This is a randomize error")
        #2;
        pet <= vpet; 
        expire <= vexpire;
    end 
    $stop; 
end 

endmodule    

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


  1. SVA Alternative for Complex Assertions
    https://verificationacademy.com/news/verification-horizons-march-2018-issue
  2. SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy
  3. SVA in a UVM Class-based Environment
    https://verificationacademy.com/verification-horizons/february-2013-volume-9-issue-1/SVA-in-a-UVM-Class-based-Environment

In reply to ben@SystemVerilog.us:

I believe that I used the wrong variable, though the concept is correct
I used expire, but I meant pet because you expect the keep_alive to be within a time period.
The expire is not used.
WHATCH THE Variabls being used :)


    sequence q_dynamic_delay_or_keep_alive(count, keep_alive);
        int v;
        keep_alive within (1, v=count) ##0 first_match((1, v=v-1'b1) [*0:$] ##1 v<=0);
    endsequence 
 
    ap_accept_OK: assert property (accept_on($rose(pet, @(posedge clk) )) @(posedge clk) $fell(pet)  |-> 
     // (1 [*0:$] ##0 pet) or 
    // (q_dynamic_delay_or_keep_alive(terminal_count, expire))) else $error("WDT failure"); 
       (q_dynamic_delay_or_keep_alive(terminal_count, pet))) else $error("WDT failure"); 

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


  1. SVA Alternative for Complex Assertions
    Verification Horizons - March 2018 Issue | Verification Academy
  2. SVA: Package for dynamic and range delays and repeats | Verification Academy
  3. SVA in a UVM Class-based Environment
    SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy