// AXI4-Lite protocol monitor (passive). Corvel / RISCON Labs integration testbench.
// Checks the slave-side obligations of AMBA AXI4-Lite and, as a BFM sanity
// check, the master-side VALID-hold rules. Counts transactions and the
// relative ordering of AW and W handshakes. Runs in Icarus (-g2012) and Verilator.
`timescale 1ns/1ps
module axil_monitor #(parameter integer AW = 12) (
    input wire          clk,
    input wire          rst_n,
    input wire [AW-1:0] awaddr, input wire awvalid, input wire awready,
    input wire [31:0]   wdata,  input wire [3:0] wstrb, input wire wvalid, input wire wready,
    input wire [1:0]    bresp,  input wire bvalid, input wire bready,
    input wire [AW-1:0] araddr, input wire arvalid, input wire arready,
    input wire [31:0]   rdata,  input wire [1:0] rresp, input wire rvalid, input wire rready
);
    integer errors = 0;
    integer n_aw = 0, n_w = 0, n_b = 0, n_ar = 0, n_r = 0;
    integer n_b_okay = 0, n_b_slverr = 0, n_r_okay = 0, n_r_slverr = 0;
    integer n_aw_first = 0, n_w_first = 0, n_same = 0;
    integer max_wr_out = 0, max_rd_out = 0;
    integer n_back_to_back_aw = 0, n_back_to_back_ar = 0;
    integer cyc = 0;
    // latency / spacing statistics (cycles between handshake edges)
    integer wr_lat_min = 1 << 30, rd_lat_min = 1 << 30, aw_gap_min = 1 << 30, ar_gap_min = 1 << 30;
    integer last_aw = -1000, last_ar = -1000;
    integer ar_cyc [0:65535];
    // handshake cycle of every AW / W (for ordering statistics)
    integer aw_cyc [0:65535];
    integer w_cyc  [0:65535];

    reg p_awvalid, p_awready, p_wvalid, p_wready, p_bvalid, p_bready;
    reg p_arvalid, p_arready, p_rvalid, p_rready;
    reg [AW-1:0] p_awaddr, p_araddr;
    reg [31:0] p_wdata, p_rdata;
    reg [3:0]  p_wstrb;
    reg [1:0]  p_bresp, p_rresp;
    reg        p_aw_hs, p_ar_hs;

    task automatic fail(input string what);
        begin
            errors = errors + 1;
            if (errors <= 20) $display("[%0t] AXIL-MON ERROR: %0s", $time, what);
        end
    endtask

    // Slave outputs must not be X/Z once reset is released. (XOR-reduction idiom:
    // Icarus 13 mis-evaluates $isunknown() of a wide concatenation inside if().)
    always @(posedge clk) if (rst_n) begin
        if ((^{awready, wready, bvalid, bresp, arready, rvalid, rresp, rdata}) === 1'bx)
            fail("X/Z on AXI4-Lite slave output");
    end

    always @(posedge clk or negedge rst_n) begin
        if (!rst_n) begin
            p_awvalid <= 0; p_awready <= 0; p_wvalid <= 0; p_wready <= 0;
            p_bvalid <= 0; p_bready <= 0; p_arvalid <= 0; p_arready <= 0;
            p_rvalid <= 0; p_rready <= 0; p_aw_hs <= 0; p_ar_hs <= 0;
            p_awaddr <= 0; p_araddr <= 0; p_wdata <= 0; p_rdata <= 0; p_wstrb <= 0;
            p_bresp <= 0; p_rresp <= 0;
        end else begin
            cyc = cyc + 1;
            // ---- master obligations (BFM sanity) ----
            if (p_awvalid && !p_awready && (!awvalid || awaddr !== p_awaddr)) fail("AWVALID/AWADDR changed before AWREADY");
            if (p_wvalid  && !p_wready  && (!wvalid || wdata !== p_wdata || wstrb !== p_wstrb)) fail("WVALID/WDATA changed before WREADY");
            if (p_arvalid && !p_arready && (!arvalid || araddr !== p_araddr)) fail("ARVALID/ARADDR changed before ARREADY");
            // ---- slave obligations ----
            if (p_bvalid && !p_bready && (!bvalid || bresp !== p_bresp)) fail("BVALID/BRESP changed before BREADY");
            if (p_rvalid && !p_rready && (!rvalid || rdata !== p_rdata || rresp !== p_rresp)) fail("RVALID/RDATA/RRESP changed before RREADY");
            if (bvalid && !(n_b < n_aw && n_b < n_w)) fail("BVALID without completed AW and W");
            if (rvalid && !(n_r < n_ar)) fail("RVALID without accepted AR");
            // ---- handshakes ----
            // back-to-back: the master presents the next address in the cycle right
            // after the previous address handshake (no idle cycle on the channel)
            if (p_aw_hs && awvalid) n_back_to_back_aw = n_back_to_back_aw + 1;
            if (p_ar_hs && arvalid) n_back_to_back_ar = n_back_to_back_ar + 1;
            if (awvalid && awready) begin
                if (n_aw < 65536) aw_cyc[n_aw] = cyc;
                if (cyc - last_aw < aw_gap_min) aw_gap_min = cyc - last_aw;
                last_aw = cyc;
                n_aw = n_aw + 1;
            end
            if (wvalid && wready) begin
                if (n_w < 65536) w_cyc[n_w] = cyc;
                n_w = n_w + 1;
            end
            if (arvalid && arready) begin
                if (n_ar < 65536) ar_cyc[n_ar] = cyc;
                if (cyc - last_ar < ar_gap_min) ar_gap_min = cyc - last_ar;
                last_ar = cyc;
                n_ar = n_ar + 1;
            end
            if (bvalid && bready) begin
                if (n_b < 65536) begin
                    if (cyc - ((aw_cyc[n_b] > w_cyc[n_b]) ? aw_cyc[n_b] : w_cyc[n_b]) < wr_lat_min)
                        wr_lat_min = cyc - ((aw_cyc[n_b] > w_cyc[n_b]) ? aw_cyc[n_b] : w_cyc[n_b]);
                    if (aw_cyc[n_b] < w_cyc[n_b]) n_aw_first = n_aw_first + 1;
                    else if (aw_cyc[n_b] > w_cyc[n_b]) n_w_first = n_w_first + 1;
                    else n_same = n_same + 1;
                end
                if (bresp == 2'b00) n_b_okay = n_b_okay + 1;
                else if (bresp == 2'b10) n_b_slverr = n_b_slverr + 1;
                else fail("BRESP is neither OKAY nor SLVERR");
                n_b = n_b + 1;
            end
            if (rvalid && rready) begin
                if (n_r < 65536 && cyc - ar_cyc[n_r] < rd_lat_min) rd_lat_min = cyc - ar_cyc[n_r];
                if (rresp == 2'b00) n_r_okay = n_r_okay + 1;
                else if (rresp == 2'b10) n_r_slverr = n_r_slverr + 1;
                else fail("RRESP is neither OKAY nor SLVERR");
                n_r = n_r + 1;
            end
            if ((n_aw - n_b) > max_wr_out) max_wr_out = n_aw - n_b;
            if ((n_ar - n_r) > max_rd_out) max_rd_out = n_ar - n_r;
            p_awvalid <= awvalid; p_awready <= awready; p_wvalid <= wvalid; p_wready <= wready;
            p_bvalid <= bvalid; p_bready <= bready; p_arvalid <= arvalid; p_arready <= arready;
            p_rvalid <= rvalid; p_rready <= rready;
            p_awaddr <= awaddr; p_araddr <= araddr; p_wdata <= wdata; p_wstrb <= wstrb;
            p_rdata <= rdata; p_bresp <= bresp; p_rresp <= rresp;
            p_aw_hs <= awvalid && awready; p_ar_hs <= arvalid && arready;
        end
    end

    // On reset, transactions in flight are discarded: re-align the counters.
    always @(negedge rst_n) begin
        n_aw = n_b; n_w = n_b; n_ar = n_r;
    end
endmodule