From adce21a91f4b55cad1126fa4d453b4d6eef79f7f Mon Sep 17 00:00:00 2001
From: Warrick Lo <wlo@warricklo.net>
Date: Wed, 24 Jun 2026 07:58:06 +0000
Subject: Add CI pipeline for formal verification

* Add formal verification tests with sby to CI
* Fix reviewdog having insufficient API permissions

See-also: #15
Signed-off-by: Warrick Lo <wlo@warricklo.net>
---
 verif/formal/simple_alu/simple_alu_fv.sv | 50 --------------------------------
 1 file changed, 50 deletions(-)
 delete mode 100644 verif/formal/simple_alu/simple_alu_fv.sv

(limited to 'verif/formal/simple_alu/simple_alu_fv.sv')

diff --git a/verif/formal/simple_alu/simple_alu_fv.sv b/verif/formal/simple_alu/simple_alu_fv.sv
deleted file mode 100644
index 98c05a7..0000000
--- a/verif/formal/simple_alu/simple_alu_fv.sv
+++ /dev/null
@@ -1,50 +0,0 @@
-// 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_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_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_i)
-    //     ~rst_ni |=> (y_i=='0);
-    // endproperty
-    // a_rst_y: assert property (p_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_i) begin
-        if ($past(~rst_ni)) begin
-            assert (y_i == '0);
-            assert (overflow_i == 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_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
-- 
cgit v1.2.3