System Verilog Assertion to check if no more than 3 ACK are generated in a 10 cycle window

The above problem statement gives us 2 conditions.

1. Window of check should be 10 cycles
2. Number of ACK should be no more than 3.

Since the both end at the same time we will use INTERSECT operator.

Assertion :

  property check_ack;
    @(posedge clk) ack[->3] intersect 1[*10];
  endproperty

ack[->3] or ack[=3] satisfies point 2.

Since we need to check it in 10 cycles (i.e., 10 posedge clk's) we used 1[*10] --> 10 consecutive clock edges.

Code :

// Generate whatever pattern you want in the test class

class test;
   rand bit ack_b;
endclass: test

module top;
  test t;
 
  bit clk;
  bit ack;
 
  initial begin
    $timeformat(-9,0,"ns",8);
    clk <= 0;
    forever #5 clk = !clk;
   
  end
 
  initial begin
    t = new;
    repeat(20) begin //{
      @(posedge clk);
      void'(t.randomize());

      ack = t.ack_b;  
    end //}
    $finish;
  end
 
  property check_ack;
    @(posedge clk) ack[->3] intersect 1[*10];
  endproperty
 

  abc: assert property (check_ack) $display("@%0t ACK is through",$time); else
      $error("Check failed at %0t",$time);

 
  initial
    begin //{
    forever begin //{
      @(posedge clk);
      $display("Time:%0t ACK:%0d",$time,ack);
    end //}
    end //}
endmodule: top

Result :

# //
# Loading sv_std.std
# Loading work.testbench_sv_unit(fast)
# Loading work.top(fast)
#
# vsim -voptargs=+acc=npr
# run -all
# Time:5ns ACK:0
# Time:15ns ACK:1
# Time:25ns ACK:1
# Time:35ns ACK:0
# Time:45ns ACK:1
# Time:55ns ACK:0
# ** Error: Check failed at 55ns
# Time: 55 ns Started: 25 ns Scope: top.abc File: testbench.sv Line: 54
# ** Error: Check failed at 55ns
# Time: 55 ns Started: 15 ns Scope: top.abc File: testbench.sv Line: 54
# ** Error: Check failed at 55ns
# Time: 55 ns Started: 5 ns Scope: top.abc File: testbench.sv Line: 54
# Time:65ns ACK:1
# Time:75ns ACK:1
# ** Error: Check failed at 75ns
# Time: 75 ns Started: 35 ns Scope: top.abc File: testbench.sv Line: 54
# Time:85ns ACK:0
# ** Error: Check failed at 85ns
# Time: 85 ns Started: 55 ns Scope: top.abc File: testbench.sv Line: 54
# ** Error: Check failed at 85ns
# Time: 85 ns Started: 45 ns Scope: top.abc File: testbench.sv Line: 54
# Time:95ns ACK:0
# Time:105ns ACK:1
# Time:115ns ACK:0
# ** Error: Check failed at 115ns
# Time: 115 ns Started: 75 ns Scope: top.abc File: testbench.sv Line: 54
# ** Error: Check failed at 115ns
# Time: 115 ns Started: 65 ns Scope: top.abc File: testbench.sv Line: 54
# Time:125ns ACK:1
# Time:135ns ACK:0
# ** Error: Check failed at 135ns
# Time: 135 ns Started: 85 ns Scope: top.abc File: testbench.sv Line: 54
# Time:145ns ACK:0
# Time:155ns ACK:0
# Time:165ns ACK:0
# Time:175ns ACK:0
# Time:185ns ACK:0
# ** Error: Check failed at 185ns
# Time: 185 ns Started: 95 ns Scope: top.abc File: testbench.sv Line: 54
# ** Note: $finish : testbench.sv(45)
# Time: 195 ns Iteration: 1 Instance: /top
# End time: 11:23:36 on Jul 20,2020, Elapsed time: 0:00:00
# Errors: 20, Warnings: 1