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
;
41 SigPool initial_state
;
43 SatGen(ezSAT
*ez
, RTLIL::Design
*design
, SigMap
*sigmap
, std::string prefix
= std::string()) :
44 ez(ez
), design(design
), sigmap(sigmap
), prefix(prefix
)
48 void setContext(RTLIL::Design
*design
, SigMap
*sigmap
, std::string prefix
= std::string())
50 this->design
= design
;
51 this->sigmap
= sigmap
;
52 this->prefix
= prefix
;
55 std::vector
<int> importSigSpec(RTLIL::SigSpec
&sig
, int timestep
= -1)
57 assert(timestep
< 0 || timestep
> 0);
58 RTLIL::SigSpec s
= sig
;
63 vec
.reserve(s
.chunks
.size());
65 for (auto &c
: s
.chunks
)
67 vec
.push_back(c
.data
.as_bool() ? ez
->TRUE
: ez
->FALSE
);
69 std::string name
= prefix
;
70 name
+= timestep
== -1 ? "" : stringf("@%d:", timestep
);
71 name
+= stringf(c
.wire
->width
== 1 ? "%s" : "%s [%d]", RTLIL::id2cstr(c
.wire
->name
), c
.offset
);
72 vec
.push_back(ez
->literal(name
));
77 void extendSignalWidth(std::vector
<int> &vec_a
, std::vector
<int> &vec_b
, RTLIL::Cell
*cell
, size_t y_width
= 0)
79 bool is_signed_a
= false, is_signed_b
= false;
80 if (cell
->parameters
.count("\\A_SIGNED") > 0)
81 is_signed_a
= cell
->parameters
["\\A_SIGNED"].as_bool();
82 if (cell
->parameters
.count("\\B_SIGNED") > 0)
83 is_signed_b
= cell
->parameters
["\\B_SIGNED"].as_bool();
84 while (vec_a
.size() < vec_b
.size() || vec_a
.size() < y_width
)
85 vec_a
.push_back(is_signed_a
&& vec_a
.size() > 0 ? vec_a
.back() : ez
->FALSE
);
86 while (vec_b
.size() < vec_a
.size() || vec_b
.size() < y_width
)
87 vec_b
.push_back(is_signed_b
&& vec_b
.size() > 0 ? vec_b
.back() : ez
->FALSE
);
90 void extendSignalWidth(std::vector
<int> &vec_a
, std::vector
<int> &vec_b
, std::vector
<int> &vec_y
, RTLIL::Cell
*cell
)
92 extendSignalWidth(vec_a
, vec_b
, cell
, vec_y
.size());
93 while (vec_y
.size() < vec_a
.size())
94 vec_y
.push_back(ez
->literal());
97 bool importCell(RTLIL::Cell
*cell
, int timestep
= -1)
99 if (cell
->type
== "$_AND_" || cell
->type
== "$_OR_" || cell
->type
== "$_XOR_" ||
100 cell
->type
== "$and" || cell
->type
== "$or" || cell
->type
== "$xor" || cell
->type
== "$xnor" ||
101 cell
->type
== "$add" || cell
->type
== "$sub") {
102 std::vector
<int> a
= importSigSpec(cell
->connections
.at("\\A"), timestep
);
103 std::vector
<int> b
= importSigSpec(cell
->connections
.at("\\B"), timestep
);
104 std::vector
<int> y
= importSigSpec(cell
->connections
.at("\\Y"), timestep
);
105 extendSignalWidth(a
, b
, y
, cell
);
106 if (cell
->type
== "$and" || cell
->type
== "$_AND_")
107 ez
->assume(ez
->vec_eq(ez
->vec_and(a
, b
), y
));
108 if (cell
->type
== "$or" || cell
->type
== "$_OR_")
109 ez
->assume(ez
->vec_eq(ez
->vec_or(a
, b
), y
));
110 if (cell
->type
== "$xor" || cell
->type
== "$_XOR_")
111 ez
->assume(ez
->vec_eq(ez
->vec_xor(a
, b
), y
));
112 if (cell
->type
== "$xnor")
113 ez
->assume(ez
->vec_eq(ez
->vec_not(ez
->vec_xor(a
, b
)), y
));
114 if (cell
->type
== "$add")
115 ez
->assume(ez
->vec_eq(ez
->vec_add(a
, b
), y
));
116 if (cell
->type
== "$sub")
117 ez
->assume(ez
->vec_eq(ez
->vec_sub(a
, b
), y
));
121 if (cell
->type
== "$_INV_" || cell
->type
== "$not") {
122 std::vector
<int> a
= importSigSpec(cell
->connections
.at("\\A"), timestep
);
123 std::vector
<int> y
= importSigSpec(cell
->connections
.at("\\Y"), timestep
);
124 ez
->assume(ez
->vec_eq(ez
->vec_not(a
), y
));
128 if (cell
->type
== "$_MUX_" || cell
->type
== "$mux") {
129 std::vector
<int> a
= importSigSpec(cell
->connections
.at("\\A"), timestep
);
130 std::vector
<int> b
= importSigSpec(cell
->connections
.at("\\B"), timestep
);
131 std::vector
<int> s
= importSigSpec(cell
->connections
.at("\\S"), timestep
);
132 std::vector
<int> y
= importSigSpec(cell
->connections
.at("\\Y"), timestep
);
133 ez
->assume(ez
->vec_eq(ez
->vec_ite(s
.at(0), b
, a
), y
));
137 if (cell
->type
== "$pmux" || cell
->type
== "$safe_pmux") {
138 std::vector
<int> a
= importSigSpec(cell
->connections
.at("\\A"), timestep
);
139 std::vector
<int> b
= importSigSpec(cell
->connections
.at("\\B"), timestep
);
140 std::vector
<int> s
= importSigSpec(cell
->connections
.at("\\S"), timestep
);
141 std::vector
<int> y
= importSigSpec(cell
->connections
.at("\\Y"), timestep
);
142 std::vector
<int> tmp
= a
;
143 for (size_t i
= 0; i
< s
.size(); i
++) {
144 std::vector
<int> part_of_b(b
.begin()+i
*a
.size(), b
.begin()+(i
+1)*a
.size());
145 tmp
= ez
->vec_ite(s
.at(i
), part_of_b
, tmp
);
147 if (cell
->type
== "$safe_pmux")
148 tmp
= ez
->vec_ite(ez
->onehot(s
, true), tmp
, a
);
149 ez
->assume(ez
->vec_eq(tmp
, y
));
153 if (cell
->type
== "$pos" || cell
->type
== "$neg") {
154 std::vector
<int> a
= importSigSpec(cell
->connections
.at("\\A"), timestep
);
155 std::vector
<int> y
= importSigSpec(cell
->connections
.at("\\Y"), timestep
);
156 if (cell
->type
== "$pos") {
157 ez
->assume(ez
->vec_eq(a
, y
));
159 std::vector
<int> zero(a
.size(), ez
->FALSE
);
160 ez
->assume(ez
->vec_eq(ez
->vec_sub(zero
, a
), y
));
165 if (cell
->type
== "$reduce_and" || cell
->type
== "$reduce_or" || cell
->type
== "$reduce_xor" ||
166 cell
->type
== "$reduce_xnor" || cell
->type
== "$reduce_bool" || cell
->type
== "$logic_not") {
167 std::vector
<int> a
= importSigSpec(cell
->connections
.at("\\A"), timestep
);
168 std::vector
<int> y
= importSigSpec(cell
->connections
.at("\\Y"), timestep
);
169 if (cell
->type
== "$reduce_and")
170 ez
->SET(ez
->expression(ez
->OpAnd
, a
), y
.at(0));
171 if (cell
->type
== "$reduce_or" || cell
->type
== "$reduce_bool")
172 ez
->SET(ez
->expression(ez
->OpOr
, a
), y
.at(0));
173 if (cell
->type
== "$reduce_xor")
174 ez
->SET(ez
->expression(ez
->OpXor
, a
), y
.at(0));
175 if (cell
->type
== "$reduce_xnor")
176 ez
->SET(ez
->NOT(ez
->expression(ez
->OpXor
, a
)), y
.at(0));
177 if (cell
->type
== "$logic_not")
178 ez
->SET(ez
->NOT(ez
->expression(ez
->OpOr
, a
)), y
.at(0));
179 for (size_t i
= 1; i
< y
.size(); i
++)
184 if (cell
->type
== "$logic_and" || cell
->type
== "$logic_or") {
185 int a
= ez
->expression(ez
->OpOr
, importSigSpec(cell
->connections
.at("\\A"), timestep
));
186 int b
= ez
->expression(ez
->OpOr
, importSigSpec(cell
->connections
.at("\\B"), timestep
));
187 std::vector
<int> y
= importSigSpec(cell
->connections
.at("\\Y"), timestep
);
188 if (cell
->type
== "$logic_and")
189 ez
->SET(ez
->expression(ez
->OpAnd
, a
, b
), y
.at(0));
191 ez
->SET(ez
->expression(ez
->OpOr
, a
, b
), y
.at(0));
192 for (size_t i
= 1; i
< y
.size(); i
++)
197 if (cell
->type
== "$lt" || cell
->type
== "$le" || cell
->type
== "$eq" || cell
->type
== "$ne" || cell
->type
== "$ge" || cell
->type
== "$gt") {
198 bool is_signed
= cell
->parameters
["\\A_SIGNED"].as_bool() && cell
->parameters
["\\B_SIGNED"].as_bool();
199 std::vector
<int> a
= importSigSpec(cell
->connections
.at("\\A"), timestep
);
200 std::vector
<int> b
= importSigSpec(cell
->connections
.at("\\B"), timestep
);
201 std::vector
<int> y
= importSigSpec(cell
->connections
.at("\\Y"), timestep
);
202 extendSignalWidth(a
, b
, cell
);
203 if (cell
->type
== "$lt")
204 ez
->SET(is_signed
? ez
->vec_lt_signed(a
, b
) : ez
->vec_lt_unsigned(a
, b
), y
.at(0));
205 if (cell
->type
== "$le")
206 ez
->SET(is_signed
? ez
->vec_le_signed(a
, b
) : ez
->vec_le_unsigned(a
, b
), y
.at(0));
207 if (cell
->type
== "$eq")
208 ez
->SET(ez
->vec_eq(a
, b
), y
.at(0));
209 if (cell
->type
== "$ne")
210 ez
->SET(ez
->vec_ne(a
, b
), y
.at(0));
211 if (cell
->type
== "$ge")
212 ez
->SET(is_signed
? ez
->vec_ge_signed(a
, b
) : ez
->vec_ge_unsigned(a
, b
), y
.at(0));
213 if (cell
->type
== "$gt")
214 ez
->SET(is_signed
? ez
->vec_gt_signed(a
, b
) : ez
->vec_gt_unsigned(a
, b
), y
.at(0));
215 for (size_t i
= 1; i
< y
.size(); i
++)
220 if (cell
->type
== "$shl" || cell
->type
== "$shr" || cell
->type
== "$sshl" || cell
->type
== "$sshr") {
221 std::vector
<int> a
= importSigSpec(cell
->connections
.at("\\A"), timestep
);
222 std::vector
<int> b
= importSigSpec(cell
->connections
.at("\\B"), timestep
);
223 std::vector
<int> y
= importSigSpec(cell
->connections
.at("\\Y"), timestep
);
224 char shift_left
= cell
->type
== "$shl" || cell
->type
== "$sshl";
225 bool sign_extend
= cell
->type
== "$sshr";
226 while (y
.size() < a
.size())
227 y
.push_back(ez
->literal());
228 std::vector
<int> tmp
= a
;
229 for (size_t i
= 0; i
< b
.size(); i
++)
231 std::vector
<int> tmp_shifted(tmp
.size());
232 for (size_t j
= 0; j
< tmp
.size(); j
++) {
233 int idx
= j
+ (1 << i
) * (shift_left
? -1 : +1);
234 tmp_shifted
.at(j
) = (0 <= idx
&& idx
< int(tmp
.size())) ? tmp
.at(idx
) : sign_extend
? tmp
.back() : ez
->FALSE
;
236 tmp
= ez
->vec_ite(b
.at(i
), tmp_shifted
, tmp
);
238 ez
->assume(ez
->vec_eq(tmp
, y
));
242 if (cell
->type
== "$mul") {
243 std::vector
<int> a
= importSigSpec(cell
->connections
.at("\\A"), timestep
);
244 std::vector
<int> b
= importSigSpec(cell
->connections
.at("\\B"), timestep
);
245 std::vector
<int> y
= importSigSpec(cell
->connections
.at("\\Y"), timestep
);
246 extendSignalWidth(a
, b
, y
, cell
);
247 std::vector
<int> tmp(a
.size(), ez
->FALSE
);
248 for (int i
= 0; i
< int(a
.size()); i
++)
250 std::vector
<int> shifted_a(a
.size(), ez
->FALSE
);
251 for (int j
= i
; j
< int(a
.size()); j
++)
252 shifted_a
.at(j
) = a
.at(j
-i
);
253 tmp
= ez
->vec_ite(b
.at(i
), ez
->vec_add(tmp
, shifted_a
), tmp
);
255 ez
->assume(ez
->vec_eq(tmp
, y
));
259 if (timestep
> 0 && (cell
->type
== "$dff" || cell
->type
== "$_DFF_N_" || cell
->type
== "$_DFF_P_")) {
261 initial_state
.add((*sigmap
)(cell
->connections
.at("\\Q")));
263 std::vector
<int> d
= importSigSpec(cell
->connections
.at("\\D"), timestep
-1);
264 std::vector
<int> q
= importSigSpec(cell
->connections
.at("\\Q"), timestep
);
265 ez
->assume(ez
->vec_eq(d
, q
));
270 // Unsupported internal cell types: $div $mod $pow
271 // .. and all sequential cells except $dff and $_DFF_[NP]_