Assertion to check a signal is stable between two pulses

SystemVerilog
1

Hi
I need to write an assertion to check if a signal is stable between a pulse A and pulse B
The signal will be asserted @ A and will deassert @B and it should stay stable inbetween.

Thanks,
Anjali

2

In reply to Anjali:


@(posedge clk) $rose(A) |=> $stable(sig)[*1:$] intersect $rose(B)[->1];
// this assumes no deassert @B

@(posedge clk) $rose(A) |=> $stable(sig)[*1:$] ##1 !$stable(sig) intersect $rose(B)[->1];
// with dessert @ B

// depending on the requirements 
@(posedge clk) $rose(A) |=> $stable(sig)[*1:$] ##1 !sig intersect $rose(B)[->1];
// with dessert @ B where sig==0

Ben systemverilog.us

3

In reply to ben@SystemVerilog.us:

Hi Ben,

I have tried the code in my context as below:
property check_env;
@(posedge clk) ($rose(A) |=> (stable(sig))[1*:] ##1 !(B) intersect $rose(B)[->1];
endproperty
assert property(check_env)
$display(“Assertion pass”);
else
$display(“Assertion fail”);

But I am getting errors as below:
Expected specification terminator “;”
This error is seen after ($stable(sig))

Thanks,
Anjali

4

In reply to Anjali:
There was a syntax error. Also,
stable(sig)[*1:] ##1 !(B)) should be
stable(sig)[*1:] ##1 !(sig))


// compiles OK
property check_env;
       @(posedge clk) $rose(A) |=> ($stable(sig)[*1:$] ##1 !(sig)) 
            intersect $rose(B)[->1];
    endproperty
    ap_1: assert property(check_env) $display("Assertion pass");
     else $display("Assertion fail");

// here is my testbench, I get fails and passes

 
import uvm_pkg::*; `include "uvm_macros.svh" 
module top; 
	bit clk, a, A, B, sig;  
	default clocking @(posedge clk); endclocking
	initial forever #10 clk=!clk;  
    property check_env;
       @(posedge clk) $rose(A) |=> ($stable(sig)[*1:$] ##1 !(sig)) 
            intersect $rose(B)[->1];
    endproperty
    ap_1: assert property(check_env) $display("Assertion pass");
     else $display("Assertion fail");


 initial begin 
     repeat(1200) begin 
       @(posedge clk); #1;   
       if (!randomize(A, B, sig)  with 
           { A dist {1'b1:=1, 1'b0:=3};
             B dist {1'b1:=1, 1'b0:=4};
             sig dist {1'b1:=4, 1'b0:=1};
           }) `uvm_error("MYERR", "This is a randomize error")
       end 
       $finish; 
    end 
endmodule  
// BTW, no need to declare a property if it is a single use and no variables. 
// Just write the assert statement

[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
5

In reply to ben@SystemVerilog.us:

HI Ben,
Thanks a lot for your quick replies.
In my case the signal A and B is a pulse of 1 clk cycle and sig rises 1clk after A rises and falls at the rising of signal B.
But by using the above assertion, I get assertion failure.

Thanks,
Anjali

6

In reply to Anjali:

HI Ben,
Thanks a lot for your quick replies.
In my case the signal A and B is a pulse of 1 clk cycle and sig rises 1clk after A rises and falls at the rising of signal B. There is random clks between pulse A and pulse B.
But by using the above assertion, I get assertion failure.

Thanks,
Anjali

7

In reply to Anjali:

Hi Ben,
I have tried the following:
@(posedge clkx) $rose(A) |=> $rose(sig) ##1 (stable(sig)[*1:] ##100 !(B)) intersect $rose(B)[->1];
With that, I am not getting the assertion failure when A pulses, but I get it @ negedge of B

As per my requirements, sig rises @ negedge of A and falls @ posedge of B. Both A and B are pulses. The number of clks between A and B are random.
Thanks,
Anjali

8

In reply to Anjali:

All signals are sampled. The following assertion

 @(posedge clk) $rose(A) |=> ($stable(sig)[*1:$] ##1 !(sig)) 
            intersect $rose(B)[->1];

One cycle after rose of A, a set of the sequence sig stable for ‘n’ clocks followed by!sig occurs during a period oc cycles with!Bs followed by a B. Thus,

 
A.   0 0 1 //assertion successfully attempted 
SIG. - - 1 1 1 1 0.// one possible sequence 
sig. - - 0 0 0 0 0 // another possible sequence 
B.   - - - 0 0 0 1
// this set satisfies the assertion

Ben systemverilog.us

9

In reply to ben@SystemVerilog.us:

 // a variation in property declaration 
 bit v;
 @(posedge clk) $rose(A) |=>  ((1, v=sig) ##0 (v==sig)[*1:$] ##1 !sig) 
            intersect $rose(B)[->1];

One cycle after rose of A, a set of the sequence sig stable for 'n' clocks thereafter  followed by!sig occurs during a period oc cycles with!Bs followed by a B. Thus, 
 
A.   0 0 1 - //assertion successfully attempted 
SIG. - - - 1 1 1 0.// one possible sequence 
sig. - - - 0 0 0 0 // another possible sequence 
B.   - - - 0 0 0 1
// this set satisfies the assertion
10

In reply to ben@SystemVerilog.us:

Hi Ben,
Thanks a lot.
It works great for me.
Thanks,
Anjali