blob: ea9700a6810b01b1438d98600fc5c744fab462f3 (
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
51
|
// 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,
input logic [31:0] a,
input logic [31:0] b,
input logic sel,
input logic rst,
input logic [31:0] y,
input logic overflow
);
// -------------------------------------------------------------------------
// Initial assumptions - constrain starting state so solver doesn't
// explore garbage initial register values
// -------------------------------------------------------------------------
initial assume(~rst);
initial assume(y == '0);
initial assume(overflow == 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)
// ~rst |=> (y=='0);
// endproperty
// a_rst_y: assert property (p_rst_y)
// else $error("RESET CHECK FAILED: rst=%0b y=%0h, expected y=0", rst, y);
// Reset check - y must be 0 one cycle after reset asserts (active low)
always @(posedge clk) begin
if ( $past(~rst)) begin
assert (y == '0);
assert (overflow == 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) begin
cover ($past(sel == 0) && overflow == 1'b1); // addition overflow
cover ($past(sel == 1) && overflow == 1'b1); // subtraction underflow
end
endmodule
|
