Sync with 'master'

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

1 files changed, 37 insertions, 0 deletions

diff --git a/verif/formal/simple_alu/simple_alu_top_fv.sv b/verif/formal/simple_alu/simple_alu_top_fv.sv
new file mode 100644
index 0000000..8f1241c
--- /dev/null
+++ b/verif/formal/simple_alu/simple_alu_top_fv.sv
@@ -0,0 +1,37 @@
+// 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