3 files changed, 44 insertions, 37 deletions

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