SVA Assertion for down Counter

SystemVerilog
1

HI All,

I have written below assertion but its not working for failing condition.

My expectation:

  1. Wait for posedge of A.
  2. Set default Count valuto 5.
  3. Decrement counter by value 1.
  4. Check value of Signal B once counter is set to 0. If counter is set to 0 and B is not equal to 1 then fire error.

Code ::

module range_in_time_constant();
logic clk, a, b ;

default clocking @(posedge clk); endclocking

initial
begin
$vcdpluson();
clk = 0;
forever #1 clk ++;
end

initial
begin
a <= 0;
b <= 0;

##10;
 a <= 1;
##10;
 b <= 1;

##20;
 a <= 0;
##5;
 b <= 0;

##20;
 a <= 1;
##5;
 b <= 1;

##1
 a <= 0;
 b <= 0;
##200 $finish;

end

//assign #5 b = a;

property p_delay_equivalent(v);
integer local_v;
bit true;
@(posedge clk) disable iff(0)
$rose(a) |-> @(negedge clk) (1, local_v = v) ##0 (1, local_v=local_v - 1,$display(time, "local_v %0d",local_v))[*1:] ##1 (local_v==0) ##0 (b == 1);
endproperty

a2_delay_equivalent: assert property(p_delay_equivalent(5))
else $display(“FAILED”);
endmodule : range_in_time_constant

Result : Code is working fine for passing condition. But its not working for failing condition.

Log ::
local_v 4
local_v 3
local_v 2
local_v 1
local_v 0
local_v -1
local_v -2
local_v -3
local_v -4
local_v -5
local_v -6
local_v -7
local_v -8
local_v -9

I don’t understand why counter is going into the negative count. I am assuming if counter reached to 0 it should check the value of signal B and assertion should fail but it’s going into the Vacuous state.

2

In reply to pvpatel:

why don’t you use code tags to make your code more readable.

3

Following property will work fine for your u:

property p_delay_equivalent(v);
   integer local_v;
   @(posedge clk)
   //($rose(a), local_v=v) |-> strong((1, local_v=local_v-1, $display($time, "local_v %0d",local_v)) [*1:$] ##1  (local_v==0) && b);
   ($rose(a), local_v=v) |-> first_match((1, local_v=local_v-1, $display($time, "local_v %0d",local_v)) [*1:$] ##1 (local_v==0)) ##0 b;
endproperty

You can use either sequence depending on your tool support, I am not sure if strong is supported by all tool vendors as of now.

Regards,
Rohit