blob: 98c05a786658fc5de29409b947552ce0e57b7723 (
plain) (
blame)
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
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
|
// Formal verification module for simple_alu.
// All ports are inputs - this module only observes DUT signals, never drives them.
// Instantiated via simple_alu_top_fv.sv wrapper (bind unsupported in open-source Yosys).
module simple_alu_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,
input logic [31:0] y_i,
input logic overflow_i
);
// -------------------------------------------------------------------------
// Initial assumptions - constrain starting state so solver doesn't
// explore garbage initial register values
// -------------------------------------------------------------------------
initial assume (~rst_ni);
initial assume (y_i == '0);
initial assume (overflow_i == 1'b0);
//assertion check: if rst deasserted, y tied to 0
//assertions are what we want to prove, formal verification is the engine that proves it
// property p_rst_y;
// @(posedge clk_i)
// ~rst_ni |=> (y_i=='0);
// endproperty
// a_rst_y: assert property (p_rst_y)
// else $error("RESET CHECK FAILED: rst_ni=%0b y_i=%0h, expected y=0", rst_ni, y_i);
// Reset check - y must be 0 one cycle after reset asserts (active low)
always @(posedge clk_i) begin
if ($past(~rst_ni)) begin
assert (y_i == '0);
assert (overflow_i == 0);
end
end
// -------------------------------------------------------------------------
// Cover statements - solver finds shortest path to reach each state
// These generate VCD traces you can inspect in GTKWave
// -------------------------------------------------------------------------
always @(posedge clk_i) begin
cover ($past(sel_i == 0) && overflow_i == 1'b1); // addition overflow
cover ($past(sel_i == 1) && overflow_i == 1'b1); // subtraction underflow
end
endmodule
|
