// FILE         : fifo_async_sva.sv
// LICENSE      : Personal/academic use only. Commercial use requires a Commercial License.
// SOURCE       : FPV properties for fifo_async.sv
// DATE         : 2026-06-16
// BIND TARGET  : fifo_async
// CLOCK DOMAIN : Dual-clock
//                write assertions: @(posedge wclk) disable iff (!wrst_n)
//                read  assertions: @(posedge rclk) disable iff (!rrst_n)
// RAG RULES    : INC-3 (no |=>), UR-5 (cp_hit per mp_), NAMING ap_/mp_/cp_,
//                EXCEPTION 7b documented, LIVELOCK s_eventually fairness
//-----------------------------------------------------------------------------
// PORT-INTENT TABLE
// ┌────────────────────────┬────────┬────────┬─────────────┬──────────────┐
// │ Signal                 │ Dir    │ Domain │ Intention   │ Activity     │
// ├────────────────────────┼────────┼────────┼─────────────┼──────────────┤
// │ wclk                   │ input  │ write  │ assume      │ clock        │
// │ wrst_n                 │ input  │ write  │ assume      │ reset        │
// │ wen_n                  │ input  │ write  │ assume      │ trigger      │
// │ wdata[WIDTH_G-1:0]     │ input  │ write  │ assume      │ trigger      │
// │ rclk                   │ input  │ read   │ assume      │ clock        │
// │ rrst_n                 │ input  │ read   │ assume      │ reset        │
// │ ren_n                  │ input  │ read   │ assume      │ trigger      │
// │ wfull                  │ output │ write  │ obligation  │ response     │
// │ rempty                 │ output │ read   │ obligation  │ response     │
// │ rdata[WIDTH_G-1:0]     │ output │ read   │ obligation  │ response     │
// │ waddr_wrside[PTR_W-1:0]│ intern │ write  │ obligation  │ structural   │
// │ raddr_rdside[PTR_W-1:0]│ intern │ read   │ obligation  │ structural   │
// │ wrbincount_wrside      │ intern │ write  │ obligation  │ structural   │
// │ rdbincount_rdside      │ intern │ read   │ obligation  │ structural   │
// └────────────────────────┴────────┴────────┴─────────────┴──────────────┘
//
// EXCEPTION 7b:
//   wfull and rempty are obligation outputs used as pure state guards in
//   ap_no_write_when_full and ap_no_read_when_empty antecedents.
//   Not used as environment constraints. Y confirmed.
//-----------------------------------------------------------------------------

`default_nettype none

module fifo_async_sva #(
    parameter int unsigned WIDTH_G  = 8,
    parameter int unsigned DEPTHEXP = 2
)(
    input logic                 wclk,
    input logic                 wrst_n,
    input logic                 wen_n,
    input logic [WIDTH_G-1:0]   wdata,
    input logic                 wfull,
    input logic                 rclk,
    input logic                 rrst_n,
    input logic                 ren_n,
    input logic [WIDTH_G-1:0]   rdata,
    input logic                 rempty,
    input logic [DEPTHEXP:0]    waddr_wrside,
    input logic [DEPTHEXP:0]    raddr_rdside,
    input logic [DEPTHEXP:0]    waddr_rdside,
    input logic [DEPTHEXP:0]    raddr_wrside,
    input logic [DEPTHEXP:0]    wrbincount_wrside,
    input logic [DEPTHEXP:0]    rdbincount_rdside,
    input logic [DEPTHEXP:0]    rdbincount_wrside
);

  localparam int unsigned DEPTH = 2**DEPTHEXP;
  localparam int unsigned PTR_W = DEPTHEXP + 1;

  //========================================================================
  // ASSUMPTIONS  (mp_)
  //========================================================================

  mp_wen_not_when_full: assume property (
      @(posedge wclk) disable iff (!wrst_n)
      wfull |-> wen_n);

  mp_ren_not_when_empty: assume property (
      @(posedge rclk) disable iff (!rrst_n)
      rempty |-> ren_n);

  //========================================================================
  // FAIRNESS CONSTRAINTS  (s_eventually)
  //========================================================================

  mp_wen_n_asserts: assume property (
      @(posedge wclk) disable iff (!wrst_n)
      s_eventually !wen_n);

  mp_wen_n_deasserts: assume property (
      @(posedge wclk) disable iff (!wrst_n)
      s_eventually wen_n);

  mp_ren_n_asserts: assume property (
      @(posedge rclk) disable iff (!rrst_n)
      s_eventually !ren_n);

  mp_ren_n_deasserts: assume property (
      @(posedge rclk) disable iff (!rrst_n)
      s_eventually ren_n);

  //========================================================================
  // COVER POINTS FOR ALL ASSUMPTIONS  (UR-5)
  //========================================================================

  cp_wen_not_full_hit: cover property (
      @(posedge wclk) disable iff (!wrst_n)
      wfull && wen_n);

  cp_ren_not_empty_hit: cover property (
      @(posedge rclk) disable iff (!rrst_n)
      rempty && ren_n);

  cp_wen_asserted_hit: cover property (
      @(posedge wclk) disable iff (!wrst_n)
      !wen_n && !wfull);

  cp_ren_asserted_hit: cover property (
      @(posedge rclk) disable iff (!rrst_n)
      !ren_n && !rempty);

  //========================================================================
  // ASSERTIONS — WRITE DOMAIN  (ap_)
  //========================================================================

  // EXCEPTION 7b: wfull is obligation output — pure state guard. Y confirmed.
  ap_no_write_when_full: assert property (
      @(posedge wclk) disable iff (!wrst_n)
      wfull |-> ##1 (wrbincount_wrside == $past(wrbincount_wrside)))
    else $error("[%0t] ap_no_write_when_full FAILED: wptr advanced while full", $time);

  ap_wfull_reset: assert property (
      @(posedge wclk) disable iff (1'b0)
      !wrst_n |-> ##1 !wfull)
    else $error("[%0t] ap_wfull_reset FAILED: wfull not cleared after wrst_n", $time);

  ap_wptr_reset: assert property (
      @(posedge wclk) disable iff (1'b0)
      !wrst_n |-> ##1 (waddr_wrside == '0) && (wrbincount_wrside == '0))
    else $error("[%0t] ap_wptr_reset FAILED: write pointers not zeroed", $time);

  ap_wptr_gray_encoded: assert property (
      @(posedge wclk) disable iff (!wrst_n)
      waddr_wrside == (wrbincount_wrside ^ (wrbincount_wrside >> 1)))
    else $error("[%0t] ap_wptr_gray_encoded FAILED: wptr gray mismatch", $time);

  ap_wptr_increments_on_write: assert property (
      @(posedge wclk) disable iff (!wrst_n)
      (!wen_n && !wfull) |-> ##1
      (wrbincount_wrside == ($past(wrbincount_wrside) + (DEPTHEXP+1)'(1))))
    else $error("[%0t] ap_wptr_increments_on_write FAILED", $time);

  ap_wptr_stable_no_write: assert property (
      @(posedge wclk) disable iff (!wrst_n)
      (wen_n || wfull) |-> ##1
      (wrbincount_wrside == $past(wrbincount_wrside)))
    else $error("[%0t] ap_wptr_stable_no_write FAILED", $time);

  ap_full_condition: assert property (
      @(posedge wclk) disable iff (!wrst_n)
      wfull == ((rdbincount_wrside[DEPTHEXP-1:0] == wrbincount_wrside[DEPTHEXP-1:0]) &&
                (rdbincount_wrside[DEPTHEXP]     != wrbincount_wrside[DEPTHEXP])))
    else $error("[%0t] ap_full_condition FAILED: wfull encoding incorrect", $time);

  ap_wptr_no_overflow: assert property (
      @(posedge wclk) disable iff (!wrst_n)
      wrbincount_wrside <= (DEPTHEXP+1)'(2*DEPTH - 1))
    else $error("[%0t] ap_wptr_no_overflow FAILED", $time);

  //========================================================================
  // ASSERTIONS — READ DOMAIN  (ap_)
  //========================================================================

  // EXCEPTION 7b: rempty is obligation output — pure state guard. Y confirmed.
  ap_no_read_when_empty: assert property (
      @(posedge rclk) disable iff (!rrst_n)
      rempty |-> ##1 (rdbincount_rdside == $past(rdbincount_rdside)))
    else $error("[%0t] ap_no_read_when_empty FAILED: rptr advanced while empty", $time);

  ap_rempty_reset: assert property (
      @(posedge rclk) disable iff (1'b0)
      !rrst_n |-> ##1 rempty)
    else $error("[%0t] ap_rempty_reset FAILED: rempty not set after rrst_n", $time);

  ap_rptr_reset: assert property (
      @(posedge rclk) disable iff (1'b0)
      !rrst_n |-> ##1 (raddr_rdside == '0) && (rdbincount_rdside == '0))
    else $error("[%0t] ap_rptr_reset FAILED: read pointers not zeroed", $time);

  ap_rptr_gray_encoded: assert property (
      @(posedge rclk) disable iff (!rrst_n)
      raddr_rdside == (rdbincount_rdside ^ (rdbincount_rdside >> 1)))
    else $error("[%0t] ap_rptr_gray_encoded FAILED: rptr gray mismatch", $time);

  ap_rptr_increments_on_read: assert property (
      @(posedge rclk) disable iff (!rrst_n)
      (!ren_n && !rempty) |-> ##1
      (rdbincount_rdside == ($past(rdbincount_rdside) + (DEPTHEXP+1)'(1))))
    else $error("[%0t] ap_rptr_increments_on_read FAILED", $time);

  ap_rptr_stable_no_read: assert property (
      @(posedge rclk) disable iff (!rrst_n)
      (ren_n || rempty) |-> ##1
      (rdbincount_rdside == $past(rdbincount_rdside)))
    else $error("[%0t] ap_rptr_stable_no_read FAILED", $time);

  ap_empty_condition: assert property (
      @(posedge rclk) disable iff (!rrst_n)
      rempty == (raddr_rdside == waddr_rdside))
    else $error("[%0t] ap_empty_condition FAILED: rempty encoding incorrect", $time);

  ap_rptr_no_overflow: assert property (
      @(posedge rclk) disable iff (!rrst_n)
      rdbincount_rdside <= (DEPTHEXP+1)'(2*DEPTH - 1))
    else $error("[%0t] ap_rptr_no_overflow FAILED", $time);

  //========================================================================
  // ASSERTIONS — CROSS-DOMAIN STRUCTURAL  (ap_)
  //========================================================================

  ap_sync_wptr_stable_stage1: assert property (
      @(posedge rclk) disable iff (!rrst_n)
      ##1 (waddr_rdside == $past(waddr_rdside0)))
    else $error("[%0t] ap_sync_wptr_stable_stage1 FAILED", $time);

  //========================================================================
  // COVER POINTS FOR ALL ASSERTIONS  (cp_)
  //========================================================================

  cp_wfull_reached:             cover property (@(posedge wclk) disable iff (!wrst_n) wfull);
  cp_write_while_not_full:      cover property (@(posedge wclk) disable iff (!wrst_n) !wen_n && !wfull);
  cp_wptr_wraps:                cover property (@(posedge wclk) disable iff (!wrst_n)
      wrbincount_wrside == (DEPTHEXP+1)'(2*DEPTH - 1));
  cp_wfull_clears:              cover property (@(posedge wclk) disable iff (!wrst_n) $fell(wfull));
  cp_wfull_sets:                cover property (@(posedge wclk) disable iff (!wrst_n) $rose(wfull));
  cp_wptr_gray_one_hot_change:  cover property (@(posedge wclk) disable iff (!wrst_n)
      $onehot(waddr_wrside ^ $past(waddr_wrside)));

  cp_rempty_reached:            cover property (@(posedge rclk) disable iff (!rrst_n) rempty);
  cp_read_while_not_empty:      cover property (@(posedge rclk) disable iff (!rrst_n) !ren_n && !rempty);
  cp_rptr_wraps:                cover property (@(posedge rclk) disable iff (!rrst_n)
      rdbincount_rdside == (DEPTHEXP+1)'(2*DEPTH - 1));
  cp_rempty_clears:             cover property (@(posedge rclk) disable iff (!rrst_n) $fell(rempty));
  cp_rempty_sets:               cover property (@(posedge rclk) disable iff (!rrst_n) $rose(rempty));
  cp_rptr_gray_one_hot_change:  cover property (@(posedge rclk) disable iff (!rrst_n)
      $onehot(raddr_rdside ^ $past(raddr_rdside)));

  cp_wptr_sync_stage1_changes:  cover property (@(posedge rclk) disable iff (!rrst_n)
      waddr_rdside0 != $past(waddr_rdside0));
  cp_rptr_sync_stage1_changes:  cover property (@(posedge wclk) disable iff (!wrst_n)
      raddr_wrside0 != $past(raddr_wrside0));

endmodule : fifo_async_sva

`default_nettype wire