Assertion to calculate and verify time difference between 2 states

[PavanSP]

Hello,
I have a scenario in which i have to verify the time taken to change a state from one value to another, say there is a 3 bit variable and i want to verify whether the time taken to change from 3’h0 to 3’h1 or 3’h0 to 3’h2 similarly any change of that variable is equal to a specific time. How to do that?
I tried by doing the following:

property calc_rate (int rate);
		realtime current_time;
		disable iff(a)
		$changed(state) |-> ('1, current_time = $realtime) |-> $past($changed(state), 1) |-> (rate == ($realtime - current_time)*1000 );
		endproperty: calc_rate

		assert_rate:
			assert property ( @(posedge CLK) calc_rate(Rate))
				`uvm_info("ASSERT", "equal", UVM_HIGH)
			else `uvm_error("ASSERT", "not equal")

This approach is not working, Can you please suggest me to do the other way?

[ben2]

In reply to PavanSP:
A generic comment: You have way too many implication operators; use those wisely.
The following model and testbench works.

import uvm_pkg::*; `include "uvm_macros.svh" 
typedef enum {ST0, ST1, ST2} state_e;
module top; 
    timeunit 1ns;     timeprecision 100ps;    
    bit clk, a, b; 
    state_e state; 
    realtime expected_time=60ns; 
    default clocking @(posedge clk); 
    endclocking
    initial forever #10 clk=!clk;  
    
    property calc_rate (state_e sta, stb, int rate);
        realtime current_time;
        disable iff(a)
        ($changed(state) && state==sta, current_time = $realtime) |-> 
         first_match(##[1:$] state==stb) ##0 ($realtime - current_time) == rate;
    endproperty: calc_rate
    
    assert_rate: assert property ( @(posedge clk) calc_rate(ST1, ST2, expected_time))
    `uvm_info("ASSERT", "equal", UVM_HIGH)
    else `uvm_error("ASSERT", "not equal")
    
    initial begin 
        bit va, vb; 
        state_e v_st;
        repeat(200) begin 
            @(posedge clk);   
            if (!randomize(va, v_st)  with 
            { va dist {1'b1:=0, 1'b0:=3};
              v_st dist {ST0:=1, ST1:=2, ST2 :=1};      
        }) `uvm_error("MYERR", "This is a randomize error")
        a <= va; 
        state <= v_st;
    end 
    $stop; 
end 
endmodule   
....
# UVM_ERROR .\time_state.sv(21) @ 5900: reporter [ASSERT] not equal
# UVM_ERROR .\time_state.sv(21) @ 7700: reporter [ASSERT] not equal
# UVM_ERROR .\time_state.sv(21) @ 7700: reporter [ASSERT] not equal
# UVM_INFO .\time_state.sv(20) @ 8500: reporter [ASSERT] equal
# UVM_ERROR .\time_state.sv(21) @ 9300: reporter [ASSERT] not equal
# UVM_INFO .\time_state.sv(20) @ 10500: reporter [ASSERT] equal
# UVM_ERROR .\time_state.sv(21) @ 12100: reporter [ASSERT] not equal
# UVM_ERROR .\time_state.sv(21) @ 13700: reporter [ASSERT] not equal
 

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

[PavanSP]

In reply to ben@SystemVerilog.us:

Thanks Ben, It is working!!

[nnd]

In reply to ben@SystemVerilog.us:

Hi Ben,

property calc_rate (state_e sta, stb, int rate);
        realtime current_time;
        disable iff(a)
        ($changed(state) && state==sta, current_time = $realtime) |-> 
         first_match(##[1:$] state==stb) ##0 ($realtime - current_time) == rate;
endproperty: calc_rate

In the above property instead of keeping track of specific states, will the property work if we use $changed in the first_match of the consequent statement?

[ben2]

In reply to nnd:

Yes. ($changed(state) is a legal expression