Skip to content

Commit 943b058

Browse files
mattvennmattvenn
committed
add formal
1 parent ef45d18 commit 943b058

File tree

6 files changed

+300
-0
lines changed

6 files changed

+300
-0
lines changed

‎formal/README.md

+14
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
# Formal Verification of the basic mux
2+
3+
Run
4+
5+
sby -f config.sby
6+
7+
To make a proof that the ins, outs and bidirectionals are all connected correctly.
8+
9+
## Setup
10+
11+
* config.sby lists all the files needed for the verification.
12+
* tt_top_formal.v instantiates tt_top.v and loops back the outputs and inputs
13+
* tt_um_formal.v is a user project that asserts that when its enabled, the inputs are driven by the outputs
14+
* p_wrapper.v is a replacement for p00, p01, p02, p03_wrapper.v that just instantiates tt_um_formal for each design

‎formal/config.sby

+24
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
[options]
2+
multiclock on
3+
mode prove
4+
# mode cover
5+
depth 10
6+
7+
[engines]
8+
smtbmc
9+
10+
[script]
11+
read -noverific
12+
read -sv sg13g2_io.v tt_top.v basic_mux.v counter.v p_wrappers.v tt_um_formal.v tt_top_formal.v
13+
14+
# convert tribuf to logic
15+
prep -top tt_top_formal; flatten #; tribuf -logic
16+
17+
[files]
18+
../IHP-Open-PDK/ihp-sg13g2/libs.ref/sg13g2_io/verilog/sg13g2_io.v
19+
../designs/src/tt-chip/tt_top.v
20+
../designs/src/tt-chip/basic_mux.v
21+
../designs/src/tt-chip/counter.v
22+
p_wrappers.v
23+
tt_um_formal.v
24+
tt_top_formal.v

‎formal/formal.gtkw

+88
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,88 @@
1+
[*]
2+
[*] GTKWave Analyzer v3.4.0 (w)1999-2022 BSI
3+
[*] Wed Jul 24 13:38:14 2024
4+
[*]
5+
[dumpfile] "/home/matt/work/asic-workshop/shuttle-tt08/tinytapeout-ihp-0p1/formal/config/engine_0/trace0.vcd"
6+
[dumpfile_mtime] "Wed Jul 24 13:37:13 2024"
7+
[dumpfile_size] 13126
8+
[savefile] "/home/matt/work/asic-workshop/shuttle-tt08/tinytapeout-ihp-0p1/formal/formal.gtkw"
9+
[timestart] 0
10+
[size] 2124 977
11+
[pos] -1 -1
12+
*-2.866297 4 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1
13+
[treeopen] tt_top_formal.
14+
[treeopen] tt_top_formal.tt_top.
15+
[treeopen] tt_top_formal.tt_top.mux_I.
16+
[treeopen] tt_top_formal.tt_top.mux_I.p00_I.
17+
[treeopen] tt_top_formal.tt_top.mux_I.p00_I.p_wrapper.
18+
[treeopen] tt_top_formal.tt_top.mux_I.p03_I.
19+
[treeopen] tt_top_formal.tt_top.mux_I.p03_I.p_wrapper.
20+
[sst_width] 333
21+
[signals_width] 534
22+
[sst_expanded] 1
23+
[sst_vpaned_height] 288
24+
@28
25+
tt_top_formal.clk
26+
@22
27+
tt_top_formal.tt_top.counter_I.addr[4:0]
28+
@28
29+
tt_top_formal.ctrl_ena
30+
tt_top_formal.ctrl_sel_inc
31+
tt_top_formal.ctrl_sel_rst_n
32+
tt_top_formal.loopback_in
33+
tt_top_formal.loopback_out
34+
tt_top_formal.rst_n
35+
@22
36+
tt_top_formal.ui_in[7:0]
37+
tt_top_formal.uio[7:0]
38+
tt_top_formal.uo_out[7:0]
39+
@800200
40+
-bidirs
41+
@22
42+
tt_top_formal.tt_top.uio_in[7:0]
43+
tt_top_formal.tt_top.uio_oe[7:0]
44+
tt_top_formal.tt_top.uio_out[7:0]
45+
@1000200
46+
-bidirs
47+
@800201
48+
-wrapper1
49+
@29
50+
tt_top_formal.tt_top.mux_I.p00_I.ena
51+
@23
52+
tt_top_formal.tt_top.mux_I.p00_I.p_wrapper.tt_um_formal.ui_in[7:0]
53+
tt_top_formal.tt_top.mux_I.p00_I.p_wrapper.tt_um_formal.uio_in[7:0]
54+
tt_top_formal.tt_top.mux_I.p00_I.p_wrapper.tt_um_formal.uio_oe[7:0]
55+
tt_top_formal.tt_top.mux_I.p00_I.p_wrapper.tt_um_formal.uio_out[7:0]
56+
tt_top_formal.tt_top.mux_I.p00_I.p_wrapper.tt_um_formal.uo_out[7:0]
57+
@1000201
58+
-wrapper1
59+
@28
60+
tt_top_formal.tt_top.mux_I.p01_I.ena
61+
tt_top_formal.tt_top.mux_I.p02_I.ena
62+
@800200
63+
-wrapper4
64+
@28
65+
tt_top_formal.tt_top.mux_I.p03_I.ena
66+
@22
67+
tt_top_formal.tt_top.mux_I.p03_I.p_wrapper.tt_um_formal.ui_in[7:0]
68+
tt_top_formal.tt_top.mux_I.p03_I.p_wrapper.tt_um_formal.uio_in[7:0]
69+
@c00022
70+
tt_top_formal.tt_top.mux_I.p03_I.p_wrapper.tt_um_formal.uio_oe[7:0]
71+
@28
72+
(0)tt_top_formal.tt_top.mux_I.p03_I.p_wrapper.tt_um_formal.uio_oe[7:0]
73+
(1)tt_top_formal.tt_top.mux_I.p03_I.p_wrapper.tt_um_formal.uio_oe[7:0]
74+
(2)tt_top_formal.tt_top.mux_I.p03_I.p_wrapper.tt_um_formal.uio_oe[7:0]
75+
(3)tt_top_formal.tt_top.mux_I.p03_I.p_wrapper.tt_um_formal.uio_oe[7:0]
76+
(4)tt_top_formal.tt_top.mux_I.p03_I.p_wrapper.tt_um_formal.uio_oe[7:0]
77+
(5)tt_top_formal.tt_top.mux_I.p03_I.p_wrapper.tt_um_formal.uio_oe[7:0]
78+
(6)tt_top_formal.tt_top.mux_I.p03_I.p_wrapper.tt_um_formal.uio_oe[7:0]
79+
(7)tt_top_formal.tt_top.mux_I.p03_I.p_wrapper.tt_um_formal.uio_oe[7:0]
80+
@1401200
81+
-group_end
82+
@22
83+
tt_top_formal.tt_top.mux_I.p03_I.p_wrapper.tt_um_formal.uio_out[7:0]
84+
tt_top_formal.tt_top.mux_I.p03_I.p_wrapper.tt_um_formal.uo_out[7:0]
85+
@1000200
86+
-wrapper4
87+
[pattern_trace] 1
88+
[pattern_trace] 0

‎formal/p_wrappers.v

+87
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,87 @@
1+
`default_nettype none
2+
3+
module p00_wrapper (
4+
input wire ena,
5+
input wire [17:0] iw,
6+
output wire [23:0] ow
7+
);
8+
9+
p_wrapper p_wrapper(
10+
.ena(ena),
11+
.iw(iw),
12+
.ow(ow)
13+
);
14+
15+
endmodule
16+
17+
module p01_wrapper (
18+
input wire ena,
19+
input wire [17:0] iw,
20+
output wire [23:0] ow
21+
);
22+
23+
p_wrapper p_wrapper(
24+
.ena(ena),
25+
.iw(iw),
26+
.ow(ow)
27+
);
28+
29+
endmodule
30+
31+
module p02_wrapper (
32+
input wire ena,
33+
input wire [17:0] iw,
34+
output wire [23:0] ow
35+
);
36+
37+
p_wrapper p_wrapper(
38+
.ena(ena),
39+
.iw(iw),
40+
.ow(ow)
41+
);
42+
43+
endmodule
44+
45+
module p03_wrapper (
46+
input wire ena,
47+
input wire [17:0] iw,
48+
output wire [23:0] ow
49+
);
50+
51+
p_wrapper p_wrapper(
52+
.ena(ena),
53+
.iw(iw),
54+
.ow(ow)
55+
);
56+
57+
endmodule
58+
59+
module p_wrapper (
60+
input wire ena,
61+
input wire [17:0] iw,
62+
output wire [23:0] ow
63+
);
64+
65+
wire [7:0] uio_in;
66+
wire [7:0] uio_out;
67+
wire [7:0] uio_oe;
68+
wire [7:0] uo_out;
69+
wire [7:0] ui_in;
70+
wire clk;
71+
wire rst_n;
72+
73+
assign { uio_in, ui_in, rst_n, clk} = iw;
74+
assign ow = { uio_oe, uio_out, uo_out };
75+
76+
tt_um_formal tt_um_formal (
77+
.uio_in (uio_in),
78+
.uio_out (uio_out),
79+
.uio_oe (uio_oe),
80+
.uo_out (uo_out),
81+
.ui_in (ui_in),
82+
.ena (ena),
83+
.clk (clk),
84+
.rst_n (rst_n)
85+
);
86+
87+
endmodule

‎formal/tt_top_formal.v

+39
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,39 @@
1+
2+
module tt_top_formal ();
3+
4+
wire ctrl_sel_rst_n;
5+
wire ctrl_sel_inc;
6+
wire ctrl_ena;
7+
wire [7:0] ui_in;
8+
wire [7:0] uo_out;
9+
wire [7:0] uio;
10+
wire clk;
11+
wire rst_n;
12+
wire loopback_in;
13+
wire loopback_out;
14+
wire unused;
15+
16+
tt_top tt_top(
17+
.ctrl_sel_rst_n_PAD(ctrl_sel_rst_n),
18+
.ctrl_sel_inc_PAD(ctrl_sel_inc),
19+
.ctrl_ena_PAD(ctrl_ena),
20+
.ui_in_PAD(ui_in),
21+
.uo_out_PAD(uo_out),
22+
.uio_PAD(uio),
23+
.clk_PAD(clk),
24+
.rst_n_PAD(rst_n),
25+
.loopback_in_PAD(loopback_in),
26+
.loopback_out_PAD(loopback_out),
27+
.unused_PAD(unused),
28+
);
29+
30+
// loopback the output to the input
31+
assign ui_in = uo_out;
32+
// loopback the bidirectionals, if they're set as output
33+
assign tt_top.uio_in = tt_top.uio_out & tt_top.uio_oe;
34+
35+
// only useful for cover
36+
initial assume(rst_n == 0);
37+
initial assume(ctrl_sel_rst_n == 0);
38+
39+
endmodule

‎formal/tt_um_formal.v

+48
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,48 @@
1+
/*
2+
* tt_um_formal.v
3+
*
4+
* User module for formal connectivity proof
5+
*
6+
* Author: Matt Venn <[email protected]>
7+
*/
8+
9+
`default_nettype none
10+
11+
module tt_um_formal (
12+
input wire [7:0] ui_in, // Dedicated inputs
13+
output wire [7:0] uo_out, // Dedicated outputs
14+
input wire [7:0] uio_in, // IOs: Input path
15+
output wire [7:0] uio_out, // IOs: Output path
16+
output wire [7:0] uio_oe, // IOs: Enable path (active high: 0=input, 1=output)
17+
input wire ena,
18+
input wire clk,
19+
input wire rst_n
20+
);
21+
22+
// let solver drive the outputs
23+
rand reg [7:0] anyseq1; assign uo_out = anyseq1;
24+
// bidirectional outputs
25+
rand reg [7:0] anyseq2; assign uio_out = anyseq2;
26+
// bidirectional enables
27+
rand reg [7:0] anyseq3; assign uio_oe = anyseq3;
28+
29+
always @(*) begin
30+
if(ena) begin
31+
// if design is enabled, looped back inputs must = outputs
32+
assert(ui_in == uo_out);
33+
// bidirectional outputs, only should match if oe is set
34+
assert(uio_in == (uio_out & uio_oe));
35+
cover(ui_in == 8'hAA);
36+
cover(uio_in == 8'hAA);
37+
end else begin
38+
// otherwise inputs must be 0
39+
assert(ui_in == 0);
40+
// design is in reset
41+
assert(rst_n == 0);
42+
// no clock
43+
assert(clk == 0);
44+
end
45+
end
46+
47+
endmodule // tt_um_formal
48+

0 commit comments

Comments
 (0)