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>

1 files changed, 0 insertions, 37 deletions

diff --git a/verif/formal/simple_alu/simple_alu_top_fv.sv b/verif/formal/simple_alu/simple_alu_top_fv.sv
deleted file mode 100644
index 8f1241c..0000000
--- a/verif/formal/simple_alu/simple_alu_top_fv.sv
+++ /dev/null
@@ -1,37 +0,0 @@
-// 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_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 (
-        .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_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