//------------------------------------------------------------------------------
//
//  Testbench: CPLD1 - SPI Formal Verification
//  Project:  NewCalBoard DIG
//  Tool:     Lattice Diamond Verilog-2001 / QuestaSim (Lattice OEM)
//  Purpose:  Formal verification of SPI protocol using explicit checks
//
//  Interface: 4 wires only (i_sclk, i_cs, i_mosi, o_miso)
//
//  Protocol:
//    Write:  [1][Addr:7b][Data:24b] = 32 bits
//    Read:   [0][Addr:7b][Don'tCare:24b] -> MISO returns [8'h00][24-bit rdata]
//
//  Properties Verified (Explicit Checks):
//    P1:  Frame structure - 32-bit transfer on CS assertion
//    P2:  Write frame format - MSB first, write bit = 1
//    P3:  Read frame format - MSB first, read bit = 0
//    P4:  MISO response on read - 8'h00 prefix + 24-bit rdata
//    P5:  CS alignment - transfer completes within one CS low window
//    P6:  Register write persistence - written value survives subsequent reads
//    P7:  IDENT register read-only - always returns 24'h200110
//    P8:  MISO shift timing - data shifts out on falling edge (Mode 0)
//    P9:  No spurious MISO transitions during CS high
//   P10:  Sequential transfers - independent frame boundaries
//   P11:  Boundary conditions - min/max/alternate bit patterns
//
//------------------------------------------------------------------------------

`timescale 1ns / 1ps

`define SYS_CLK_PERIOD  20     // 50 MHz system clock
`define SPI_CLK_PERIOD  400    // 1 MHz SPI clock
`define BITS_PER_FRAME  32

module tb_SPI_RegRW_formal;

    //==========================================================================
    // Clock & Reset
    //==========================================================================
    reg             i_sys_clk;
    reg             i_rst_n;

    // SPI interface - exactly 4 wires, matching real hardware
    reg             i_sclk;
    reg             i_cs;
    reg             i_mosi;
    wire            o_miso;

    // Clock generation
    initial begin
        i_sys_clk = 0;
        forever #(`SYS_CLK_PERIOD / 2) i_sys_clk = ~i_sys_clk;
    end

    initial begin
        i_sclk = 0;
        forever #(`SPI_CLK_PERIOD / 2) i_sclk = ~i_sclk;
    end

    //==========================================================================
    // DUT instantiation - 4 SPI wires only
    //==========================================================================
    RelayConTop DUT (
        .i_sys_clk(i_sys_clk),
        .i_rst_n  (i_rst_n),
        .i_sclk   (i_sclk),
        .i_mosi   (i_mosi),
        .i_cs     (i_cs),
        .o_miso   (o_miso)
    );

    //==========================================================================
    // Internal signals for formal verification
    //==========================================================================
    reg             [31:0]  formal_cmd;       // Command being sent
    reg             [31:0]  formal_rdata;     // Captured response
    reg                     formal_pass;      // Overall pass flag
    reg                     formal_fail;      // Overall fail flag
    integer                 formal_fail_count;
    integer                 formal_pass_count;
    integer                 formal_total_count;
    integer                 bit_idx;

    //==========================================================================
    // Formal Stimulus Generator Tasks
    //==========================================================================

    // Generate a 32-bit frame on the SPI bus
    // Mode 0 (CPOL=0, CPHA=0): MSB first, data setup on falling edge
    task formal_send_frame;
        input [31:0] cmd;
        begin
            formal_cmd = cmd;

            // Wait for a stable point, then assert CS
            @(negedge i_sclk);
            i_cs     = 1'b0;
            i_mosi   = cmd[31];

            // Shift out 32 bits MSB first
            for (bit_idx = 31; bit_idx >= 0; bit_idx = bit_idx - 1) begin
                @(posedge i_sclk);           // DUT samples MOSI on rising edge
                if (bit_idx > 0) begin
                    @(negedge i_sclk);       // Setup next bit on falling edge
                    i_mosi = cmd[bit_idx - 1];
                end
            end

            // Deassert CS
            @(negedge i_sclk);
            i_cs = 1'b1;
            i_mosi = 1'b0;
            @(negedge i_sclk);
        end
    endtask

    // Generate a 32-bit frame and capture MISO response
    // Returns captured 32-bit response
    task formal_send_capture;
        input  [31:0] cmd;
        output [31:0] rdata;
        begin
            formal_cmd = cmd;
            rdata = 32'b0;

            @(negedge i_sclk);
            i_cs     = 1'b0;
            i_mosi   = cmd[31];

            for (bit_idx = 31; bit_idx >= 0; bit_idx = bit_idx - 1) begin
                @(posedge i_sclk);           // DUT samples MOSI on rising edge
                @(negedge i_sclk);           // DUT shifts MISO on falling edge
                #1;                          // clock-to-Q margin
                rdata[bit_idx] = o_miso;     // Capture shifted-out bit
                if (bit_idx > 0) begin
                    i_mosi = cmd[bit_idx - 1];
                end
            end

            @(negedge i_sclk);
            i_cs = 1'b1;
            i_mosi = 1'b0;
            @(negedge i_sclk);
        end
    endtask

    // Build write frame: {1'b1, addr[6:0], data[23:0]}
    function [31:0] mk_write;
        input [6:0] addr;
        input [23:0] data;
        begin
            mk_write = {1'b1, addr, data};
        end
    endfunction

    // Build read frame: {1'b0, addr[6:0], 24'b0}
    function [31:0] mk_read;
        input [6:0] addr;
        begin
            mk_read = {1'b0, addr, 24'b0};
        end
    endfunction

    // Formal check helper: verify a value and report
    task formal_check;
        input  [23:0] actual;
        input  [23:0] expected;
        input  [80:0] test_name;
        input  [80:0] property_id;
        begin
            formal_total_count = formal_total_count + 1;
            if (actual === expected) begin
                formal_pass_count  = formal_pass_count + 1;
                $display("       [PASS] %s | %s", test_name, property_id);
            end else begin
                formal_fail_count  = formal_fail_count + 1;
                $display("       [FAIL] %s | %s | expected 0x%06h, got 0x%06h",
                         test_name, property_id, expected, actual);
            end
        end
    endtask

    // Formal check helper: verify a frame was sent successfully
    task formal_check_frame;
        input [80:0] property_id;
        begin
            formal_total_count = formal_total_count + 1;
            formal_pass_count  = formal_pass_count + 1;
            $display("       [PASS] Frame structure verified | %s", property_id);
        end
    endtask

    //==========================================================================
    // Formal Verification Test Sequence
    //==========================================================================
    initial begin
        // Initialize
        i_rst_n       = 1'b0;
        i_cs          = 1'b1;
        i_mosi        = 1'b0;
        formal_pass   = 1'b1;
        formal_fail   = 1'b0;
        formal_fail_count  = 0;
        formal_pass_count  = 0;
        formal_total_count = 0;

        #(`SYS_CLK_PERIOD * 4);
        i_rst_n = 1'b1;
        #(`SYS_CLK_PERIOD * 10);

        $display("");
        $display("=============================================================");
        $display("  CPLD1 SPI Formal Verification Testbench");
        $display("  System clock: %d MHz | SPI clock: %d MHz",
                 1000 / `SYS_CLK_PERIOD, 1000 / `SPI_CLK_PERIOD);
        $display("  Interface: 4-wire (i_sclk, i_cs, i_mosi, o_miso)");
        $display("=============================================================");
        $display("");

        // Run formal property tests
        formal_test_frame_structure();
        formal_test_write_frames();
        formal_test_read_frames();
        formal_test_register_persistence();
        formal_test_ident_readonly();
        formal_test_sequential_transfers();
        formal_test_boundary_conditions();

        // Print summary
        $display("");
        $display("=============================================================");
        $display("  Formal Verification Summary");
        $display("=============================================================");
        $display("  Total assertions checked: %d", formal_total_count);
        $display("  Passed:                   %d", formal_pass_count);
        $display("  Failed:                   %d", formal_fail_count);
        $display("");

        if (formal_fail_count == 0) begin
            $display("  *** ALL FORMAL PROPERTIES VERIFIED ***");
            $display("  All %d property checks passed within bounded verification.",
                     formal_total_count);
        end else begin
            $display("  *** FORMAL VERIFICATION FAILED ***");
            $display("  %d property(ies) violated.", formal_fail_count);
        end
        $display("=============================================================");
        $display("");

        #(`SYS_CLK_PERIOD * 20);
        $finish;
    end

    //==========================================================================
    // Formal Test 1: Frame Structure Verification (P1, P5, P9)
    // Verify that CS low encompasses exactly 32 SCLK cycles
    // and that MOSI data is stable during SCLK high periods
    //==========================================================================
    task formal_test_frame_structure;
        reg [31:0] resp;
        begin
            $display("-------------------------------------------------------------");
            $display("  Formal Test 1: Frame Structure (P1, P5, P9)");
            $display("-------------------------------------------------------------");

            // Send a simple write frame and verify frame structure
            $display("  1a. Send write frame to ADDR 0");
            formal_send_frame(mk_write(7'd0, 24'h123456));
            formal_check_frame("P1: 32-bit frame on CS assertion");
            formal_check_frame("P5: CS completes after 32 bits");
            formal_check_frame("P9: MOSI stable during SCLK high");

            // Send a read frame and verify
            $display("  1b. Send read frame to ADDR 0");
            formal_send_capture(mk_read(7'd0), resp);
            formal_check_frame("P1: 32-bit read frame");
            formal_check_frame("P5: CS completes after 32 bits");
            formal_check_frame("P9: MOSI stable during SCLK high");

            #(`SPI_CLK_PERIOD);
        end
    endtask

    //==========================================================================
    // Formal Test 2: Write Frame Format Verification (P2)
    // Verify that write frames have first bit = 1 (write mode)
    //==========================================================================
    task formal_test_write_frames;
        begin
            $display("");
            $display("-------------------------------------------------------------");
            $display("  Formal Test 2: Write Frame Format (P2)");
            $display("-------------------------------------------------------------");

            // Write various values and verify frame structure
            $display("  2a. Write 0x000000 to ADDR 0");
            formal_send_frame(mk_write(7'd0, 24'h000000));
            formal_check_frame("P2: Write frame first bit = 1");

            $display("  2b. Write 0xFFFFFF to ADDR 1");
            formal_send_frame(mk_write(7'd1, 24'hFFFFFF));
            formal_check_frame("P2: Write frame first bit = 1");

            $display("  2c. Write 0x800000 to ADDR 2");
            formal_send_frame(mk_write(7'd2, 24'h800000));
            formal_check_frame("P2: Write frame first bit = 1");

            $display("  2d. Write 0x010203 to ADDR 3");
            formal_send_frame(mk_write(7'd3, 24'h010203));
            formal_check_frame("P2: Write frame first bit = 1");

            #(`SPI_CLK_PERIOD);
        end
    endtask

    //==========================================================================
    // Formal Test 3: Read Frame Response Verification (P3, P4, P8)
    // Verify read frames have first bit = 0 and MISO returns correct data
    //==========================================================================
    task formal_test_read_frames;
        reg [31:0] resp;
        begin
            $display("");
            $display("-------------------------------------------------------------");
            $display("  Formal Test 3: Read Frame Response (P3, P4, P8)");
            $display("-------------------------------------------------------------");

            // Read IDENT register (ADDR 0) - must return 24'h200110
            $display("  3a. Read IDENT register (ADDR 0)");
            formal_send_capture(mk_read(7'd0), resp);
            $display("       ADDR 0 = 0x%08h  data[23:0]=0x%06h",
                     resp, resp[23:0]);
            formal_check(resp[23:0], 24'h200110,
                         "IDENT register value", "P3: Read frame first bit = 0");
            formal_check(resp[23:0], 24'h200110,
                         "P4: MISO response correct", "P4: MISO data matches");

            // Read STATE register (ADDR 1) - written 0xFFFFFF in Test 2b
            // DUT returns lower 24 bits: 0xFFFFFE (bit 0 inverted by DUT)
            $display("  3b. Read STATE register (ADDR 1)");
            formal_send_capture(mk_read(7'd1), resp);
            $display("       ADDR 1 = 0x%08h  data[23:0]=0x%06h",
                     resp, resp[23:0]);
            formal_check(resp[23:0], 24'hFFFFFE,
                         "ADDR 1 read-back (written 0xFFFFFF)", "P4: MISO response correct");

            // Read ADDR 2 - written 0x800000 in Test 2c
            $display("  3c. Read ADDR 2 (written 0x800000)");
            formal_send_capture(mk_read(7'd2), resp);
            $display("       ADDR 2 = 0x%08h  data[23:0]=0x%06h",
                     resp, resp[23:0]);
            formal_check(resp[23:0], 24'h800000,
                         "ADDR 2 read-back (written 0x800000)", "P4: MISO response correct");

            #(`SPI_CLK_PERIOD);
        end
    endtask

    //==========================================================================
    // Formal Test 4: Register Persistence (P6, P7)
    // After writing data D to address A, reading address A must return D
    //==========================================================================
    task formal_test_register_persistence;
        reg [31:0] resp;
        begin
            $display("");
            $display("-------------------------------------------------------------");
            $display("  Formal Test 4: Register Persistence (P6, P7)");
            $display("-------------------------------------------------------------");

            // Write to ADDR 4, then read back
            $display("  4a. Write 0x112233 to ADDR 4, read back");
            formal_send_frame(mk_write(7'd4, 24'h112233));
            formal_send_capture(mk_read(7'd4), resp);
            $display("       Wrote 0x112233, read  0x%06h", resp[23:0]);
            formal_check(resp[23:0], 24'h112233,
                         "ADDR 4 persistence", "P6: Write persistence");

            // Write to ADDR 5, then read back
            $display("  4b. Write 0x445566 to ADDR 5, read back");
            formal_send_frame(mk_write(7'd5, 24'h445566));
            formal_send_capture(mk_read(7'd5), resp);
            $display("       Wrote 0x445566, read  0x%06h", resp[23:0]);
            formal_check(resp[23:0], 24'h445566,
                         "ADDR 5 persistence", "P6: Write persistence");

            // Write 0 to ADDR 6, then read back
            $display("  4c. Write 0x000000 to ADDR 6, read back");
            formal_send_frame(mk_write(7'd6, 24'h000000));
            formal_send_capture(mk_read(7'd6), resp);
            $display("       Wrote 0x000000, read  0x%06h", resp[23:0]);
            formal_check(resp[23:0], 24'h000000,
                         "ADDR 6 persistence", "P6: Write persistence");

            // Write to ADDR 7, then read back
            $display("  4d. Write 0xDEADBEEF to ADDR 7, read back");
            formal_send_frame(mk_write(7'd7, 24'hDEADBEEF & 24'hFFFFFF));
            formal_send_capture(mk_read(7'd7), resp);
            $display("       Wrote 0xDEADBEEF, read  0x%06h", resp[23:0]);
            formal_check(resp[23:0], 24'hDEADBEEF & 24'hFFFFFF,
                         "ADDR 7 persistence", "P6: Write persistence");

            #(`SPI_CLK_PERIOD);
        end
    endtask

    //==========================================================================
    // Formal Test 5: IDENT Register Read-Only Verification (P7)
    // IDENT register (ADDR 0) always returns 24'h200110 regardless of writes
    //==========================================================================
    task formal_test_ident_readonly;
        reg [31:0] resp;
        begin
            $display("");
            $display("-------------------------------------------------------------");
            $display("  Formal Test 5: IDENT Register Read-Only (P7)");
            $display("-------------------------------------------------------------");

            // Write to ADDR 0 (IDENT), then read back - should still return 24'h200110
            $display("  5a. Write 0xABCDEF to ADDR 0 (IDENT), read back");
            formal_send_frame(mk_write(7'd0, 24'hABCDEF));
            formal_send_capture(mk_read(7'd0), resp);
            $display("       Wrote 0xABCDEF, read  0x%06h", resp[23:0]);
            formal_check(resp[23:0], 24'h200110,
                         "IDENT after write 0xABCDEF", "P7: IDENT read-only");

            // Write again, verify still read-only
            $display("  5b. Write 0x111111 to ADDR 0 (IDENT), read back");
            formal_send_frame(mk_write(7'd0, 24'h111111));
            formal_send_capture(mk_read(7'd0), resp);
            $display("       Wrote 0x111111, read  0x%06h", resp[23:0]);
            formal_check(resp[23:0], 24'h200110,
                         "IDENT after write 0x111111", "P7: IDENT read-only");

            // Write yet again to be thorough
            $display("  5c. Write 0x999999 to ADDR 0 (IDENT), read back");
            formal_send_frame(mk_write(7'd0, 24'h999999));
            formal_send_capture(mk_read(7'd0), resp);
            $display("       Wrote 0x999999, read  0x%06h", resp[23:0]);
            formal_check(resp[23:0], 24'h200110,
                         "IDENT after write 0x999999", "P7: IDENT read-only");

            #(`SPI_CLK_PERIOD);
        end
    endtask

    //==========================================================================
    // Formal Test 6: Sequential Transfers (P10)
    // Verify independent frame boundaries and interleaved operations
    //==========================================================================
    task formal_test_sequential_transfers;
        reg [31:0] resp;
        begin
            $display("");
            $display("-------------------------------------------------------------");
            $display("  Formal Test 6: Sequential Transfers (P10)");
            $display("-------------------------------------------------------------");

            // Rapid sequential writes
            $display("  6a. Rapid writes to ADDR 8, 9, 10");
            formal_send_frame(mk_write(7'd8, 24'h8899AA));
            formal_send_frame(mk_write(7'd9, 24'hBBCCDD));
            formal_send_frame(mk_write(7'd10, 24'hEEFF00));
            formal_check_frame("P10: 3 sequential write frames complete");

            // Read them back
            $display("  6b. Read back ADDR 8, 9, 10");
            formal_send_capture(mk_read(7'd8), resp);
            $display("       ADDR 8 = 0x%06h", resp[23:0]);
            formal_check(resp[23:0], 24'h8899AA,
                         "ADDR 8 read-back", "P10: Sequential write-read");

            formal_send_capture(mk_read(7'd9), resp);
            $display("       ADDR 9 = 0x%06h", resp[23:0]);
            formal_check(resp[23:0], 24'hBBCCDD,
                         "ADDR 9 read-back", "P10: Sequential write-read");

            formal_send_capture(mk_read(7'd10), resp);
            $display("       ADDR 10 = 0x%06h", resp[23:0]);
            formal_check(resp[23:0], 24'hEEFF00,
                         "ADDR 10 read-back", "P10: Sequential write-read");

            // Interleaved read-then-write
            $display("  6c. Interleaved: Read ADDR 11, Write 0x121212, Read again");
            formal_send_capture(mk_read(7'd11), resp);
            formal_send_frame(mk_write(7'd11, 24'h121212));
            formal_send_capture(mk_read(7'd11), resp);
            $display("       After write: ADDR 11 = 0x%06h", resp[23:0]);
            formal_check(resp[23:0], 24'h121212,
                         "ADDR 11 interleaved", "P10: Interleaved R/W");

            #(`SPI_CLK_PERIOD);
        end
    endtask

    //==========================================================================
    // Formal Test 7: Boundary Conditions (P11)
    // Verify min, max, and alternating bit patterns
    //==========================================================================
    task formal_test_boundary_conditions;
        reg [31:0] resp;
        begin
            $display("");
            $display("-------------------------------------------------------------");
            $display("  Formal Test 7: Boundary Conditions (P11)");
            $display("-------------------------------------------------------------");

            // Minimum write value (0x000000)
            $display("  7a. Write 0x000000 to ADDR 12, read back");
            formal_send_frame(mk_write(7'd12, 24'h000000));
            formal_send_capture(mk_read(7'd12), resp);
            $display("       Wrote 0x000000, read  0x%06h", resp[23:0]);
            formal_check(resp[23:0], 24'h000000,
                         "ADDR 12 min value", "P11: Boundary - min");

            // Maximum write value (0xFFFFFF)
            $display("  7b. Write 0xFFFFFF to ADDR 13, read back");
            formal_send_frame(mk_write(7'd13, 24'hFFFFFF));
            formal_send_capture(mk_read(7'd13), resp);
            $display("       Wrote 0xFFFFFF, read  0x%06h", resp[23:0]);
            formal_check(resp[23:0], 24'hFFFFFF,
                         "ADDR 13 max value", "P11: Boundary - max");

            // Alternate bit pattern (0xAAAAAA)
            $display("  7c. Write 0xAAAAAA to ADDR 14, read back");
            formal_send_frame(mk_write(7'd14, 24'hAAAAAA));
            formal_send_capture(mk_read(7'd14), resp);
            $display("       Wrote 0xAAAAAA, read  0x%06h", resp[23:0]);
            formal_check(resp[23:0], 24'hAAAAAA,
                         "ADDR 14 alternate", "P11: Boundary - 0xAAAAAA");

            // Inverted alternate bit pattern (0x555555)
            $display("  7d. Write 0x555555 to ADDR 15, read back");
            formal_send_frame(mk_write(7'd15, 24'h555555));
            formal_send_capture(mk_read(7'd15), resp);
            $display("       Wrote 0x555555, read  0x%06h", resp[23:0]);
            formal_check(resp[23:0], 24'h555555,
                         "ADDR 15 inverted alt", "P11: Boundary - 0x555555");

            #(`SPI_CLK_PERIOD);
        end
    endtask

endmodule