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 --- dv/formal/simple_alu/simple_alu_top_fv.sv | 37 +++++++++++++++++++++++++++++++ 1 file changed, 37 insertions(+) create mode 100644 dv/formal/simple_alu/simple_alu_top_fv.sv (limited to 'dv/formal/simple_alu/simple_alu_top_fv.sv') diff --git a/dv/formal/simple_alu/simple_alu_top_fv.sv b/dv/formal/simple_alu/simple_alu_top_fv.sv new file mode 100644 index 0000000..8f1241c --- /dev/null +++ b/dv/formal/simple_alu/simple_alu_top_fv.sv @@ -0,0 +1,37 @@ +// 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