aboutsummaryrefslogtreecommitdiff
path: root/verif/formal/simple_alu/simple_alu_top_fv.sv
diff options
context:
space:
mode:
authorWarrick Lo <wlo@warricklo.net>2026-07-07 06:01:17 +0000
committerWarrick Lo <wlo@warricklo.net>2026-07-07 06:01:17 +0000
commit6c24f49f3239c79173fd180d065f8f03cfaeabfd (patch)
tree4ac1ebc964784b655cda35de979331196b19a3c2 /verif/formal/simple_alu/simple_alu_top_fv.sv
parentMerge branch 'feature/fu' from MyDariell (diff)
parentAdd DCO [skip ci] (diff)
downloadmontreal-feature/fu.tar.xz
montreal-feature/fu.zip
Sync with 'master'feature/fu
Signed-off-by: Warrick Lo <wlo@warricklo.net>
Diffstat (limited to 'verif/formal/simple_alu/simple_alu_top_fv.sv')
-rw-r--r--verif/formal/simple_alu/simple_alu_top_fv.sv37
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