From adce21a91f4b55cad1126fa4d453b4d6eef79f7f Mon Sep 17 00:00:00 2001 From: Warrick Lo 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 --- verif/formal/simple_alu/simple_alu_top_fv.sv | 37 ---------------------------- 1 file changed, 37 deletions(-) delete mode 100644 verif/formal/simple_alu/simple_alu_top_fv.sv (limited to 'verif/formal/simple_alu/simple_alu_top_fv.sv') 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 -- cgit v1.2.3