Sync with 'master'feature/fu

Signed-off-by: Warrick Lo <wlo@warricklo.net>

7 files changed, 0 insertions, 418 deletions

diff --git a/verif/formal/regfile/regfile.sby b/verif/formal/regfile/regfile.sby
deleted file mode 100644
index 69cb7b9..0000000
--- a/verif/formal/regfile/regfile.sby
+++ /dev/null
@@ -1,23 +0,0 @@
-[tasks]
-cover
-prove
-
-[options]
-cover: mode cover
-prove: mode prove
-prove: depth 20
-
-[engines]
-smtbmc
-
-[script]
-read -formal -sv config_pkg.sv
-read -formal -sv regfile.sv
-read -formal -sv regfile_fv.sv
-prep -top regfile_fv
-
-[files]
-rtl/types.svh
-rtl/config_pkg.sv
-rtl/regfile.sv
-verif/formal/regfile/regfile_fv.sv
diff --git a/verif/formal/regfile/regfile_fv.sv b/verif/formal/regfile/regfile_fv.sv
deleted file mode 100644
index 795024e..0000000
--- a/verif/formal/regfile/regfile_fv.sv
+++ /dev/null
@@ -1,248 +0,0 @@
-/* SPDX-License-Identifier: CERN-OHL-P-2.0 */
-
-/*
- * Copyright 2026 UBC ASIC contributors (Montreal project).
- *
- * Author: Warrick Lo <wlo@warricklo.net>
- *
- * Formal verification of regfile requirements
- *
- * This module verifies the regfile module against the requirements
- * specified in the design specification.
- *
- * The following parameters are used for all tests:
- * - Word width:           32 bits wide
- * - Slice width:          8 bits wide
- * - Number of words:      16 words
- * - Number of read ports: 2
- *
- * The following are design requirements that are assumed to be verifed by construction:
- * - REQ-REGFILE-010
- * - REQ-REGFILE-040
- * REQ-REGFILE-010 is further verified below.
- *
- * The following requirements are verified through this module:
- * - Cover:
- *   - REQ-REGFILE-053
- * - Bounded model checking:
- *   - REQ-REGFILE-010
- *   - REQ-REGFILE-053
- * - K-induction:
- *   - REQ-REGFILE-020
- *   - REQ-REGFILE-030
- *   - REQ-REGFILE-041
- *   - REQ-REGFILE-042
- *   - REQ-REGFILE-043
- *   - REQ-REGFILE-050
- *   - REQ-REGFILE-051
- *   - REQ-REGFILE-052
- *   - REQ-REGFILE-060
- *
- * See also: MAS, Regfile Specification, version 0.2
- *           rtl/regfile.sv
- */
-
-`include "types.svh"
-
-module regfile_fv (
-  input logic clk_i,
-  input logic rst_ni,
-  input logic [1:0] slice_sel_i,
-
-  input logic [1:0][3:0] raddr_i,
-
-  input logic wen_i,
-  input logic [3:0] waddr_i,
-  input logic [7:0] wdata_i
-);
-
-  /*
-   * DUT interface and internal signals.
-   */
-
-  word_bank_t register;
-  logic [1:0][7:0] rdata;
-
-  /*
-   * DUT instance.
-   */
-
-  regfile #(
-    .XLEN(32),
-    .SLICE_WIDTH(8),
-    .ADDR_WIDTH(4),
-    .NUM_READ_PORTS(2)
-  ) dut (
-    .register_dbg(register),
-    .clk_i,
-    .rst_ni,
-    .slice_sel_i,
-
-    .raddr_i,
-    .rdata_o(rdata),
-
-    .wen_i,
-    .waddr_i,
-    .wdata_i
-  );
-
-  /*
-   * Some assertions use $past(), which requires at least one clock edge.
-   * Those tests will use past_valid to check if a valid history exists.
-   */
-
-  logic past_valid;
-
-  initial assume (past_valid == '0);
-
-  always_ff @(posedge clk_i) begin : past_valid_dff
-    /* verilog_lint: waive dff-name-style */
-    past_valid <= '1;
-  end : past_valid_dff
-
-  /*
-   * REQ-REGFILE-010:
-   * The module must store NUM_WORDS words, each XLEN bits wide.
-   */
-
-  /* The definition of 'register' must use the type defined in types.svh. */
-  initial assert ($bits(register) == 16 * 32);
-
-  /*
-   * REQ-REGFILE-020:
-   * Slice k of word n shall correspond to bits [(k+1)*SLICE_WIDTH−1:k*SLICE_WIDTH]
-   * of register n, partitioning each word into XLEN/SLICE_WIDTH
-   * non-overlapping slices, each SLICE_WIDTH bits wide.
-   *
-   * REQ-REGFILE-050:
-   * The read output rdata_o[i] shall be combinationally derived from
-   * the current register state, raddr_i[i], and slice_sel_i. There shall not
-   * be any latency on reads.
-   *
-   * REQ-REGFILE-051:
-   * The read output rdata_o[i] must reflect the slice selected by slice_sel_i
-   * within the register selected by raddr_i[i].
-   *
-   * Note: These three requirements are easiest to verify together.
-   */
-
-  /* We explicitly ignore the use of part-selects to verify the description of REQ-REGFILE-020. */
-  always_comb begin : req_020_050_051
-    if (raddr_i[0] != '0) begin
-      assert (rdata[0] == register[raddr_i[0]][(slice_sel_i + 1) * 8 - 1 : slice_sel_i * 8]);
-    end
-    if (raddr_i[1] != '0) begin
-      assert (rdata[1] == register[raddr_i[1]][(slice_sel_i + 1) * 8 - 1 : slice_sel_i * 8]);
-    end
-  end : req_020_050_051
-
-  /*
-   * REQ-REGFILE-030:
-   * Register contents must be 0 at most one clock after the synchronous reset is asserted.
-   */
-
-  always_ff @(posedge clk_i) begin : req_030
-    if (past_valid && $past(!rst_ni, 1)) begin
-      assert (register == '0);
-    end
-  end : req_030
-
-  /*
-   * REQ-REGFILE-041:
-   * Writes to the register file must only occur when wen_i is asserted.
-   */
-
-  always_ff @(posedge clk_i) begin : req_041
-    if (past_valid && $past(rst_ni && !wen_i, 1)) begin
-      /* Satisfies the requirement, but possibly not the intended RTL behaviour.
-       * See ticket #14. */
-      assert ($stable(register));
-    end
-  end : req_041
-
-  /*
-   * REQ-REGFILE-042:
-   * Contents of wdata_i must be written only to the slice selected by slice_sel_i
-   * within the register selected by waddr_i. All other slices of the target register
-   * shall remain unchanged.
-   */
-
-  /* We'll use a part-select to obtain the slice data since we can assume that
-   * slice_sel_i will select the correct slice within the target register,
-   * according to requirement REQ-REGFILE-020. */
-  always_ff @(posedge clk_i) begin : req_042
-    /* For register 0, this test will specifically permit writes targeting
-     * the register to succeed. The stability of register 0 is separately
-     * verified below in REQ-REGFILE-043. */
-    for (int i = 0; i < 16; i++) begin : word_loop
-      for (int j = 0; j < 4; j++) begin : slice_loop
-        /* Ignore reset events. */
-        if (past_valid && $past(rst_ni, 1)) begin
-          if ($past((waddr_i == i) && (slice_sel_i == j), 1)) begin
-            assert ($stable(register[i][j*8+:8]) || (register[i][j*8+:8] == $past(wdata_i, 1)));
-          end else begin
-            assert ($stable(register[i][j*8+:8]));
-          end
-        end
-      end : slice_loop
-    end : word_loop
-  end : req_042
-
-  /*
-   * REQ-REGFILE-043:
-   * Writes to register 0 shall be silently ignored, regardless of the state of wen_i.
-   */
-
-  always_ff @(posedge clk_i) begin : req_043
-    if (past_valid && $past(rst_ni && (waddr_i == '0), 1)) begin
-      assert ($stable(register[0]));
-    end
-  end : req_043
-
-  /*
-   * REQ-REGFILE-052:
-   * The read output rdata[i] must be zero when raddr[i] is zero,
-   * regardless of any prior writes to register 0.
-   */
-
-  always_comb begin : req_052
-    if (raddr_i[0] == '0) assert (rdata[0] == '0);
-    if (raddr_i[1] == '0) assert (rdata[1] == '0);
-  end : req_052
-
-  /*
-   * REQ-REGFILE-053:
-   * Requirement REQ-REGFILE-052 shall be unconditional: it must hold at power-on
-   * without reset having been asserted, and at all times during normal operation.
-   */
-
-  logic rst_asserted;
-
-  initial assume (rst_asserted == '0);
-
-  always_ff @(posedge clk_i) begin : req_053
-    if (!rst_ni) begin
-      rst_asserted <= '1;
-    end
-
-    cover (!rst_asserted && wen_i && (waddr_i == '0));
-  end : req_053
-
-  /*
-   * REQ-REGFILE-060:
-   * The module shall not implement any bypass logic. A read and write to
-   * the same address in the same cycle shall return the value held in
-   * the register prior to the rising clock edge of the current cycle.
-   */
-
-  /* Similar to above, we will use a part-select here. */
-  always_comb begin : req_060
-    if (wen_i && raddr_i[0] != '0 && raddr_i[0] == waddr_i) begin
-      assert (rdata[0] == register[raddr_i[0]][slice_sel_i*8+:8]);
-    end
-    if (wen_i && raddr_i[1] != '0 && raddr_i[1] == waddr_i) begin
-      assert (rdata[1] == register[raddr_i[1]][slice_sel_i*8+:8]);
-    end
-  end : req_060
-
-endmodule : regfile_fv
diff --git a/verif/formal/simple_alu/README.md b/verif/formal/simple_alu/README.md
deleted file mode 100644
index 3355ced..0000000
--- a/verif/formal/simple_alu/README.md
+++ /dev/null
@@ -1,23 +0,0 @@
-# simple_alu Formal Verification
-
-Run with: `sby -f simple_alu.sby` from this directory.
-
-Reference: https://yosyshq.readthedocs.io/projects/sby/en/latest/reference.html
-
-## Mode
-
-Bounded Model Check (BMC, depth=100): proves assertions hold for the first 100 clock cycles.
-A counterexample waveform is generated on failure.
-
-Prove mode (k-induction): proves assertions hold for infinite time. Much stronger guarantee but harder to converge. Change `mode bmc` to `mode prove` in the `.sby` to use it.
-
-## Properties
-
-| Name              | Status      | Description                              |
-|-------------------|-------------|------------------------------------------|
-| `a_rst_check`     | implemented | y == 0 one cycle after reset asserts     |
-| `a_rst_overflow`  | planned     | overflow == 0 one cycle after reset      |
-| `a_add`           | planned     | y == a+b one cycle after sel=0           |
-| `a_sub`           | planned     | y == a-b one cycle after sel=1           |
-| `a_overflow_add`  | planned     | overflow correct for addition            |
-| `a_overflow_sub`  | planned     | overflow correct for subtraction         |
\ No newline at end of file
diff --git a/verif/formal/simple_alu/simple_alu.sby b/verif/formal/simple_alu/simple_alu.sby
deleted file mode 100644
index cd028d9..0000000
--- a/verif/formal/simple_alu/simple_alu.sby
+++ /dev/null
@@ -1,22 +0,0 @@
-[tasks]
-bmc
-cover
-
-[options]
-bmc: mode bmc
-cover: mode cover
-depth 100
-
-[engines]
-smtbmc
-
-[script]
-read -formal -sv simple_alu.sv
-read -formal -sv simple_alu_fv.sv
-read -formal -sv simple_alu_top_fv.sv
-prep -top simple_alu_top_fv
-
-[files]
-../../../rtl/simple_alu.sv
-simple_alu_fv.sv
-simple_alu_top_fv.sv
diff --git a/verif/formal/simple_alu/simple_alu_bind.sv b/verif/formal/simple_alu/simple_alu_bind.sv
deleted file mode 100644
index 8ed7057..0000000
--- a/verif/formal/simple_alu/simple_alu_bind.sv
+++ /dev/null
@@ -1,15 +0,0 @@
-// Bind file for simple_alu formal verification.
-// Attaches simple_alu_fv to every instance of simple_alu in the design.
-// RTL is completely unaware of this file.
-//
-// bind <dut_module> <fv_module> <instance_name> (<port_connections>);
-
-bind simple_alu simple_alu_fv u_simple_alu_fv (
-    .clk      (clk),
-    .rst      (rst),
-    .a        (a),
-    .b        (b),
-    .sel      (sel),
-    .y        (y),
-    .overflow (overflow)
-);
diff --git a/verif/formal/simple_alu/simple_alu_fv.sv b/verif/formal/simple_alu/simple_alu_fv.sv
deleted file mode 100644
index 98c05a7..0000000
--- a/verif/formal/simple_alu/simple_alu_fv.sv
+++ /dev/null
@@ -1,50 +0,0 @@
-// Formal verification module for simple_alu.
-// All ports are inputs - this module only observes DUT signals, never drives them.
-// Instantiated via simple_alu_top_fv.sv wrapper (bind unsupported in open-source Yosys).
-module simple_alu_fv (
-    input logic        clk_i,
-    input logic [31:0] a_i,
-    input logic [31:0] b_i,
-    input logic        sel_i,
-    input logic        rst_ni,
-
-    input logic [31:0] y_i,
-    input logic        overflow_i
-  );
-
-    // -------------------------------------------------------------------------
-    // Initial assumptions - constrain starting state so solver doesn't
-    // explore garbage initial register values
-    // -------------------------------------------------------------------------
-    initial assume (~rst_ni);
-    initial assume (y_i == '0);
-    initial assume (overflow_i == 1'b0);
-
-    //assertion check: if rst deasserted, y tied to 0
-    //assertions are what we want to prove, formal verification is the engine that proves it
-    // property p_rst_y;
-    //     @(posedge clk_i)
-    //     ~rst_ni |=> (y_i=='0);
-    // endproperty
-    // a_rst_y: assert property (p_rst_y)
-    //     else $error("RESET CHECK FAILED: rst_ni=%0b y_i=%0h, expected y=0", rst_ni, y_i);
-
-    // Reset check - y must be 0 one cycle after reset asserts (active low)
-    always @(posedge clk_i) begin
-        if ($past(~rst_ni)) begin
-            assert (y_i == '0);
-            assert (overflow_i == 0);
-        end
-    end
-
-    // -------------------------------------------------------------------------
-    // Cover statements - solver finds shortest path to reach each state
-    // These generate VCD traces you can inspect in GTKWave
-    // -------------------------------------------------------------------------
-
-    always @(posedge clk_i) begin
-        cover ($past(sel_i == 0) && overflow_i == 1'b1);  // addition overflow
-        cover ($past(sel_i == 1) && overflow_i == 1'b1);  // subtraction underflow
-    end
-
-endmodule
diff --git a/verif/formal/simple_alu/simple_alu_top_fv.sv b/verif/formal/simple_alu/simple_alu_top_fv.sv
deleted file mode 100644
index 8f1241c..0000000
--- a/verif/formal/simple_alu/simple_alu_top_fv.sv
+++ /dev/null
@@ -1,37 +0,0 @@
-// Wrapper top module for formal verification of simple_alu.
-// Instantiates the DUT and the checker side-by-side so the formal tool
-// sees both. Used because open-source Yosys does not support bind.
-// Note: only DUT ports are accessible here - internal signals (sum, diff)
-// cannot be tapped without bind or Verific.
-module simple_alu_top_fv (
-    input logic        clk_i,
-    input logic [31:0] a_i,
-    input logic [31:0] b_i,
-    input logic        sel_i,
-    input logic        rst_ni
-);
-    logic [31:0] y;
-    logic        overflow;
-
-    // DUT instance
-    simple_alu dut (
-        .clk_i      (clk_i),
-        .a_i        (a_i),
-        .b_i        (b_i),
-        .sel_i      (sel_i),
-        .rst_ni     (rst_ni),
-        .y_o        (y),
-        .overflow_o (overflow)
-    );
-
-    // Checker instance - observes DUT outputs
-    simple_alu_fv u_checker (
-        .clk_i      (clk_i),
-        .a_i        (a_i),
-        .b_i        (b_i),
-        .sel_i      (sel_i),
-        .rst_ni     (rst_ni),
-        .y_i        (y),
-        .overflow_i (overflow)
-    );
-endmodule