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
---
 verif/formal/simple_alu/README.md            | 23 +++++++++++++
 verif/formal/simple_alu/simple_alu.sby       | 22 ++++++++++++
 verif/formal/simple_alu/simple_alu_bind.sv   | 15 ++++++++
 verif/formal/simple_alu/simple_alu_fv.sv     | 51 ++++++++++++++++++++++++++++
 verif/formal/simple_alu/simple_alu_top_fv.sv | 29 ++++++++++++++++
 verif/uvm/env.sv                             |  0
 6 files changed, 140 insertions(+)
 create mode 100644 verif/formal/simple_alu/README.md
 create mode 100644 verif/formal/simple_alu/simple_alu.sby
 create mode 100644 verif/formal/simple_alu/simple_alu_bind.sv
 create mode 100644 verif/formal/simple_alu/simple_alu_fv.sv
 create mode 100644 verif/formal/simple_alu/simple_alu_top_fv.sv
 create mode 100644 verif/uvm/env.sv

(limited to 'verif')

diff --git a/verif/formal/simple_alu/README.md b/verif/formal/simple_alu/README.md
new file mode 100644
index 0000000..3355ced
--- /dev/null
+++ b/verif/formal/simple_alu/README.md
@@ -0,0 +1,23 @@
+# 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
new file mode 100644
index 0000000..cd028d9
--- /dev/null
+++ b/verif/formal/simple_alu/simple_alu.sby
@@ -0,0 +1,22 @@
+[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
new file mode 100644
index 0000000..b12e0eb
--- /dev/null
+++ b/verif/formal/simple_alu/simple_alu_bind.sv
@@ -0,0 +1,15 @@
+// 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)
+);
\ No newline at end of file
diff --git a/verif/formal/simple_alu/simple_alu_fv.sv b/verif/formal/simple_alu/simple_alu_fv.sv
new file mode 100644
index 0000000..ea9700a
--- /dev/null
+++ b/verif/formal/simple_alu/simple_alu_fv.sv
@@ -0,0 +1,51 @@
+// 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,
+    input logic [31:0] a,
+    input logic [31:0] b,
+    input logic        sel,
+    input logic        rst,
+
+    input logic [31:0] y,
+    input logic        overflow
+  );
+
+    // -------------------------------------------------------------------------
+    // Initial assumptions - constrain starting state so solver doesn't
+    // explore garbage initial register values
+    // -------------------------------------------------------------------------
+    initial assume(~rst);
+    initial assume(y == '0);
+    initial assume(overflow == 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)
+    //     ~rst |=> (y=='0);      
+    // endproperty
+    // a_rst_y: assert property (p_rst_y)
+    //     else $error("RESET CHECK FAILED: rst=%0b y=%0h, expected y=0", rst, y);
+
+    // Reset check - y must be 0 one cycle after reset asserts (active low)
+    always @(posedge clk) begin
+        if ( $past(~rst)) begin
+            assert (y == '0);
+            assert (overflow == 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) begin      
+        cover ($past(sel == 0) && overflow == 1'b1);  // addition overflow
+        cover ($past(sel == 1) && overflow == 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
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
diff --git a/verif/uvm/env.sv b/verif/uvm/env.sv
new file mode 100644
index 0000000..e69de29
-- 
cgit v1.2.3


From 429dd4fa609a5b8c71f8cd6ae6f8d74fd59f2280 Mon Sep 17 00:00:00 2001
From: Chat <63841542+chatrajaman3@users.noreply.github.com>
Date: Tue, 19 May 2026 01:31:06 -0700
Subject: Pass linter

  - simple_alu.sv: rename ports with suffixes (clk_i, rst_ni, a_i, b_i,
    sel_i, y_o, overflow_o); add default case to sel case statement;
    add y_next and overflow_next combinational signals; simplify
    always_ff to only register y_next and overflow_next
  - simple_alu_fv.sv: rename ports to match RTL (clk_i, rst_ni, a_i, b_i,
    sel_i, y_i, overflow_i); remove trailing spaces
  - simple_alu_top_fv.sv: rename ports; replace .* with explicit
    connections to match updated port names
  - simple_alu_bind.sv: add missing posix newline at EOF
---
 rtl/simple_alu.sv                            | 64 +++++++++++++++++-----------
 verif/formal/simple_alu/simple_alu_bind.sv   |  2 +-
 verif/formal/simple_alu/simple_alu_fv.sv     | 45 ++++++++++---------
 verif/formal/simple_alu/simple_alu_top_fv.sv | 34 +++++++++------
 4 files changed, 83 insertions(+), 62 deletions(-)

(limited to 'verif')

diff --git a/rtl/simple_alu.sv b/rtl/simple_alu.sv
index 8dc0586..a5ae9e7 100644
--- a/rtl/simple_alu.sv
+++ b/rtl/simple_alu.sv
@@ -4,41 +4,55 @@
 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
+    input logic        clk_i,
+    input logic [31:0] a_i,
+    input logic [31:0] b_i,
+    input logic        sel_i,         //sel = 0 -> ADD, sel = 1 -> SUB
+    input logic        rst_ni,        //active LOW sync reset
 
     //outputs
-    output logic [31:0] y,
-    output logic        overflow
+    output logic [31:0] y_o,
+    output logic        overflow_o
 );
 
     logic [32:0] sum;
     logic [32:0] diff;
+    logic [31:0] y_r;
+    logic        overflow_r;
+    logic [31:0] y_next;
+    logic        overflow_next;
 
     always_comb begin
-        sum  = {1'b0, a} + {1'b0, b};
-        diff = {1'b0, a} - {1'b0, b};
-    end
+        sum  = {1'b0, a_i} + {1'b0, b_i};
+        diff = {1'b0, a_i} - {1'b0, b_i};
 
-    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];
+        y_next        = '0;
+        overflow_next = '0;
+
+        if (rst_ni) begin
+            case (sel_i)
+                0: begin
+                    y_next        = sum[31:0];
+                    overflow_next = sum[32];
+                end
+                1: begin
+                    y_next        = diff[31:0];
+                    overflow_next = diff[32];
+                end
+                default: begin
+                    y_next        = '0;
+                    overflow_next = '0;
+                end
+            endcase
         end
-        endcase
     end
+
+    always_ff @(posedge clk_i) begin
+        y_r        <= y_next;
+        overflow_r <= overflow_next;
     end
+
+    assign y_o        = y_r;
+    assign overflow_o = overflow_r;
+
 endmodule
diff --git a/verif/formal/simple_alu/simple_alu_bind.sv b/verif/formal/simple_alu/simple_alu_bind.sv
index b12e0eb..8ed7057 100644
--- a/verif/formal/simple_alu/simple_alu_bind.sv
+++ b/verif/formal/simple_alu/simple_alu_bind.sv
@@ -12,4 +12,4 @@ bind simple_alu simple_alu_fv u_simple_alu_fv (
     .sel      (sel),
     .y        (y),
     .overflow (overflow)
-);
\ No newline at end of file
+);
diff --git a/verif/formal/simple_alu/simple_alu_fv.sv b/verif/formal/simple_alu/simple_alu_fv.sv
index ea9700a..98c05a7 100644
--- a/verif/formal/simple_alu/simple_alu_fv.sv
+++ b/verif/formal/simple_alu/simple_alu_fv.sv
@@ -2,38 +2,38 @@
 // 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,
-    input logic [31:0] a,
-    input logic [31:0] b,
-    input logic        sel,
-    input logic        rst,
-
-    input logic [31:0] y,
-    input logic        overflow
+    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);
-    initial assume(y == '0);
-    initial assume(overflow == 1'b0);
+    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)
-    //     ~rst |=> (y=='0);      
+    // 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=%0b y=%0h, expected y=0", 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) begin
-        if ( $past(~rst)) begin
-            assert (y == '0);
-            assert (overflow == 0);
+    always @(posedge clk_i) begin
+        if ($past(~rst_ni)) begin
+            assert (y_i == '0);
+            assert (overflow_i == 0);
         end
     end
 
@@ -42,10 +42,9 @@ module simple_alu_fv (
     // These generate VCD traces you can inspect in GTKWave
     // -------------------------------------------------------------------------
 
-    always @(posedge clk) begin      
-        cover ($past(sel == 0) && overflow == 1'b1);  // addition overflow
-        cover ($past(sel == 1) && overflow == 1'b1);  // subtraction underflow  
+    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
index 2292713..8f1241c 100644
--- a/verif/formal/simple_alu/simple_alu_top_fv.sv
+++ b/verif/formal/simple_alu/simple_alu_top_fv.sv
@@ -4,26 +4,34 @@
 // 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
+    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 (.*);
+    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      (clk),
-        .a        (a),
-        .b        (b),
-        .sel      (sel),
-        .rst      (rst),
-        .y        (y),
-        .overflow (overflow)
+        .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
-- 
cgit v1.2.3