// SPDX-License-Identifier: MIT
`timescale 1ns/1ps
module tb;
  bit clk = 0;
  bit reset = 1;
  bit request = 0;
  bit acknowledge = 0;
  bit [7:0] data = 0;
  int mode = 0;
  int active_samples = 0;
  int trigger_count = 0;
  int implication_failures = 0;
  int sampled_failures = 0;
  always #5 clk = ~clk;

  Reply: assert property (@(posedge clk) disable iff (reset)
    request |=> acknowledge)
    else begin
      implication_failures++;
      $display("REPLY_FAIL t=%0t", $time);
    end
  Trigger: cover property (@(posedge clk) !reset && request);
  PreviousData: assert property (@(posedge clk) disable iff (reset)
    acknowledge |-> data == $past(data) + 8'd1)
    else begin
      sampled_failures++;
      $display("SAMPLED_FAIL t=%0t", $time);
    end

  always @(posedge clk) begin
    if (!reset) begin
      active_samples++;
      if (request) trigger_count++;
    end
  end
  task automatic drive(input bit r, input bit a, input bit rst,
                       input bit [7:0] value);
    @(negedge clk);
    request = r;
    acknowledge = a;
    reset = rst;
    data = value;
  endtask
  initial begin
    if (!$value$plusargs("MODE=%d", mode)) mode = 0;
    drive(0, 0, 0, 8'd10);
    if (mode == 2) begin
      drive(0, 0, 0, 8'd11);
      drive(0, 0, 0, 8'd12);
    end else begin
      drive(1, 0, 0, 8'd20);
      if (mode == 3) drive(0, 0, 1, 8'd21);
      else if (mode == 1) drive(0, 0, 0, 8'd21);
      else if (mode == 4) drive(0, 1, 0, 8'd25);
      else drive(0, 1, 0, 8'd21);
    end
    drive(0, 0, 0, 8'd30);
    drive(0, 0, 0, 8'd31);
    @(negedge clk);
    $display("RESULT mode=%0d active=%0d triggers=%0d reply_fail=%0d sampled_fail=%0d",
      mode, active_samples, trigger_count,
      implication_failures, sampled_failures);
    if (mode == 1 && implication_failures != 1) $fatal(1, "Expected reply failure");
    if (mode != 1 && implication_failures != 0) $fatal(1, "Unexpected reply failure");
    if (mode == 4 && sampled_failures != 1) $fatal(1, "Expected sampled failure");
    if (mode != 4 && sampled_failures != 0) $fatal(1, "Unexpected sampled failure");
    if (mode == 2 && trigger_count != 0) $fatal(1, "Expected no trigger");
    if (mode != 2 && trigger_count != 1) $fatal(1, "Expected one trigger");
    $finish;
  end
endmodule