verif/formal/simple_alu/simple_alu_top_fv.sv


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29

// 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,
    input logic [31:0] a,
    input logic [31:0] b,
    input logic        sel,
    input logic        rst
);
    logic [31:0] y;
    logic        overflow;

    // DUT instance
    simple_alu dut (.*);

    // Checker instance - observes DUT outputs
    simple_alu_fv u_checker (
        .clk      (clk),
        .a        (a),
        .b        (b),
        .sel      (sel),
        .rst      (rst),
        .y        (y),
        .overflow (overflow)
    );
endmodule