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
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
|
# Single-bit $xnor
read_verilog -noopt <<EOT
module gold(input i, output o);
assign o = 1'bx ~^ i;
endmodule
EOT
select -assert-count 1 t:$xnor
copy gold coarse
copy gold fine
copy gold coarse_keepdc
copy gold fine_keepdc
cd coarse
opt_expr
select -assert-none t:$xnor
cd fine
simplemap
opt_expr
select -assert-none c:t$_XNOR_
cd
miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold coarse miter
sat -verify -prove-asserts -show-ports -enable_undef miter
miter -equiv -flatten -make_assert -make_outputs coarse fine miter2
sat -verify -prove-asserts -show-ports -enable_undef miter2
cd coarse_keepdc
opt_expr -keepdc
select -assert-count 1 c:*
cd fine_keepdc
simplemap
opt_expr -keepdc
select -assert-count 1 t:$_XNOR_
cd
miter -equiv -flatten -make_assert -make_outputs gold coarse_keepdc miter3
sat -verify -prove-asserts -show-ports -enable_undef miter3
miter -equiv -flatten -make_assert -make_outputs coarse_keepdc fine_keepdc miter4
sat -verify -prove-asserts -show-ports -enable_undef miter4
# Multi-bit $xnor
design -reset
read_verilog -noopt <<EOT
module gold(input i, output [6:0] o);
assign o = {1'bx, 1'b0, 1'b0, 1'b1, 1'bx, 1'b1, i} ~^ {7{i}};
endmodule
EOT
select -assert-count 1 t:$xnor
copy gold coarse
copy gold fine
copy gold coarse_keepdc
copy gold fine_keepdc
cd coarse
opt_expr -fine
select -assert-none t:$xnor
cd fine
simplemap
opt_expr
select -assert-none t:$_XNOR_
cd
miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold coarse miter
sat -verify -prove-asserts -show-ports -enable_undef miter
miter -equiv -flatten -make_assert -make_outputs coarse fine miter2
sat -verify -prove-asserts -show-ports -enable_undef miter2
cd coarse_keepdc
opt_expr -keepdc -fine
select -assert-count 1 t:$xnor
cd fine_keepdc
simplemap
opt_expr -keepdc
select -assert-count 0 c:$_XOR_
cd
miter -equiv -flatten -make_assert -make_outputs gold coarse_keepdc miter3
sat -verify -prove-asserts -show-ports -enable_undef miter3
miter -equiv -flatten -make_assert -make_outputs coarse_keepdc fine_keepdc miter4
sat -verify -prove-asserts -show-ports -enable_undef miter4
# Single-bit $xnor extension
design -reset
read_verilog -noopt <<EOT
module gold(input i, output [1:0] o, p, q);
assign o = i ~^ i;
assign p = 1'b0 ~^ i;
assign q = 1'b1 ~^ i;
endmodule
EOT
select -assert-count 3 t:$xnor
copy gold coarse
copy gold fine
copy gold coarse_keepdc
copy gold fine_keepdc
cd coarse
opt_expr -fine
select -assert-none t:$xnor
cd fine
simplemap
opt_expr
select -assert-none t:$_XNOR_
cd
miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold coarse miter
sat -verify -prove-asserts -show-ports -enable_undef miter
miter -equiv -flatten -make_assert -make_outputs coarse fine miter2
sat -verify -prove-asserts -show-ports -enable_undef miter2
cd coarse_keepdc
opt_expr -keepdc -fine
select -assert-count 1 t:$xnor
cd fine_keepdc
simplemap
opt_expr -keepdc
select -assert-count 0 c:$_XNOR_
cd
miter -equiv -flatten -make_assert -make_outputs gold coarse_keepdc miter3
sat -verify -prove-asserts -show-ports -enable_undef miter3
miter -equiv -flatten -make_assert -make_outputs coarse_keepdc fine_keepdc miter4
sat -verify -prove-asserts -show-ports -enable_undef miter4
|
