projects / yosys.git / blob
? search:


991853c2cca0f0790101a528d881b7f1d12625b2
[yosys.git] / kernel / satgen.h
1 /*
2 * yosys -- Yosys Open SYnthesis Suite
3 *
4 * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
5 *
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.
9 *
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.
17 *
18 */
19
20 #ifndef SATGEN_H
21 #define SATGEN_H
22
23 #include "kernel/rtlil.h"
24 #include "kernel/sigtools.h"
25 #include "kernel/celltypes.h"
26
27 #ifdef YOSYS_ENABLE_MINISAT
28 # include "libs/ezsat/ezminisat.h"
29 typedef ezMiniSAT ezDefaultSAT;
30 #else
31 # include "libs/ezsat/ezsat.h"
32 typedef ezSAT ezDefaultSAT;
33 #endif
34
35 struct SatGen
36 {
37 ezSAT *ez;
38 RTLIL::Design *design;
39 SigMap *sigmap;
40 std::string prefix;
41 SigPool initial_state;
42
43 SatGen(ezSAT *ez, RTLIL::Design *design, SigMap *sigmap, std::string prefix = std::string()) :
44 ez(ez), design(design), sigmap(sigmap), prefix(prefix)
45 {
46 }
47
48 void setContext(RTLIL::Design *design, SigMap *sigmap, std::string prefix = std::string())
49 {
50 this->design = design;
51 this->sigmap = sigmap;
52 this->prefix = prefix;
53 }
54
55 std::vector<int> importSigSpec(RTLIL::SigSpec &sig, int timestep = -1)
56 {
57 assert(timestep < 0 || timestep > 0);
58 RTLIL::SigSpec s = sig;
59 sigmap->apply(s);
60 s.expand();
61
62 std::vector<int> vec;
63 vec.reserve(s.chunks.size());
64
65 for (auto &c : s.chunks)
66 if (c.wire == NULL) {
67 vec.push_back(c.data.as_bool() ? ez->TRUE : ez->FALSE);
68 } else {
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));
73 }
74 return vec;
75 }
76
77 void extendSignalWidth(std::vector<int> &vec_a, std::vector<int> &vec_b, RTLIL::Cell *cell, size_t y_width = 0)
78 {
79 bool is_signed = false;
80 if (cell->parameters.count("\\A_SIGNED") > 0 && cell->parameters.count("\\B_SIGNED") > 0)
81 is_signed = cell->parameters["\\A_SIGNED"].as_bool() && cell->parameters["\\B_SIGNED"].as_bool();
82 while (vec_a.size() < vec_b.size() || vec_a.size() < y_width)
83 vec_a.push_back(is_signed && vec_a.size() > 0 ? vec_a.back() : ez->FALSE);
84 while (vec_b.size() < vec_a.size() || vec_b.size() < y_width)
85 vec_b.push_back(is_signed && vec_b.size() > 0 ? vec_b.back() : ez->FALSE);
86 }
87
88 void extendSignalWidth(std::vector<int> &vec_a, std::vector<int> &vec_b, std::vector<int> &vec_y, RTLIL::Cell *cell)
89 {
90 extendSignalWidth(vec_a, vec_b, cell, vec_y.size());
91 while (vec_y.size() < vec_a.size())
92 vec_y.push_back(ez->literal());
93 }
94
95 void extendSignalWidthUnary(std::vector<int> &vec_a, std::vector<int> &vec_y, RTLIL::Cell *cell)
96 {
97 bool is_signed = cell->parameters.count("\\A_SIGNED") > 0 && cell->parameters["\\A_SIGNED"].as_bool();
98 while (vec_a.size() < vec_y.size())
99 vec_a.push_back(is_signed && vec_a.size() > 0 ? vec_a.back() : ez->FALSE);
100 while (vec_y.size() < vec_a.size())
101 vec_y.push_back(ez->literal());
102 }
103
104 bool importCell(RTLIL::Cell *cell, int timestep = -1)
105 {
106 if (cell->type == "$_AND_" || cell->type == "$_OR_" || cell->type == "$_XOR_" ||
107 cell->type == "$and" || cell->type == "$or" || cell->type == "$xor" || cell->type == "$xnor" ||
108 cell->type == "$add" || cell->type == "$sub") {
109 std::vector<int> a = importSigSpec(cell->connections.at("\\A"), timestep);
110 std::vector<int> b = importSigSpec(cell->connections.at("\\B"), timestep);
111 std::vector<int> y = importSigSpec(cell->connections.at("\\Y"), timestep);
112 extendSignalWidth(a, b, y, cell);
113 if (cell->type == "$and" || cell->type == "$_AND_")
114 ez->assume(ez->vec_eq(ez->vec_and(a, b), y));
115 if (cell->type == "$or" || cell->type == "$_OR_")
116 ez->assume(ez->vec_eq(ez->vec_or(a, b), y));
117 if (cell->type == "$xor" || cell->type == "$_XOR_")
118 ez->assume(ez->vec_eq(ez->vec_xor(a, b), y));
119 if (cell->type == "$xnor")
120 ez->assume(ez->vec_eq(ez->vec_not(ez->vec_xor(a, b)), y));
121 if (cell->type == "$add")
122 ez->assume(ez->vec_eq(ez->vec_add(a, b), y));
123 if (cell->type == "$sub")
124 ez->assume(ez->vec_eq(ez->vec_sub(a, b), y));
125 return true;
126 }
127
128 if (cell->type == "$_INV_" || cell->type == "$not") {
129 std::vector<int> a = importSigSpec(cell->connections.at("\\A"), timestep);
130 std::vector<int> y = importSigSpec(cell->connections.at("\\Y"), timestep);
131 extendSignalWidthUnary(a, y, cell);
132 ez->assume(ez->vec_eq(ez->vec_not(a), y));
133 return true;
134 }
135
136 if (cell->type == "$_MUX_" || cell->type == "$mux") {
137 std::vector<int> a = importSigSpec(cell->connections.at("\\A"), timestep);
138 std::vector<int> b = importSigSpec(cell->connections.at("\\B"), timestep);
139 std::vector<int> s = importSigSpec(cell->connections.at("\\S"), timestep);
140 std::vector<int> y = importSigSpec(cell->connections.at("\\Y"), timestep);
141 ez->assume(ez->vec_eq(ez->vec_ite(s.at(0), b, a), y));
142 return true;
143 }
144
145 if (cell->type == "$pmux" || cell->type == "$safe_pmux") {
146 std::vector<int> a = importSigSpec(cell->connections.at("\\A"), timestep);
147 std::vector<int> b = importSigSpec(cell->connections.at("\\B"), timestep);
148 std::vector<int> s = importSigSpec(cell->connections.at("\\S"), timestep);
149 std::vector<int> y = importSigSpec(cell->connections.at("\\Y"), timestep);
150 std::vector<int> tmp = a;
151 for (size_t i = 0; i < s.size(); i++) {
152 std::vector<int> part_of_b(b.begin()+i*a.size(), b.begin()+(i+1)*a.size());
153 tmp = ez->vec_ite(s.at(i), part_of_b, tmp);
154 }
155 if (cell->type == "$safe_pmux")
156 tmp = ez->vec_ite(ez->onehot(s, true), tmp, a);
157 ez->assume(ez->vec_eq(tmp, y));
158 return true;
159 }
160
161 if (cell->type == "$pos" || cell->type == "$neg") {
162 std::vector<int> a = importSigSpec(cell->connections.at("\\A"), timestep);
163 std::vector<int> y = importSigSpec(cell->connections.at("\\Y"), timestep);
164 extendSignalWidthUnary(a, y, cell);
165 if (cell->type == "$pos") {
166 ez->assume(ez->vec_eq(a, y));
167 } else {
168 std::vector<int> zero(a.size(), ez->FALSE);
169 ez->assume(ez->vec_eq(ez->vec_sub(zero, a), y));
170 }
171 return true;
172 }
173
174 if (cell->type == "$reduce_and" || cell->type == "$reduce_or" || cell->type == "$reduce_xor" ||
175 cell->type == "$reduce_xnor" || cell->type == "$reduce_bool" || cell->type == "$logic_not") {
176 std::vector<int> a = importSigSpec(cell->connections.at("\\A"), timestep);
177 std::vector<int> y = importSigSpec(cell->connections.at("\\Y"), timestep);
178 if (cell->type == "$reduce_and")
179 ez->SET(ez->expression(ez->OpAnd, a), y.at(0));
180 if (cell->type == "$reduce_or" || cell->type == "$reduce_bool")
181 ez->SET(ez->expression(ez->OpOr, a), y.at(0));
182 if (cell->type == "$reduce_xor")
183 ez->SET(ez->expression(ez->OpXor, a), y.at(0));
184 if (cell->type == "$reduce_xnor")
185 ez->SET(ez->NOT(ez->expression(ez->OpXor, a)), y.at(0));
186 if (cell->type == "$logic_not")
187 ez->SET(ez->NOT(ez->expression(ez->OpOr, a)), y.at(0));
188 for (size_t i = 1; i < y.size(); i++)
189 ez->SET(0, y.at(0));
190 return true;
191 }
192
193 if (cell->type == "$logic_and" || cell->type == "$logic_or") {
194 int a = ez->expression(ez->OpOr, importSigSpec(cell->connections.at("\\A"), timestep));
195 int b = ez->expression(ez->OpOr, importSigSpec(cell->connections.at("\\B"), timestep));
196 std::vector<int> y = importSigSpec(cell->connections.at("\\Y"), timestep);
197 if (cell->type == "$logic_and")
198 ez->SET(ez->expression(ez->OpAnd, a, b), y.at(0));
199 else
200 ez->SET(ez->expression(ez->OpOr, a, b), y.at(0));
201 for (size_t i = 1; i < y.size(); i++)
202 ez->SET(0, y.at(0));
203 return true;
204 }
205
206 if (cell->type == "$lt" || cell->type == "$le" || cell->type == "$eq" || cell->type == "$ne" || cell->type == "$ge" || cell->type == "$gt") {
207 bool is_signed = cell->parameters["\\A_SIGNED"].as_bool() && cell->parameters["\\B_SIGNED"].as_bool();
208 std::vector<int> a = importSigSpec(cell->connections.at("\\A"), timestep);
209 std::vector<int> b = importSigSpec(cell->connections.at("\\B"), timestep);
210 std::vector<int> y = importSigSpec(cell->connections.at("\\Y"), timestep);
211 extendSignalWidth(a, b, cell);
212 if (cell->type == "$lt")
213 ez->SET(is_signed ? ez->vec_lt_signed(a, b) : ez->vec_lt_unsigned(a, b), y.at(0));
214 if (cell->type == "$le")
215 ez->SET(is_signed ? ez->vec_le_signed(a, b) : ez->vec_le_unsigned(a, b), y.at(0));
216 if (cell->type == "$eq")
217 ez->SET(ez->vec_eq(a, b), y.at(0));
218 if (cell->type == "$ne")
219 ez->SET(ez->vec_ne(a, b), y.at(0));
220 if (cell->type == "$ge")
221 ez->SET(is_signed ? ez->vec_ge_signed(a, b) : ez->vec_ge_unsigned(a, b), y.at(0));
222 if (cell->type == "$gt")
223 ez->SET(is_signed ? ez->vec_gt_signed(a, b) : ez->vec_gt_unsigned(a, b), y.at(0));
224 for (size_t i = 1; i < y.size(); i++)
225 ez->SET(0, y.at(0));
226 return true;
227 }
228
229 if (cell->type == "$shl" || cell->type == "$shr" || cell->type == "$sshl" || cell->type == "$sshr") {
230 std::vector<int> a = importSigSpec(cell->connections.at("\\A"), timestep);
231 std::vector<int> b = importSigSpec(cell->connections.at("\\B"), timestep);
232 std::vector<int> y = importSigSpec(cell->connections.at("\\Y"), timestep);
233 char shift_left = cell->type == "$shl" || cell->type == "$sshl";
234 bool sign_extend = cell->type == "$sshr" && cell->parameters["\\A_SIGNED"].as_bool();
235 while (y.size() < a.size())
236 y.push_back(ez->literal());
237 while (y.size() > a.size())
238 a.push_back(cell->parameters["\\A_SIGNED"].as_bool() ? a.back() : ez->FALSE);
239 std::vector<int> tmp = a;
240 for (size_t i = 0; i < b.size(); i++)
241 {
242 std::vector<int> tmp_shifted(tmp.size());
243 for (size_t j = 0; j < tmp.size(); j++) {
244 int idx = j + (1 << i) * (shift_left ? -1 : +1);
245 tmp_shifted.at(j) = (0 <= idx && idx < int(tmp.size())) ? tmp.at(idx) : sign_extend ? tmp.back() : ez->FALSE;
246 }
247 tmp = ez->vec_ite(b.at(i), tmp_shifted, tmp);
248 }
249 ez->assume(ez->vec_eq(tmp, y));
250 return true;
251 }
252
253 if (cell->type == "$mul") {
254 std::vector<int> a = importSigSpec(cell->connections.at("\\A"), timestep);
255 std::vector<int> b = importSigSpec(cell->connections.at("\\B"), timestep);
256 std::vector<int> y = importSigSpec(cell->connections.at("\\Y"), timestep);
257 extendSignalWidth(a, b, y, cell);
258 std::vector<int> tmp(a.size(), ez->FALSE);
259 for (int i = 0; i < int(a.size()); i++)
260 {
261 std::vector<int> shifted_a(a.size(), ez->FALSE);
262 for (int j = i; j < int(a.size()); j++)
263 shifted_a.at(j) = a.at(j-i);
264 tmp = ez->vec_ite(b.at(i), ez->vec_add(tmp, shifted_a), tmp);
265 }
266 ez->assume(ez->vec_eq(tmp, y));
267 return true;
268 }
269
270 if (timestep > 0 && (cell->type == "$dff" || cell->type == "$_DFF_N_" || cell->type == "$_DFF_P_")) {
271 if (timestep == 1) {
272 initial_state.add((*sigmap)(cell->connections.at("\\Q")));
273 } else {
274 std::vector<int> d = importSigSpec(cell->connections.at("\\D"), timestep-1);
275 std::vector<int> q = importSigSpec(cell->connections.at("\\Q"), timestep);
276 ez->assume(ez->vec_eq(d, q));
277 }
278 return true;
279 }
280
281 // Unsupported internal cell types: $div $mod $pow
282 // .. and all sequential cells except $dff and $_DFF_[NP]_
283 return false;
284 }
285 };
286
287 #endif
288