Add simple_alu RTL and formal verification

  - simple_alu.sv: 32-bit ALU with add/sub, 33-bit extended overflow
    detection, and active-low synchronous reset
  - simple_alu_bind.sv: attaches checker to simple_alu without modifying RTL
  - simple_alu_top_fv.sv: replace bind (unsupported in open-source Yosys)
    with explicit wrapper that instantiates DUT and checker side-by-side
  - simple_alu_fv.sv: bind-based checker module observing DUT signals
  - simple_alu.sby: SymbiYosys config running BMC and cover tasks
  - README.md: verification plan tracking implemented and planned properties
  - .gitignore: exclude SymbiYosys output directories

1 files changed, 29 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..2292713
--- /dev/null
+++ b/verif/formal/simple_alu/simple_alu_top_fv.sv
@@ -0,0 +1,29 @@
+// 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,
+    input logic [31:0] a,
+    input logic [31:0] b,
+    input logic        sel,
+    input logic        rst
+);
+    logic [31:0] y;
+    logic        overflow;
+
+    // DUT instance
+    simple_alu dut (.*);
+
+    // Checker instance - observes DUT outputs
+    simple_alu_fv u_checker (
+        .clk      (clk),
+        .a        (a),
+        .b        (b),
+        .sel      (sel),
+        .rst      (rst),
+        .y        (y),
+        .overflow (overflow)
+    );
+endmodule