SystemVerilog
Assertions (SVA)

module tb;
  logic clk, valid, ready;

  always @(posedge clk) begin
    // Immediate assertion: fires at THIS clock edge
    assert (valid !== 1'bx)
      else $error("valid is X at time %0t", $time);

    // Named assertion — name appears in waveform tool
    chk_no_x: assert (ready !== 1'bx)
      else $fatal("ready driven X — fatal error");
  end
endmodule

// req must be high, then exactly 1 cycle later ack must be high
sequence req_then_ack;
  req ##1 ack;
endsequence

// req high for 4 consecutive cycles
sequence req_burst;
  req [*4];           // req ##0 req ##0 req ##0 req
endsequence

// valid holds while !last, then last goes high within 1..8 cycles
sequence axi_beat;
  (valid && !last)[*1:8] ##1 (valid && last);
endsequence

// Every time req goes high, ack must follow within 1..4 cycles
property p_req_ack;
  @(posedge clk)
  req |-> ##[1:4] ack;
endproperty

// Instantiate as an assertion
A_req_ack: assert property (p_req_ack)
  else $error("req-ack timeout at %0t", $time);

// Cover: track how often the sequence fires
C_req_ack: cover property (p_req_ack);

property p_overlap;
  @(posedge clk)
  req |-> ack;       // when req=1, ack must ALSO be 1 at same edge
endproperty

property p_nonoverlap;
  @(posedge clk)
  req |=> ack;       // when req=1, ack must be 1 the NEXT cycle
endproperty

// AXI: when valid=1 and ready=0, valid must not drop (data stability)
property p_axi_stable;
  @(posedge clk)
  (valid && !ready) |=> valid;
endproperty

A_axi_stable: assert property (p_axi_stable)
  else $error("AXI protocol violation: valid dropped before ready");

// Data must be stable while valid is asserted
property p_data_stable;
  @(posedge clk)
  (valid && !$rose(valid)) |-> $stable(data);
endproperty

// Output must equal input delayed by 2 cycles (pipeline check)
property p_pipeline;
  @(posedge clk)
  disable iff (rst)
  dout === $past(din, 2);
endproperty

A_pipe: assert property (p_pipeline)
  else $error("Pipeline mismatch: dout=%0h, expected=%0h", dout, $past(din,2));

property p_no_double_grant;
  @(posedge clk) disable iff (!rst_n)
  $onehot0(grant);    // at most one grant bit high at a time
endproperty

// Without disable iff, this would fire during reset when grant is X
A_grant: assert property (p_no_double_grant)
  else $fatal("Multiple grants detected!");

// Separate assertion module
module fifo_assertions (
  input clk, rst_n, wr_en, rd_en, full, empty
);
  property p_no_wr_when_full;
    @(posedge clk) disable iff (!rst_n)
    full |-> !wr_en;
  endproperty

  property p_no_rd_when_empty;
    @(posedge clk) disable iff (!rst_n)
    empty |-> !rd_en;
  endproperty

  A_wr_full:  assert property (p_no_wr_when_full)  else $error("Write to full FIFO!");
  A_rd_empty: assert property (p_no_rd_when_empty) else $error("Read from empty FIFO!");
endmodule

// Bind it to the DUT instance — zero DUT code changes
bind sync_fifo fifo_assertions u_chk (
  .clk(clk), .rst_n(rst_n),
  .wr_en(wr_en), .rd_en(rd_en),
  .full(full), .empty(empty)
);

module axis_checker (
  input clk, rst_n,
  input tvalid, tready, tlast,
  input [7:0] tdata
);

  // AXI-Stream Rule 1: once valid asserted, hold until handshake
  property p_valid_stable;
    @(posedge clk) disable iff (!rst_n)
    (tvalid && !tready) |=> tvalid;
  endproperty

  // AXI-Stream Rule 2: data must be stable while valid & !ready
  property p_data_stable;
    @(posedge clk) disable iff (!rst_n)
    (tvalid && !tready) |=> $stable(tdata);
  endproperty

  // AXI-Stream Rule 3: tlast must arrive within 256 beats of burst start
  property p_burst_end;
    @(posedge clk) disable iff (!rst_n)
    $rose(tvalid) |-> ##[1:256] (tvalid && tlast);
  endproperty

  A_valid:  assert property (p_valid_stable)  else $error("TVALID dropped before handshake");
  A_data:   assert property (p_data_stable)   else $error("TDATA changed before handshake");
  A_burst:  assert property (p_burst_end)     else $error("Burst has no TLAST within 256 beats");

  // Coverage: ensure both paths (last, no-last) are exercised
  C_tlast:  cover property (@(posedge clk) tvalid && tready && tlast);
  C_nodata: cover property (@(posedge clk) !tvalid);

endmodule