From 1fcb70209582fd05c03919b31502deb2b7af472a Mon Sep 17 00:00:00 2001
From: Chat <63841542+ChillZero@users.noreply.github.com>
Date: Thu, 14 May 2026 19:58:51 -0700
Subject: 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
---
 rtl/simple_alu.sv | 44 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 44 insertions(+)
 create mode 100644 rtl/simple_alu.sv

(limited to 'rtl/simple_alu.sv')

diff --git a/rtl/simple_alu.sv b/rtl/simple_alu.sv
new file mode 100644
index 0000000..8dc0586
--- /dev/null
+++ b/rtl/simple_alu.sv
@@ -0,0 +1,44 @@
+// Simple 32-bit ALU supporting addition and subtraction (sel=0/1).
+// Outputs are registered. Overflow/underflow detected via 33-bit extended arithmetic.
+// Active-low synchronous reset. Used as a sandbox for formal verification.
+module simple_alu (
+
+    //inputs
+    input logic        clk,
+    input logic [31:0] a,
+    input logic [31:0] b,
+    input logic        sel,         //sel = 0 -> ADD, sel = 1 -> SUB
+    input logic        rst,         //active LOW sync reset
+
+    //outputs
+    output logic [31:0] y,
+    output logic        overflow
+);
+
+    logic [32:0] sum;
+    logic [32:0] diff;
+
+    always_comb begin
+        sum  = {1'b0, a} + {1'b0, b};
+        diff = {1'b0, a} - {1'b0, b};
+    end
+
+    always_ff @(posedge clk) begin
+    if (~rst) begin
+        y <= '0;
+        overflow <= '0;
+    end
+    else begin
+        case (sel)
+        0:  begin
+                y <= sum[31:0];
+                overflow <= sum[32];
+        end
+        1:  begin
+                y <= diff[31:0];
+                overflow <= diff[32];
+        end
+        endcase
+    end
+    end
+endmodule
-- 
cgit v1.2.3