2 * yosys -- Yosys Open SYnthesis Suite
4 * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
6 * Permission to use, copy, modify, and/or distribute this software for any
7 * purpose with or without fee is hereby granted, provided that the above
8 * copyright notice and this permission notice appear in all copies.
10 * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
11 * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
12 * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
13 * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
14 * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
15 * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
16 * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
23 #include "kernel/rtlil.h"
24 #include "kernel/sigtools.h"
25 #include "kernel/celltypes.h"
27 #ifdef YOSYS_ENABLE_MINISAT
28 # include "libs/ezsat/ezminisat.h"
29 typedef ezMiniSAT ezDefaultSAT
;
31 # include "libs/ezsat/ezsat.h"
32 typedef ezSAT ezDefaultSAT
;
38 RTLIL::Design
*design
;
42 SatGen(ezSAT
*ez
, RTLIL::Design
*design
, SigMap
*sigmap
, std::string prefix
= std::string()) :
43 ez(ez
), design(design
), sigmap(sigmap
), prefix(prefix
)
47 void setContext(RTLIL::Design
*design
, SigMap
*sigmap
, std::string prefix
= std::string())
49 this->design
= design
;
50 this->sigmap
= sigmap
;
51 this->prefix
= prefix
;
54 std::vector
<int> importSigSpec(RTLIL::SigSpec
&sig
)
56 RTLIL::SigSpec s
= sig
;
61 vec
.reserve(s
.chunks
.size());
63 for (auto &c
: s
.chunks
)
65 vec
.push_back(c
.data
.as_bool() ? ez
->TRUE
: ez
->FALSE
);
67 vec
.push_back(ez
->literal(prefix
+ stringf(c
.wire
->width
== 1 ?
68 "%s" : "%s [%d]", RTLIL::id2cstr(c
.wire
->name
), c
.offset
)));
72 void extendSignalWidth(std::vector
<int> &vec_a
, std::vector
<int> &vec_b
, RTLIL::Cell
*cell
)
74 bool is_signed_a
= false, is_signed_b
= false;
75 if (cell
->parameters
.count("\\A_SIGNED") > 0)
76 is_signed_a
= cell
->parameters
["\\A_SIGNED"].as_bool();
77 if (cell
->parameters
.count("\\B_SIGNED") > 0)
78 is_signed_b
= cell
->parameters
["\\B_SIGNED"].as_bool();
79 while (vec_a
.size() < vec_b
.size())
80 vec_a
.push_back(is_signed_a
&& vec_a
.size() > 0 ? vec_a
.back() : ez
->FALSE
);
81 while (vec_b
.size() < vec_a
.size())
82 vec_b
.push_back(is_signed_b
&& vec_b
.size() > 0 ? vec_b
.back() : ez
->FALSE
);
85 void extendSignalWidth(std::vector
<int> &vec_a
, std::vector
<int> &vec_b
, std::vector
<int> &vec_y
, RTLIL::Cell
*cell
)
87 extendSignalWidth(vec_a
, vec_b
, cell
);
88 while (vec_y
.size() < vec_a
.size())
89 vec_y
.push_back(ez
->literal());
92 bool importCell(RTLIL::Cell
*cell
)
94 if (cell
->type
== "$_AND_" || cell
->type
== "$_OR_" || cell
->type
== "$_XOR_" ||
95 cell
->type
== "$and" || cell
->type
== "$or" || cell
->type
== "$xor" || cell
->type
== "$xnor" ||
96 cell
->type
== "$add" || cell
->type
== "$sub") {
97 std::vector
<int> a
= importSigSpec(cell
->connections
.at("\\A"));
98 std::vector
<int> b
= importSigSpec(cell
->connections
.at("\\B"));
99 std::vector
<int> y
= importSigSpec(cell
->connections
.at("\\Y"));
100 extendSignalWidth(a
, b
, y
, cell
);
101 if (cell
->type
== "$and" || cell
->type
== "$_AND_")
102 ez
->assume(ez
->vec_eq(ez
->vec_and(a
, b
), y
));
103 if (cell
->type
== "$or" || cell
->type
== "$_OR_")
104 ez
->assume(ez
->vec_eq(ez
->vec_or(a
, b
), y
));
105 if (cell
->type
== "$xor" || cell
->type
== "$_XOR")
106 ez
->assume(ez
->vec_eq(ez
->vec_xor(a
, b
), y
));
107 if (cell
->type
== "$xnor")
108 ez
->assume(ez
->vec_eq(ez
->vec_not(ez
->vec_xor(a
, b
)), y
));
109 if (cell
->type
== "$add")
110 ez
->assume(ez
->vec_eq(ez
->vec_add(a
, b
), y
));
111 if (cell
->type
== "$sub")
112 ez
->assume(ez
->vec_eq(ez
->vec_sub(a
, b
), y
));
116 if (cell
->type
== "$_INV_" || cell
->type
== "$not") {
117 std::vector
<int> a
= importSigSpec(cell
->connections
.at("\\A"));
118 std::vector
<int> y
= importSigSpec(cell
->connections
.at("\\Y"));
119 ez
->assume(ez
->vec_eq(ez
->vec_not(a
), y
));
123 if (cell
->type
== "$_MUX_" || cell
->type
== "$mux") {
124 std::vector
<int> a
= importSigSpec(cell
->connections
.at("\\A"));
125 std::vector
<int> b
= importSigSpec(cell
->connections
.at("\\B"));
126 std::vector
<int> s
= importSigSpec(cell
->connections
.at("\\S"));
127 std::vector
<int> y
= importSigSpec(cell
->connections
.at("\\Y"));
128 ez
->assume(ez
->vec_eq(ez
->vec_ite(s
.at(0), b
, a
), y
));
132 if (cell
->type
== "$pmux" || cell
->type
== "$safe_pmux") {
133 std::vector
<int> a
= importSigSpec(cell
->connections
.at("\\A"));
134 std::vector
<int> b
= importSigSpec(cell
->connections
.at("\\B"));
135 std::vector
<int> s
= importSigSpec(cell
->connections
.at("\\S"));
136 std::vector
<int> y
= importSigSpec(cell
->connections
.at("\\Y"));
137 std::vector
<int> tmp
= a
;
138 for (size_t i
= 0; i
< s
.size(); i
++) {
139 std::vector
<int> part_of_b(b
.begin()+i
*a
.size(), b
.begin()+(i
+1)*a
.size());
140 tmp
= ez
->vec_ite(s
.at(i
), part_of_b
, tmp
);
142 if (cell
->type
== "$safe_pmux")
143 tmp
= ez
->vec_ite(ez
->onehot(s
, true), tmp
, a
);
144 ez
->assume(ez
->vec_eq(tmp
, y
));
148 if (cell
->type
== "$pos" || cell
->type
== "$neg") {
149 std::vector
<int> a
= importSigSpec(cell
->connections
.at("\\A"));
150 std::vector
<int> y
= importSigSpec(cell
->connections
.at("\\Y"));
151 if (cell
->type
== "$pos") {
152 ez
->assume(ez
->vec_eq(a
, y
));
154 std::vector
<int> zero(a
.size(), ez
->FALSE
);
155 ez
->assume(ez
->vec_eq(ez
->vec_sub(zero
, a
), y
));
160 if (cell
->type
== "$reduce_and" || cell
->type
== "$reduce_or" || cell
->type
== "$reduce_xor" ||
161 cell
->type
== "$reduce_xnor" || cell
->type
== "$reduce_bool" || cell
->type
== "$logic_not") {
162 std::vector
<int> a
= importSigSpec(cell
->connections
.at("\\A"));
163 std::vector
<int> y
= importSigSpec(cell
->connections
.at("\\Y"));
164 if (cell
->type
== "$reduce_and")
165 ez
->SET(ez
->expression(ez
->OpAnd
, a
), y
.at(0));
166 if (cell
->type
== "$reduce_or" || cell
->type
== "$reduce_bool")
167 ez
->SET(ez
->expression(ez
->OpOr
, a
), y
.at(0));
168 if (cell
->type
== "$reduce_xor")
169 ez
->SET(ez
->expression(ez
->OpXor
, a
), y
.at(0));
170 if (cell
->type
== "$reduce_xnor")
171 ez
->SET(ez
->NOT(ez
->expression(ez
->OpXor
, a
)), y
.at(0));
172 if (cell
->type
== "$logic_not")
173 ez
->SET(ez
->NOT(ez
->expression(ez
->OpOr
, a
)), y
.at(0));
174 for (size_t i
= 1; i
< y
.size(); i
++)
179 if (cell
->type
== "$logic_and" || cell
->type
== "$logic_or") {
180 int a
= ez
->expression(ez
->OpOr
, importSigSpec(cell
->connections
.at("\\A")));
181 int b
= ez
->expression(ez
->OpOr
, importSigSpec(cell
->connections
.at("\\B")));
182 std::vector
<int> y
= importSigSpec(cell
->connections
.at("\\Y"));
183 if (cell
->type
== "$logic_and")
184 ez
->SET(ez
->expression(ez
->OpAnd
, a
, b
), y
.at(0));
186 ez
->SET(ez
->expression(ez
->OpOr
, a
, b
), y
.at(0));
187 for (size_t i
= 1; i
< y
.size(); i
++)
192 if (cell
->type
== "$lt" || cell
->type
== "$le" || cell
->type
== "$eq" || cell
->type
== "$ne" || cell
->type
== "$ge" || cell
->type
== "$gt") {
193 bool is_signed
= cell
->parameters
["\\A_SIGNED"].as_bool() && cell
->parameters
["\\B_SIGNED"].as_bool();
194 std::vector
<int> a
= importSigSpec(cell
->connections
.at("\\A"));
195 std::vector
<int> b
= importSigSpec(cell
->connections
.at("\\B"));
196 std::vector
<int> y
= importSigSpec(cell
->connections
.at("\\Y"));
197 extendSignalWidth(a
, b
, cell
);
198 if (cell
->type
== "$lt")
199 ez
->SET(is_signed
? ez
->vec_lt_signed(a
, b
) : ez
->vec_lt_unsigned(a
, b
), y
.at(0));
200 if (cell
->type
== "$le")
201 ez
->SET(is_signed
? ez
->vec_le_signed(a
, b
) : ez
->vec_le_unsigned(a
, b
), y
.at(0));
202 if (cell
->type
== "$eq")
203 ez
->SET(ez
->vec_eq(a
, b
), y
.at(0));
204 if (cell
->type
== "$ne")
205 ez
->SET(ez
->vec_ne(a
, b
), y
.at(0));
206 if (cell
->type
== "$ge")
207 ez
->SET(is_signed
? ez
->vec_ge_signed(a
, b
) : ez
->vec_ge_unsigned(a
, b
), y
.at(0));
208 if (cell
->type
== "$gt")
209 ez
->SET(is_signed
? ez
->vec_gt_signed(a
, b
) : ez
->vec_gt_unsigned(a
, b
), y
.at(0));
210 for (size_t i
= 1; i
< y
.size(); i
++)
215 if (cell
->type
== "$shl" || cell
->type
== "$shr" || cell
->type
== "$sshl" || cell
->type
== "$sshr") {
216 std::vector
<int> a
= importSigSpec(cell
->connections
.at("\\A"));
217 std::vector
<int> b
= importSigSpec(cell
->connections
.at("\\B"));
218 std::vector
<int> y
= importSigSpec(cell
->connections
.at("\\Y"));
219 char shift_left
= cell
->type
== "$shl" || cell
->type
== "$sshl";
220 bool sign_extend
= cell
->type
== "$sshr";
221 while (y
.size() < a
.size())
222 y
.push_back(ez
->literal());
223 std::vector
<int> tmp
= a
;
224 for (size_t i
= 0; i
< b
.size(); i
++)
226 std::vector
<int> tmp_shifted(tmp
.size());
227 for (size_t j
= 0; j
< tmp
.size(); j
++) {
228 int idx
= j
+ (1 << i
) * (shift_left
? -1 : +1);
229 tmp_shifted
.at(j
) = (0 <= idx
&& idx
< int(tmp
.size())) ? tmp
.at(idx
) : sign_extend
? tmp
.back() : ez
->FALSE
;
231 tmp
= ez
->vec_ite(b
.at(i
), tmp_shifted
, tmp
);
233 ez
->assume(ez
->vec_eq(tmp
, y
));
237 // Unsupported internal cell types: $mul $div $mod $pow