projects / yosys.git / blob
? search:
summary | shortlog | log | commit | commitdiff | tree
history | raw | HEAD
Merge branch 'master' into btor-ng
[yosys.git] / backends / smt2 / smt2.cc
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 #include "kernel/rtlil.h"
21 #include "kernel/register.h"
22 #include "kernel/sigtools.h"
23 #include "kernel/celltypes.h"
24 #include "kernel/log.h"
25 #include <string>
26
27 USING_YOSYS_NAMESPACE
28 PRIVATE_NAMESPACE_BEGIN
29
30 struct Smt2Worker
31 {
32 CellTypes ct;
33 SigMap sigmap;
34 RTLIL::Module *module;
35 bool bvmode, memmode, wiresmode, verbose, statebv, statedt;
36 dict<IdString, int> &mod_stbv_width;
37 int idcounter, statebv_width;
38
39 std::vector<std::string> decls, trans, hier, dtmembers;
40 std::map<RTLIL::SigBit, RTLIL::Cell*> bit_driver;
41 std::set<RTLIL::Cell*> exported_cells, hiercells, hiercells_queue;
42 pool<Cell*> recursive_cells, registers;
43
44 std::map<RTLIL::SigBit, std::pair<int, int>> fcache;
45 std::map<Cell*, int> memarrays;
46 std::map<int, int> bvsizes;
47 dict<IdString, char*> ids;
48
49 const char *get_id(IdString n)
50 {
51 if (ids.count(n) == 0) {
52 std::string str = log_id(n);
53 for (int i = 0; i < GetSize(str); i++) {
54 if (str[i] == '\\')
55 str[i] = '/';
56 }
57 ids[n] = strdup(str.c_str());
58 }
59 return ids[n];
60 }
61
62 template<typename T>
63 const char *get_id(T *obj) {
64 return get_id(obj->name);
65 }
66
67 void makebits(std::string name, int width = 0, std::string comment = std::string())
68 {
69 std::string decl_str;
70
71 if (statebv)
72 {
73 if (width == 0) {
74 decl_str = stringf("(define-fun |%s| ((state |%s_s|)) Bool (= ((_ extract %d %d) state) #b1))", name.c_str(), get_id(module), statebv_width, statebv_width);
75 statebv_width += 1;
76 } else {
77 decl_str = stringf("(define-fun |%s| ((state |%s_s|)) (_ BitVec %d) ((_ extract %d %d) state))", name.c_str(), get_id(module), width, statebv_width+width-1, statebv_width);
78 statebv_width += width;
79 }
80 }
81 else if (statedt)
82 {
83 if (width == 0) {
84 decl_str = stringf(" (|%s| Bool)", name.c_str());
85 } else {
86 decl_str = stringf(" (|%s| (_ BitVec %d))", name.c_str(), width);
87 }
88 }
89 else
90 {
91 if (width == 0) {
92 decl_str = stringf("(declare-fun |%s| (|%s_s|) Bool)", name.c_str(), get_id(module));
93 } else {
94 decl_str = stringf("(declare-fun |%s| (|%s_s|) (_ BitVec %d))", name.c_str(), get_id(module), width);
95 }
96 }
97
98 if (!comment.empty())
99 decl_str += " ; " + comment;
100
101 if (statedt)
102 dtmembers.push_back(decl_str + "\n");
103 else
104 decls.push_back(decl_str + "\n");
105 }
106
107 Smt2Worker(RTLIL::Module *module, bool bvmode, bool memmode, bool wiresmode, bool verbose, bool statebv, bool statedt, dict<IdString, int> &mod_stbv_width) :
108 ct(module->design), sigmap(module), module(module), bvmode(bvmode), memmode(memmode), wiresmode(wiresmode),
109 verbose(verbose), statebv(statebv), statedt(statedt), mod_stbv_width(mod_stbv_width), idcounter(0), statebv_width(0)
110 {
111 makebits(stringf("%s_is", get_id(module)));
112
113 for (auto cell : module->cells())
114 for (auto &conn : cell->connections()) {
115 bool is_input = ct.cell_input(cell->type, conn.first);
116 bool is_output = ct.cell_output(cell->type, conn.first);
117 if (is_output && !is_input)
118 for (auto bit : sigmap(conn.second)) {
119 if (bit_driver.count(bit))
120 log_error("Found multiple drivers for %s.\n", log_signal(bit));
121 bit_driver[bit] = cell;
122 }
123 else if (is_output || !is_input)
124 log_error("Unsupported or unknown directionality on port %s of cell %s.%s (%s).\n",
125 log_id(conn.first), log_id(module), log_id(cell), log_id(cell->type));
126 }
127 }
128
129 ~Smt2Worker()
130 {
131 for (auto &it : ids)
132 free(it.second);
133 ids.clear();
134 }
135
136 const char *get_id(Module *m)
137 {
138 return get_id(m->name);
139 }
140
141 const char *get_id(Cell *c)
142 {
143 return get_id(c->name);
144 }
145
146 const char *get_id(Wire *w)
147 {
148 return get_id(w->name);
149 }
150
151 void register_bool(RTLIL::SigBit bit, int id)
152 {
153 if (verbose) log("%*s-> register_bool: %s %d\n", 2+2*GetSize(recursive_cells), "",
154 log_signal(bit), id);
155
156 sigmap.apply(bit);
157 log_assert(fcache.count(bit) == 0);
158 fcache[bit] = std::pair<int, int>(id, -1);
159 }
160
161 void register_bv(RTLIL::SigSpec sig, int id)
162 {
163 if (verbose) log("%*s-> register_bv: %s %d\n", 2+2*GetSize(recursive_cells), "",
164 log_signal(sig), id);
165
166 log_assert(bvmode);
167 sigmap.apply(sig);
168
169 log_assert(bvsizes.count(id) == 0);
170 bvsizes[id] = GetSize(sig);
171
172 for (int i = 0; i < GetSize(sig); i++) {
173 log_assert(fcache.count(sig[i]) == 0);
174 fcache[sig[i]] = std::pair<int, int>(id, i);
175 }
176 }
177
178 void register_boolvec(RTLIL::SigSpec sig, int id)
179 {
180 if (verbose) log("%*s-> register_boolvec: %s %d\n", 2+2*GetSize(recursive_cells), "",
181 log_signal(sig), id);
182
183 log_assert(bvmode);
184 sigmap.apply(sig);
185 register_bool(sig[0], id);
186
187 for (int i = 1; i < GetSize(sig); i++)
188 sigmap.add(sig[i], RTLIL::State::S0);
189 }
190
191 std::string get_bool(RTLIL::SigBit bit, const char *state_name = "state")
192 {
193 sigmap.apply(bit);
194
195 if (bit.wire == nullptr)
196 return bit == RTLIL::State::S1 ? "true" : "false";
197
198 if (bit_driver.count(bit))
199 export_cell(bit_driver.at(bit));
200 sigmap.apply(bit);
201
202 if (fcache.count(bit) == 0) {
203 if (verbose) log("%*s-> external bool: %s\n", 2+2*GetSize(recursive_cells), "",
204 log_signal(bit));
205 makebits(stringf("%s#%d", get_id(module), idcounter), 0, log_signal(bit));
206 register_bool(bit, idcounter++);
207 }
208
209 auto f = fcache.at(bit);
210 if (f.second >= 0)
211 return stringf("(= ((_ extract %d %d) (|%s#%d| %s)) #b1)", f.second, f.second, get_id(module), f.first, state_name);
212 return stringf("(|%s#%d| %s)", get_id(module), f.first, state_name);
213 }
214
215 std::string get_bool(RTLIL::SigSpec sig, const char *state_name = "state")
216 {
217 return get_bool(sig.as_bit(), state_name);
218 }
219
220 std::string get_bv(RTLIL::SigSpec sig, const char *state_name = "state")
221 {
222 log_assert(bvmode);
223 sigmap.apply(sig);
224
225 std::vector<std::string> subexpr;
226
227 SigSpec orig_sig;
228 while (orig_sig != sig) {
229 for (auto bit : sig)
230 if (bit_driver.count(bit))
231 export_cell(bit_driver.at(bit));
232 orig_sig = sig;
233 sigmap.apply(sig);
234 }
235
236 for (int i = 0, j = 1; i < GetSize(sig); i += j, j = 1)
237 {
238 if (sig[i].wire == nullptr) {
239 while (i+j < GetSize(sig) && sig[i+j].wire == nullptr) j++;
240 subexpr.push_back("#b");
241 for (int k = i+j-1; k >= i; k--)
242 subexpr.back() += sig[k] == RTLIL::State::S1 ? "1" : "0";
243 continue;
244 }
245
246 if (fcache.count(sig[i]) && fcache.at(sig[i]).second == -1) {
247 subexpr.push_back(stringf("(ite %s #b1 #b0)", get_bool(sig[i], state_name).c_str()));
248 continue;
249 }
250
251 if (fcache.count(sig[i])) {
252 auto t1 = fcache.at(sig[i]);
253 while (i+j < GetSize(sig)) {
254 if (fcache.count(sig[i+j]) == 0)
255 break;
256 auto t2 = fcache.at(sig[i+j]);
257 if (t1.first != t2.first)
258 break;
259 if (t1.second+j != t2.second)
260 break;
261 j++;
262 }
263 if (t1.second == 0 && j == bvsizes.at(t1.first))
264 subexpr.push_back(stringf("(|%s#%d| %s)", get_id(module), t1.first, state_name));
265 else
266 subexpr.push_back(stringf("((_ extract %d %d) (|%s#%d| %s))",
267 t1.second + j - 1, t1.second, get_id(module), t1.first, state_name));
268 continue;
269 }
270
271 std::set<RTLIL::SigBit> seen_bits = { sig[i] };
272 while (i+j < GetSize(sig) && sig[i+j].wire && !fcache.count(sig[i+j]) && !seen_bits.count(sig[i+j]))
273 seen_bits.insert(sig[i+j]), j++;
274
275 if (verbose) log("%*s-> external bv: %s\n", 2+2*GetSize(recursive_cells), "",
276 log_signal(sig.extract(i, j)));
277 for (auto bit : sig.extract(i, j))
278 log_assert(bit_driver.count(bit) == 0);
279 makebits(stringf("%s#%d", get_id(module), idcounter), j, log_signal(sig.extract(i, j)));
280 subexpr.push_back(stringf("(|%s#%d| %s)", get_id(module), idcounter, state_name));
281 register_bv(sig.extract(i, j), idcounter++);
282 }
283
284 if (GetSize(subexpr) > 1) {
285 std::string expr = "", end_str = "";
286 for (int i = GetSize(subexpr)-1; i >= 0; i--) {
287 if (i > 0) expr += " (concat", end_str += ")";
288 expr += " " + subexpr[i];
289 }
290 return expr.substr(1) + end_str;
291 } else {
292 log_assert(GetSize(subexpr) == 1);
293 return subexpr[0];
294 }
295 }
296
297 void export_gate(RTLIL::Cell *cell, std::string expr)
298 {
299 RTLIL::SigBit bit = sigmap(cell->getPort("\\Y").as_bit());
300 std::string processed_expr;
301
302 for (char ch : expr) {
303 if (ch == 'A') processed_expr += get_bool(cell->getPort("\\A"));
304 else if (ch == 'B') processed_expr += get_bool(cell->getPort("\\B"));
305 else if (ch == 'C') processed_expr += get_bool(cell->getPort("\\C"));
306 else if (ch == 'D') processed_expr += get_bool(cell->getPort("\\D"));
307 else if (ch == 'S') processed_expr += get_bool(cell->getPort("\\S"));
308 else processed_expr += ch;
309 }
310
311 if (verbose)
312 log("%*s-> import cell: %s\n", 2+2*GetSize(recursive_cells), "", log_id(cell));
313
314 decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool %s) ; %s\n",
315 get_id(module), idcounter, get_id(module), processed_expr.c_str(), log_signal(bit)));
316 register_bool(bit, idcounter++);
317 recursive_cells.erase(cell);
318 }
319
320 void export_bvop(RTLIL::Cell *cell, std::string expr, char type = 0)
321 {
322 RTLIL::SigSpec sig_a, sig_b;
323 RTLIL::SigSpec sig_y = sigmap(cell->getPort("\\Y"));
324 bool is_signed = cell->getParam("\\A_SIGNED").as_bool();
325 int width = GetSize(sig_y);
326
327 if (type == 's' || type == 'd' || type == 'b') {
328 width = max(width, GetSize(cell->getPort("\\A")));
329 width = max(width, GetSize(cell->getPort("\\B")));
330 }
331
332 if (cell->hasPort("\\A")) {
333 sig_a = cell->getPort("\\A");
334 sig_a.extend_u0(width, is_signed);
335 }
336
337 if (cell->hasPort("\\B")) {
338 sig_b = cell->getPort("\\B");
339 sig_b.extend_u0(width, is_signed && !(type == 's'));
340 }
341
342 std::string processed_expr;
343
344 for (char ch : expr) {
345 if (ch == 'A') processed_expr += get_bv(sig_a);
346 else if (ch == 'B') processed_expr += get_bv(sig_b);
347 else if (ch == 'L') processed_expr += is_signed ? "a" : "l";
348 else if (ch == 'U') processed_expr += is_signed ? "s" : "u";
349 else processed_expr += ch;
350 }
351
352 if (width != GetSize(sig_y) && type != 'b')
353 processed_expr = stringf("((_ extract %d 0) %s)", GetSize(sig_y)-1, processed_expr.c_str());
354
355 if (verbose)
356 log("%*s-> import cell: %s\n", 2+2*GetSize(recursive_cells), "", log_id(cell));
357
358 if (type == 'b') {
359 decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool %s) ; %s\n",
360 get_id(module), idcounter, get_id(module), processed_expr.c_str(), log_signal(sig_y)));
361 register_boolvec(sig_y, idcounter++);
362 } else {
363 decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
364 get_id(module), idcounter, get_id(module), GetSize(sig_y), processed_expr.c_str(), log_signal(sig_y)));
365 register_bv(sig_y, idcounter++);
366 }
367
368 recursive_cells.erase(cell);
369 }
370
371 void export_reduce(RTLIL::Cell *cell, std::string expr, bool identity_val)
372 {
373 RTLIL::SigSpec sig_y = sigmap(cell->getPort("\\Y"));
374 std::string processed_expr;
375
376 for (char ch : expr)
377 if (ch == 'A' || ch == 'B') {
378 RTLIL::SigSpec sig = sigmap(cell->getPort(stringf("\\%c", ch)));
379 for (auto bit : sig)
380 processed_expr += " " + get_bool(bit);
381 if (GetSize(sig) == 1)
382 processed_expr += identity_val ? " true" : " false";
383 } else
384 processed_expr += ch;
385
386 if (verbose)
387 log("%*s-> import cell: %s\n", 2+2*GetSize(recursive_cells), "", log_id(cell));
388
389 decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool %s) ; %s\n",
390 get_id(module), idcounter, get_id(module), processed_expr.c_str(), log_signal(sig_y)));
391 register_boolvec(sig_y, idcounter++);
392 recursive_cells.erase(cell);
393 }
394
395 void export_cell(RTLIL::Cell *cell)
396 {
397 if (verbose)
398 log("%*s=> export_cell %s (%s) [%s]\n", 2+2*GetSize(recursive_cells), "",
399 log_id(cell), log_id(cell->type), exported_cells.count(cell) ? "old" : "new");
400
401 if (recursive_cells.count(cell))
402 log_error("Found logic loop in module %s! See cell %s.\n", get_id(module), get_id(cell));
403
404 if (exported_cells.count(cell))
405 return;
406
407 exported_cells.insert(cell);
408 recursive_cells.insert(cell);
409
410 if (cell->type == "$initstate")
411 {
412 SigBit bit = sigmap(cell->getPort("\\Y").as_bit());
413 decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool (|%s_is| state)) ; %s\n",
414 get_id(module), idcounter, get_id(module), get_id(module), log_signal(bit)));
415 register_bool(bit, idcounter++);
416 recursive_cells.erase(cell);
417 return;
418 }
419
420 if (cell->type.in("$_FF_", "$_DFF_P_", "$_DFF_N_"))
421 {
422 registers.insert(cell);
423 makebits(stringf("%s#%d", get_id(module), idcounter), 0, log_signal(cell->getPort("\\Q")));
424 register_bool(cell->getPort("\\Q"), idcounter++);
425 recursive_cells.erase(cell);
426 return;
427 }
428
429 if (cell->type == "$_BUF_") return export_gate(cell, "A");
430 if (cell->type == "$_NOT_") return export_gate(cell, "(not A)");
431 if (cell->type == "$_AND_") return export_gate(cell, "(and A B)");
432 if (cell->type == "$_NAND_") return export_gate(cell, "(not (and A B))");
433 if (cell->type == "$_OR_") return export_gate(cell, "(or A B)");
434 if (cell->type == "$_NOR_") return export_gate(cell, "(not (or A B))");
435 if (cell->type == "$_XOR_") return export_gate(cell, "(xor A B)");
436 if (cell->type == "$_XNOR_") return export_gate(cell, "(not (xor A B))");
437 if (cell->type == "$_ANDNOT_") return export_gate(cell, "(and A (not B))");
438 if (cell->type == "$_ORNOT_") return export_gate(cell, "(or A (not B))");
439 if (cell->type == "$_MUX_") return export_gate(cell, "(ite S B A)");
440 if (cell->type == "$_AOI3_") return export_gate(cell, "(not (or (and A B) C))");
441 if (cell->type == "$_OAI3_") return export_gate(cell, "(not (and (or A B) C))");
442 if (cell->type == "$_AOI4_") return export_gate(cell, "(not (or (and A B) (and C D)))");
443 if (cell->type == "$_OAI4_") return export_gate(cell, "(not (and (or A B) (or C D)))");
444
445 // FIXME: $lut
446
447 if (bvmode)
448 {
449 if (cell->type.in("$ff", "$dff"))
450 {
451 registers.insert(cell);
452 makebits(stringf("%s#%d", get_id(module), idcounter), GetSize(cell->getPort("\\Q")), log_signal(cell->getPort("\\Q")));
453 register_bv(cell->getPort("\\Q"), idcounter++);
454 recursive_cells.erase(cell);
455 return;
456 }
457
458 if (cell->type.in("$anyconst", "$anyseq"))
459 {
460 registers.insert(cell);
461 string infostr = cell->attributes.count("\\src") ? cell->attributes.at("\\src").decode_string().c_str() : get_id(cell);
462 if (cell->attributes.count("\\reg"))
463 infostr += " " + cell->attributes.at("\\reg").decode_string();
464 decls.push_back(stringf("; yosys-smt2-%s %s#%d %s\n", cell->type.c_str() + 1, get_id(module), idcounter, infostr.c_str()));
465 makebits(stringf("%s#%d", get_id(module), idcounter), GetSize(cell->getPort("\\Y")), log_signal(cell->getPort("\\Y")));
466 register_bv(cell->getPort("\\Y"), idcounter++);
467 recursive_cells.erase(cell);
468 return;
469 }
470
471 if (cell->type == "$and") return export_bvop(cell, "(bvand A B)");
472 if (cell->type == "$or") return export_bvop(cell, "(bvor A B)");
473 if (cell->type == "$xor") return export_bvop(cell, "(bvxor A B)");
474 if (cell->type == "$xnor") return export_bvop(cell, "(bvxnor A B)");
475
476 if (cell->type == "$shl") return export_bvop(cell, "(bvshl A B)", 's');
477 if (cell->type == "$shr") return export_bvop(cell, "(bvlshr A B)", 's');
478 if (cell->type == "$sshl") return export_bvop(cell, "(bvshl A B)", 's');
479 if (cell->type == "$sshr") return export_bvop(cell, "(bvLshr A B)", 's');
480
481 if (cell->type.in("$shift", "$shiftx")) {
482 if (cell->getParam("\\B_SIGNED").as_bool()) {
483 /* FIXME */
484 } else {
485 return export_bvop(cell, "(bvlshr A B)", 's');
486 }
487 }
488
489 if (cell->type == "$lt") return export_bvop(cell, "(bvUlt A B)", 'b');
490 if (cell->type == "$le") return export_bvop(cell, "(bvUle A B)", 'b');
491 if (cell->type == "$ge") return export_bvop(cell, "(bvUge A B)", 'b');
492 if (cell->type == "$gt") return export_bvop(cell, "(bvUgt A B)", 'b');
493
494 if (cell->type == "$ne") return export_bvop(cell, "(distinct A B)", 'b');
495 if (cell->type == "$nex") return export_bvop(cell, "(distinct A B)", 'b');
496 if (cell->type == "$eq") return export_bvop(cell, "(= A B)", 'b');
497 if (cell->type == "$eqx") return export_bvop(cell, "(= A B)", 'b');
498
499 if (cell->type == "$not") return export_bvop(cell, "(bvnot A)");
500 if (cell->type == "$pos") return export_bvop(cell, "A");
501 if (cell->type == "$neg") return export_bvop(cell, "(bvneg A)");
502
503 if (cell->type == "$add") return export_bvop(cell, "(bvadd A B)");
504 if (cell->type == "$sub") return export_bvop(cell, "(bvsub A B)");
505 if (cell->type == "$mul") return export_bvop(cell, "(bvmul A B)");
506 if (cell->type == "$div") return export_bvop(cell, "(bvUdiv A B)", 'd');
507 if (cell->type == "$mod") return export_bvop(cell, "(bvUrem A B)", 'd');
508
509 if (cell->type == "$reduce_and") return export_reduce(cell, "(and A)", true);
510 if (cell->type == "$reduce_or") return export_reduce(cell, "(or A)", false);
511 if (cell->type == "$reduce_xor") return export_reduce(cell, "(xor A)", false);
512 if (cell->type == "$reduce_xnor") return export_reduce(cell, "(not (xor A))", false);
513 if (cell->type == "$reduce_bool") return export_reduce(cell, "(or A)", false);
514
515 if (cell->type == "$logic_not") return export_reduce(cell, "(not (or A))", false);
516 if (cell->type == "$logic_and") return export_reduce(cell, "(and (or A) (or B))", false);
517 if (cell->type == "$logic_or") return export_reduce(cell, "(or A B)", false);
518
519 if (cell->type == "$mux" || cell->type == "$pmux")
520 {
521 int width = GetSize(cell->getPort("\\Y"));
522 std::string processed_expr = get_bv(cell->getPort("\\A"));
523
524 RTLIL::SigSpec sig_b = cell->getPort("\\B");
525 RTLIL::SigSpec sig_s = cell->getPort("\\S");
526 get_bv(sig_b);
527 get_bv(sig_s);
528
529 for (int i = 0; i < GetSize(sig_s); i++)
530 processed_expr = stringf("(ite %s %s %s)", get_bool(sig_s[i]).c_str(),
531 get_bv(sig_b.extract(i*width, width)).c_str(), processed_expr.c_str());
532
533 if (verbose)
534 log("%*s-> import cell: %s\n", 2+2*GetSize(recursive_cells), "", log_id(cell));
535
536 RTLIL::SigSpec sig = sigmap(cell->getPort("\\Y"));
537 decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
538 get_id(module), idcounter, get_id(module), width, processed_expr.c_str(), log_signal(sig)));
539 register_bv(sig, idcounter++);
540 recursive_cells.erase(cell);
541 return;
542 }
543
544 // FIXME: $slice $concat
545 }
546
547 if (memmode && cell->type == "$mem")
548 {
549 int arrayid = idcounter++;
550 memarrays[cell] = arrayid;
551
552 int abits = cell->getParam("\\ABITS").as_int();
553 int width = cell->getParam("\\WIDTH").as_int();
554 int rd_ports = cell->getParam("\\RD_PORTS").as_int();
555 int wr_ports = cell->getParam("\\WR_PORTS").as_int();
556
557 bool async_read = false;
558 if (!cell->getParam("\\WR_CLK_ENABLE").is_fully_ones()) {
559 if (!cell->getParam("\\WR_CLK_ENABLE").is_fully_zero())
560 log_error("Memory %s.%s has mixed clocked/nonclocked write ports. This is not supported by \"write_smt2\".\n", log_id(cell), log_id(module));
561 async_read = true;
562 }
563
564 decls.push_back(stringf("; yosys-smt2-memory %s %d %d %d %d %s\n", get_id(cell), abits, width, rd_ports, wr_ports, async_read ? "async" : "sync"));
565
566 string memstate;
567 if (async_read) {
568 memstate = stringf("%s#%d#final", get_id(module), arrayid);
569 } else {
570 memstate = stringf("%s#%d#0", get_id(module), arrayid);
571 }
572
573 if (statebv)
574 {
575 int mem_size = cell->getParam("\\SIZE").as_int();
576 int mem_offset = cell->getParam("\\OFFSET").as_int();
577
578 makebits(memstate, width*mem_size, get_id(cell));
579 decls.push_back(stringf("(define-fun |%s_m %s| ((state |%s_s|)) (_ BitVec %d) (|%s| state))\n",
580 get_id(module), get_id(cell), get_id(module), width*mem_size, memstate.c_str()));
581
582 for (int i = 0; i < rd_ports; i++)
583 {
584 SigSpec addr_sig = cell->getPort("\\RD_ADDR").extract(abits*i, abits);
585 SigSpec data_sig = cell->getPort("\\RD_DATA").extract(width*i, width);
586 std::string addr = get_bv(addr_sig);
587
588 if (cell->getParam("\\RD_CLK_ENABLE").extract(i).as_bool())
589 log_error("Read port %d (%s) of memory %s.%s is clocked. This is not supported by \"write_smt2\"! "
590 "Call \"memory\" with -nordff to avoid this error.\n", i, log_signal(data_sig), log_id(cell), log_id(module));
591
592 decls.push_back(stringf("(define-fun |%s_m:R%dA %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
593 get_id(module), i, get_id(cell), get_id(module), abits, addr.c_str(), log_signal(addr_sig)));
594
595 std::string read_expr = "#b";
596 for (int k = 0; k < width; k++)
597 read_expr += "0";
598
599 for (int k = 0; k < mem_size; k++)
600 read_expr = stringf("(ite (= (|%s_m:R%dA %s| state) #b%s) ((_ extract %d %d) (|%s| state))\n %s)",
601 get_id(module), i, get_id(cell), Const(k+mem_offset, abits).as_string().c_str(),
602 width*(k+1)-1, width*k, memstate.c_str(), read_expr.c_str());
603
604 decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d)\n %s) ; %s\n",
605 get_id(module), idcounter, get_id(module), width, read_expr.c_str(), log_signal(data_sig)));
606
607 decls.push_back(stringf("(define-fun |%s_m:R%dD %s| ((state |%s_s|)) (_ BitVec %d) (|%s#%d| state))\n",
608 get_id(module), i, get_id(cell), get_id(module), width, get_id(module), idcounter));
609
610 register_bv(data_sig, idcounter++);
611 }
612 }
613 else
614 {
615 if (statedt)
616 dtmembers.push_back(stringf(" (|%s| (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n",
617 memstate.c_str(), abits, width, get_id(cell)));
618 else
619 decls.push_back(stringf("(declare-fun |%s| (|%s_s|) (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n",
620 memstate.c_str(), get_id(module), abits, width, get_id(cell)));
621
622 decls.push_back(stringf("(define-fun |%s_m %s| ((state |%s_s|)) (Array (_ BitVec %d) (_ BitVec %d)) (|%s| state))\n",
623 get_id(module), get_id(cell), get_id(module), abits, width, memstate.c_str()));
624
625 for (int i = 0; i < rd_ports; i++)
626 {
627 SigSpec addr_sig = cell->getPort("\\RD_ADDR").extract(abits*i, abits);
628 SigSpec data_sig = cell->getPort("\\RD_DATA").extract(width*i, width);
629 std::string addr = get_bv(addr_sig);
630
631 if (cell->getParam("\\RD_CLK_ENABLE").extract(i).as_bool())
632 log_error("Read port %d (%s) of memory %s.%s is clocked. This is not supported by \"write_smt2\"! "
633 "Call \"memory\" with -nordff to avoid this error.\n", i, log_signal(data_sig), log_id(cell), log_id(module));
634
635 decls.push_back(stringf("(define-fun |%s_m:R%dA %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
636 get_id(module), i, get_id(cell), get_id(module), abits, addr.c_str(), log_signal(addr_sig)));
637
638 decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d) (select (|%s| state) (|%s_m:R%dA %s| state))) ; %s\n",
639 get_id(module), idcounter, get_id(module), width, memstate.c_str(), get_id(module), i, get_id(cell), log_signal(data_sig)));
640
641 decls.push_back(stringf("(define-fun |%s_m:R%dD %s| ((state |%s_s|)) (_ BitVec %d) (|%s#%d| state))\n",
642 get_id(module), i, get_id(cell), get_id(module), width, get_id(module), idcounter));
643
644 register_bv(data_sig, idcounter++);
645 }
646 }
647
648 registers.insert(cell);
649 recursive_cells.erase(cell);
650 return;
651 }
652
653 Module *m = module->design->module(cell->type);
654
655 if (m != nullptr)
656 {
657 decls.push_back(stringf("; yosys-smt2-cell %s %s\n", get_id(cell->type), get_id(cell->name)));
658 string cell_state = stringf("(|%s_h %s| state)", get_id(module), get_id(cell->name));
659
660 for (auto &conn : cell->connections())
661 {
662 Wire *w = m->wire(conn.first);
663 SigSpec sig = sigmap(conn.second);
664
665 if (w->port_output && !w->port_input) {
666 if (GetSize(w) > 1) {
667 if (bvmode) {
668 makebits(stringf("%s#%d", get_id(module), idcounter), GetSize(w), log_signal(sig));
669 register_bv(sig, idcounter++);
670 } else {
671 for (int i = 0; i < GetSize(w); i++) {
672 makebits(stringf("%s#%d", get_id(module), idcounter), 0, log_signal(sig[i]));
673 register_bool(sig[i], idcounter++);
674 }
675 }
676 } else {
677 makebits(stringf("%s#%d", get_id(module), idcounter), 0, log_signal(sig));
678 register_bool(sig, idcounter++);
679 }
680 }
681 }
682
683 if (statebv)
684 makebits(stringf("%s_h %s", get_id(module), get_id(cell->name)), mod_stbv_width.at(cell->type));
685 if (statedt)
686 dtmembers.push_back(stringf(" (|%s_h %s| |%s_s|)\n",
687 get_id(module), get_id(cell->name), get_id(cell->type)));
688 else
689 decls.push_back(stringf("(declare-fun |%s_h %s| (|%s_s|) |%s_s|)\n",
690 get_id(module), get_id(cell->name), get_id(module), get_id(cell->type)));
691
692 hiercells.insert(cell);
693 hiercells_queue.insert(cell);
694 recursive_cells.erase(cell);
695 return;
696 }
697
698 log_error("Unsupported cell type %s for cell %s.%s.\n",
699 log_id(cell->type), log_id(module), log_id(cell));
700 }
701
702 void run()
703 {
704 if (verbose) log("=> export logic driving outputs\n");
705
706 pool<SigBit> reg_bits;
707 for (auto cell : module->cells())
708 if (cell->type.in("$ff", "$dff", "$_FF_", "$_DFF_P_", "$_DFF_N_")) {
709 // not using sigmap -- we want the net directly at the dff output
710 for (auto bit : cell->getPort("\\Q"))
711 reg_bits.insert(bit);
712 }
713
714 for (auto wire : module->wires()) {
715 bool is_register = false;
716 for (auto bit : SigSpec(wire))
717 if (reg_bits.count(bit))
718 is_register = true;
719 if (wire->port_id || is_register || wire->get_bool_attribute("\\keep") || (wiresmode && wire->name[0] == '\\')) {
720 RTLIL::SigSpec sig = sigmap(wire);
721 if (wire->port_input)
722 decls.push_back(stringf("; yosys-smt2-input %s %d\n", get_id(wire), wire->width));
723 if (wire->port_output)
724 decls.push_back(stringf("; yosys-smt2-output %s %d\n", get_id(wire), wire->width));
725 if (is_register)
726 decls.push_back(stringf("; yosys-smt2-register %s %d\n", get_id(wire), wire->width));
727 if (wire->get_bool_attribute("\\keep") || (wiresmode && wire->name[0] == '\\'))
728 decls.push_back(stringf("; yosys-smt2-wire %s %d\n", get_id(wire), wire->width));
729 if (bvmode && GetSize(sig) > 1) {
730 decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) (_ BitVec %d) %s)\n",
731 get_id(module), get_id(wire), get_id(module), GetSize(sig), get_bv(sig).c_str()));
732 } else {
733 for (int i = 0; i < GetSize(sig); i++)
734 if (GetSize(sig) > 1)
735 decls.push_back(stringf("(define-fun |%s_n %s %d| ((state |%s_s|)) Bool %s)\n",
736 get_id(module), get_id(wire), i, get_id(module), get_bool(sig[i]).c_str()));
737 else
738 decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) Bool %s)\n",
739 get_id(module), get_id(wire), get_id(module), get_bool(sig[i]).c_str()));
740 }
741 }
742 }
743
744 if (verbose) log("=> export logic associated with the initial state\n");
745
746 vector<string> init_list;
747 for (auto wire : module->wires())
748 if (wire->attributes.count("\\init")) {
749 RTLIL::SigSpec sig = sigmap(wire);
750 Const val = wire->attributes.at("\\init");
751 val.bits.resize(GetSize(sig), State::Sx);
752 if (bvmode && GetSize(sig) > 1) {
753 Const mask(State::S1, GetSize(sig));
754 bool use_mask = false;
755 for (int i = 0; i < GetSize(sig); i++)
756 if (val[i] != State::S0 && val[i] != State::S1) {
757 val[i] = State::S0;
758 mask[i] = State::S0;
759 use_mask = true;
760 }
761 if (use_mask)
762 init_list.push_back(stringf("(= (bvand %s #b%s) #b%s) ; %s", get_bv(sig).c_str(), mask.as_string().c_str(), val.as_string().c_str(), get_id(wire)));
763 else
764 init_list.push_back(stringf("(= %s #b%s) ; %s", get_bv(sig).c_str(), val.as_string().c_str(), get_id(wire)));
765 } else {
766 for (int i = 0; i < GetSize(sig); i++)
767 if (val[i] == State::S0 || val[i] == State::S1)
768 init_list.push_back(stringf("(= %s %s) ; %s", get_bool(sig[i]).c_str(), val[i] == State::S1 ? "true" : "false", get_id(wire)));
769 }
770 }
771
772 if (verbose) log("=> export logic driving asserts\n");
773
774 int assert_id = 0, assume_id = 0, cover_id = 0;
775 vector<string> assert_list, assume_list, cover_list;
776
777 for (auto cell : module->cells())
778 {
779 if (cell->type.in("$assert", "$assume", "$cover"))
780 {
781 int &id = cell->type == "$assert" ? assert_id :
782 cell->type == "$assume" ? assume_id :
783 cell->type == "$cover" ? cover_id : *(int*)nullptr;
784
785 char postfix = cell->type == "$assert" ? 'a' :
786 cell->type == "$assume" ? 'u' :
787 cell->type == "$cover" ? 'c' : 0;
788
789 string name_a = get_bool(cell->getPort("\\A"));
790 string name_en = get_bool(cell->getPort("\\EN"));
791 decls.push_back(stringf("; yosys-smt2-%s %d %s\n", cell->type.c_str() + 1, id,
792 cell->attributes.count("\\src") ? cell->attributes.at("\\src").decode_string().c_str() : get_id(cell)));
793
794 if (cell->type == "$cover")
795 decls.push_back(stringf("(define-fun |%s_%c %d| ((state |%s_s|)) Bool (and %s %s)) ; %s\n",
796 get_id(module), postfix, id, get_id(module), name_a.c_str(), name_en.c_str(), get_id(cell)));
797 else
798 decls.push_back(stringf("(define-fun |%s_%c %d| ((state |%s_s|)) Bool (or %s (not %s))) ; %s\n",
799 get_id(module), postfix, id, get_id(module), name_a.c_str(), name_en.c_str(), get_id(cell)));
800
801 if (cell->type == "$assert")
802 assert_list.push_back(stringf("(|%s_a %d| state)", get_id(module), id));
803 else if (cell->type == "$assume")
804 assume_list.push_back(stringf("(|%s_u %d| state)", get_id(module), id));
805
806 id++;
807 }
808 }
809
810 if (verbose) log("=> export logic driving hierarchical cells\n");
811
812 for (auto cell : module->cells())
813 if (module->design->module(cell->type) != nullptr)
814 export_cell(cell);
815
816 while (!hiercells_queue.empty())
817 {
818 std::set<RTLIL::Cell*> queue;
819 queue.swap(hiercells_queue);
820
821 for (auto cell : queue)
822 {
823 string cell_state = stringf("(|%s_h %s| state)", get_id(module), get_id(cell->name));
824 Module *m = module->design->module(cell->type);
825 log_assert(m != nullptr);
826
827 hier.push_back(stringf(" (= (|%s_is| state) (|%s_is| %s))\n",
828 get_id(module), get_id(cell->type), cell_state.c_str()));
829
830 for (auto &conn : cell->connections())
831 {
832 Wire *w = m->wire(conn.first);
833 SigSpec sig = sigmap(conn.second);
834
835 if (bvmode || GetSize(w) == 1) {
836 hier.push_back(stringf(" (= %s (|%s_n %s| %s)) ; %s.%s\n", (GetSize(w) > 1 ? get_bv(sig) : get_bool(sig)).c_str(),
837 get_id(cell->type), get_id(w), cell_state.c_str(), get_id(cell->type), get_id(w)));
838 } else {
839 for (int i = 0; i < GetSize(w); i++)
840 hier.push_back(stringf(" (= %s (|%s_n %s %d| %s)) ; %s.%s[%d]\n", get_bool(sig[i]).c_str(),
841 get_id(cell->type), get_id(w), i, cell_state.c_str(), get_id(cell->type), get_id(w), i));
842 }
843 }
844 }
845 }
846
847 for (int iter = 1; !registers.empty(); iter++)
848 {
849 pool<Cell*> this_regs;
850 this_regs.swap(registers);
851
852 if (verbose) log("=> export logic driving registers [iteration %d]\n", iter);
853
854 for (auto cell : this_regs)
855 {
856 if (cell->type.in("$_FF_", "$_DFF_P_", "$_DFF_N_"))
857 {
858 std::string expr_d = get_bool(cell->getPort("\\D"));
859 std::string expr_q = get_bool(cell->getPort("\\Q"), "next_state");
860 trans.push_back(stringf(" (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell), log_signal(cell->getPort("\\Q"))));
861 }
862
863 if (cell->type.in("$ff", "$dff"))
864 {
865 std::string expr_d = get_bv(cell->getPort("\\D"));
866 std::string expr_q = get_bv(cell->getPort("\\Q"), "next_state");
867 trans.push_back(stringf(" (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell), log_signal(cell->getPort("\\Q"))));
868 }
869
870 if (cell->type == "$anyconst")
871 {
872 std::string expr_d = get_bv(cell->getPort("\\Y"));
873 std::string expr_q = get_bv(cell->getPort("\\Y"), "next_state");
874 trans.push_back(stringf(" (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell), log_signal(cell->getPort("\\Y"))));
875 }
876
877 if (cell->type == "$mem")
878 {
879 int arrayid = memarrays.at(cell);
880
881 int abits = cell->getParam("\\ABITS").as_int();
882 int width = cell->getParam("\\WIDTH").as_int();
883 int wr_ports = cell->getParam("\\WR_PORTS").as_int();
884
885 bool async_read = false;
886 string initial_memstate, final_memstate;
887
888 if (!cell->getParam("\\WR_CLK_ENABLE").is_fully_ones()) {
889 log_assert(cell->getParam("\\WR_CLK_ENABLE").is_fully_zero());
890 async_read = true;
891 initial_memstate = stringf("%s#%d#0", get_id(module), arrayid);
892 final_memstate = stringf("%s#%d#final", get_id(module), arrayid);
893 }
894
895 if (statebv)
896 {
897 int mem_size = cell->getParam("\\SIZE").as_int();
898 int mem_offset = cell->getParam("\\OFFSET").as_int();
899
900 if (async_read) {
901 makebits(final_memstate, width*mem_size, get_id(cell));
902 }
903
904 for (int i = 0; i < wr_ports; i++)
905 {
906 SigSpec addr_sig = cell->getPort("\\WR_ADDR").extract(abits*i, abits);
907 SigSpec data_sig = cell->getPort("\\WR_DATA").extract(width*i, width);
908 SigSpec mask_sig = cell->getPort("\\WR_EN").extract(width*i, width);
909
910 std::string addr = get_bv(addr_sig);
911 std::string data = get_bv(data_sig);
912 std::string mask = get_bv(mask_sig);
913
914 decls.push_back(stringf("(define-fun |%s_m:W%dA %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
915 get_id(module), i, get_id(cell), get_id(module), abits, addr.c_str(), log_signal(addr_sig)));
916 addr = stringf("(|%s_m:W%dA %s| state)", get_id(module), i, get_id(cell));
917
918 decls.push_back(stringf("(define-fun |%s_m:W%dD %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
919 get_id(module), i, get_id(cell), get_id(module), width, data.c_str(), log_signal(data_sig)));
920 data = stringf("(|%s_m:W%dD %s| state)", get_id(module), i, get_id(cell));
921
922 decls.push_back(stringf("(define-fun |%s_m:W%dM %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
923 get_id(module), i, get_id(cell), get_id(module), width, mask.c_str(), log_signal(mask_sig)));
924 mask = stringf("(|%s_m:W%dM %s| state)", get_id(module), i, get_id(cell));
925
926 std::string data_expr;
927
928 for (int k = mem_size-1; k >= 0; k--) {
929 std::string new_data = stringf("(bvor (bvand %s %s) (bvand ((_ extract %d %d) (|%s#%d#%d| state)) (bvnot %s)))",
930 data.c_str(), mask.c_str(), width*(k+1)-1, width*k, get_id(module), arrayid, i, mask.c_str());
931 data_expr += stringf("\n (ite (= %s #b%s) %s ((_ extract %d %d) (|%s#%d#%d| state)))",
932 addr.c_str(), Const(k+mem_offset, abits).as_string().c_str(), new_data.c_str(),
933 width*(k+1)-1, width*k, get_id(module), arrayid, i);
934 }
935
936 decls.push_back(stringf("(define-fun |%s#%d#%d| ((state |%s_s|)) (_ BitVec %d) (concat%s)) ; %s\n",
937 get_id(module), arrayid, i+1, get_id(module), width*mem_size, data_expr.c_str(), get_id(cell)));
938 }
939 }
940 else
941 {
942 if (async_read) {
943 if (statedt)
944 dtmembers.push_back(stringf(" (|%s| (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n",
945 initial_memstate.c_str(), abits, width, get_id(cell)));
946 else
947 decls.push_back(stringf("(declare-fun |%s| (|%s_s|) (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n",
948 initial_memstate.c_str(), get_id(module), abits, width, get_id(cell)));
949 }
950
951 for (int i = 0; i < wr_ports; i++)
952 {
953 SigSpec addr_sig = cell->getPort("\\WR_ADDR").extract(abits*i, abits);
954 SigSpec data_sig = cell->getPort("\\WR_DATA").extract(width*i, width);
955 SigSpec mask_sig = cell->getPort("\\WR_EN").extract(width*i, width);
956
957 std::string addr = get_bv(addr_sig);
958 std::string data = get_bv(data_sig);
959 std::string mask = get_bv(mask_sig);
960
961 decls.push_back(stringf("(define-fun |%s_m:W%dA %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
962 get_id(module), i, get_id(cell), get_id(module), abits, addr.c_str(), log_signal(addr_sig)));
963 addr = stringf("(|%s_m:W%dA %s| state)", get_id(module), i, get_id(cell));
964
965 decls.push_back(stringf("(define-fun |%s_m:W%dD %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
966 get_id(module), i, get_id(cell), get_id(module), width, data.c_str(), log_signal(data_sig)));
967 data = stringf("(|%s_m:W%dD %s| state)", get_id(module), i, get_id(cell));
968
969 decls.push_back(stringf("(define-fun |%s_m:W%dM %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
970 get_id(module), i, get_id(cell), get_id(module), width, mask.c_str(), log_signal(mask_sig)));
971 mask = stringf("(|%s_m:W%dM %s| state)", get_id(module), i, get_id(cell));
972
973 data = stringf("(bvor (bvand %s %s) (bvand (select (|%s#%d#%d| state) %s) (bvnot %s)))",
974 data.c_str(), mask.c_str(), get_id(module), arrayid, i, addr.c_str(), mask.c_str());
975
976 decls.push_back(stringf("(define-fun |%s#%d#%d| ((state |%s_s|)) (Array (_ BitVec %d) (_ BitVec %d)) "
977 "(store (|%s#%d#%d| state) %s %s)) ; %s\n",
978 get_id(module), arrayid, i+1, get_id(module), abits, width,
979 get_id(module), arrayid, i, addr.c_str(), data.c_str(), get_id(cell)));
980 }
981 }
982
983 std::string expr_d = stringf("(|%s#%d#%d| state)", get_id(module), arrayid, wr_ports);
984 std::string expr_q = stringf("(|%s#%d#0| next_state)", get_id(module), arrayid);
985 trans.push_back(stringf(" (= %s %s) ; %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell)));
986
987 if (async_read)
988 hier.push_back(stringf(" (= %s (|%s| state)) ; %s\n", expr_d.c_str(), final_memstate.c_str(), get_id(cell)));
989
990 Const init_data = cell->getParam("\\INIT");
991 int memsize = cell->getParam("\\SIZE").as_int();
992
993 for (int i = 0; i < memsize; i++)
994 {
995 if (i*width >= GetSize(init_data))
996 break;
997
998 Const initword = init_data.extract(i*width, width, State::Sx);
999 bool gen_init_constr = false;
1000
1001 for (auto bit : initword.bits)
1002 if (bit == State::S0 || bit == State::S1)
1003 gen_init_constr = true;
1004
1005 if (gen_init_constr)
1006 {
1007 if (statebv)
1008 /* FIXME */;
1009 else
1010 init_list.push_back(stringf("(= (select (|%s#%d#0| state) #b%s) #b%s) ; %s[%d]",
1011 get_id(module), arrayid, Const(i, abits).as_string().c_str(),
1012 initword.as_string().c_str(), get_id(cell), i));
1013 }
1014 }
1015 }
1016 }
1017 }
1018
1019 if (verbose) log("=> finalizing SMT2 representation of %s.\n", log_id(module));
1020
1021 for (auto c : hiercells) {
1022 assert_list.push_back(stringf("(|%s_a| (|%s_h %s| state))", get_id(c->type), get_id(module), get_id(c->name)));
1023 assume_list.push_back(stringf("(|%s_u| (|%s_h %s| state))", get_id(c->type), get_id(module), get_id(c->name)));
1024 init_list.push_back(stringf("(|%s_i| (|%s_h %s| state))", get_id(c->type), get_id(module), get_id(c->name)));
1025 hier.push_back(stringf(" (|%s_h| (|%s_h %s| state))\n", get_id(c->type), get_id(module), get_id(c->name)));
1026 trans.push_back(stringf(" (|%s_t| (|%s_h %s| state) (|%s_h %s| next_state))\n",
1027 get_id(c->type), get_id(module), get_id(c->name), get_id(module), get_id(c->name)));
1028 }
1029
1030 string assert_expr = assert_list.empty() ? "true" : "(and";
1031 if (!assert_list.empty()) {
1032 if (GetSize(assert_list) == 1) {
1033 assert_expr = "\n " + assert_list.front() + "\n";
1034 } else {
1035 for (auto &str : assert_list)
1036 assert_expr += stringf("\n %s", str.c_str());
1037 assert_expr += "\n)";
1038 }
1039 }
1040 decls.push_back(stringf("(define-fun |%s_a| ((state |%s_s|)) Bool %s)\n",
1041 get_id(module), get_id(module), assert_expr.c_str()));
1042
1043 string assume_expr = assume_list.empty() ? "true" : "(and";
1044 if (!assume_list.empty()) {
1045 if (GetSize(assume_list) == 1) {
1046 assume_expr = "\n " + assume_list.front() + "\n";
1047 } else {
1048 for (auto &str : assume_list)
1049 assume_expr += stringf("\n %s", str.c_str());
1050 assume_expr += "\n)";
1051 }
1052 }
1053 decls.push_back(stringf("(define-fun |%s_u| ((state |%s_s|)) Bool %s)\n",
1054 get_id(module), get_id(module), assume_expr.c_str()));
1055
1056 string init_expr = init_list.empty() ? "true" : "(and";
1057 if (!init_list.empty()) {
1058 if (GetSize(init_list) == 1) {
1059 init_expr = "\n " + init_list.front() + "\n";
1060 } else {
1061 for (auto &str : init_list)
1062 init_expr += stringf("\n %s", str.c_str());
1063 init_expr += "\n)";
1064 }
1065 }
1066 decls.push_back(stringf("(define-fun |%s_i| ((state |%s_s|)) Bool %s)\n",
1067 get_id(module), get_id(module), init_expr.c_str()));
1068 }
1069
1070 void write(std::ostream &f)
1071 {
1072 f << stringf("; yosys-smt2-module %s\n", get_id(module));
1073
1074 if (statebv) {
1075 f << stringf("(define-sort |%s_s| () (_ BitVec %d))\n", get_id(module), statebv_width);
1076 mod_stbv_width[module->name] = statebv_width;
1077 } else
1078 if (statedt) {
1079 f << stringf("(declare-datatype |%s_s| ((|%s_mk|\n", get_id(module), get_id(module));
1080 for (auto it : dtmembers)
1081 f << it;
1082 f << stringf(")))\n");
1083 } else
1084 f << stringf("(declare-sort |%s_s| 0)\n", get_id(module));
1085
1086 for (auto it : decls)
1087 f << it;
1088
1089 f << stringf("(define-fun |%s_h| ((state |%s_s|)) Bool ", get_id(module), get_id(module));
1090 if (GetSize(hier) > 1) {
1091 f << "(and\n";
1092 for (auto it : hier)
1093 f << it;
1094 f << "))\n";
1095 } else
1096 if (GetSize(hier) == 1)
1097 f << "\n" + hier.front() + ")\n";
1098 else
1099 f << "true)\n";
1100
1101 f << stringf("(define-fun |%s_t| ((state |%s_s|) (next_state |%s_s|)) Bool ", get_id(module), get_id(module), get_id(module));
1102 if (GetSize(trans) > 1) {
1103 f << "(and\n";
1104 for (auto it : trans)
1105 f << it;
1106 f << "))";
1107 } else
1108 if (GetSize(trans) == 1)
1109 f << "\n" + trans.front() + ")";
1110 else
1111 f << "true)";
1112 f << stringf(" ; end of module %s\n", get_id(module));
1113 }
1114 };
1115
1116 struct Smt2Backend : public Backend {
1117 Smt2Backend() : Backend("smt2", "write design to SMT-LIBv2 file") { }
1118 virtual void help()
1119 {
1120 // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
1121 log("\n");
1122 log(" write_smt2 [options] [filename]\n");
1123 log("\n");
1124 log("Write a SMT-LIBv2 [1] description of the current design. For a module with name\n");
1125 log("'<mod>' this will declare the sort '<mod>_s' (state of the module) and will\n");
1126 log("define and declare functions operating on that state.\n");
1127 log("\n");
1128 log("The following SMT2 functions are generated for a module with name '<mod>'.\n");
1129 log("Some declarations/definitions are printed with a special comment. A prover\n");
1130 log("using the SMT2 files can use those comments to collect all relevant metadata\n");
1131 log("about the design.\n");
1132 log("\n");
1133 log(" ; yosys-smt2-module <mod>\n");
1134 log(" (declare-sort |<mod>_s| 0)\n");
1135 log(" The sort representing a state of module <mod>.\n");
1136 log("\n");
1137 log(" (define-fun |<mod>_h| ((state |<mod>_s|)) Bool (...))\n");
1138 log(" This function must be asserted for each state to establish the\n");
1139 log(" design hierarchy.\n");
1140 log("\n");
1141 log(" ; yosys-smt2-input <wirename> <width>\n");
1142 log(" ; yosys-smt2-output <wirename> <width>\n");
1143 log(" ; yosys-smt2-register <wirename> <width>\n");
1144 log(" ; yosys-smt2-wire <wirename> <width>\n");
1145 log(" (define-fun |<mod>_n <wirename>| (|<mod>_s|) (_ BitVec <width>))\n");
1146 log(" (define-fun |<mod>_n <wirename>| (|<mod>_s|) Bool)\n");
1147 log(" For each port, register, and wire with the 'keep' attribute set an\n");
1148 log(" accessor function is generated. Single-bit wires are returned as Bool,\n");
1149 log(" multi-bit wires as BitVec.\n");
1150 log("\n");
1151 log(" ; yosys-smt2-cell <submod> <instancename>\n");
1152 log(" (declare-fun |<mod>_h <instancename>| (|<mod>_s|) |<submod>_s|)\n");
1153 log(" There is a function like that for each hierarchical instance. It\n");
1154 log(" returns the sort that represents the state of the sub-module that\n");
1155 log(" implements the instance.\n");
1156 log("\n");
1157 log(" (declare-fun |<mod>_is| (|<mod>_s|) Bool)\n");
1158 log(" This function must be asserted 'true' for initial states, and 'false'\n");
1159 log(" otherwise.\n");
1160 log("\n");
1161 log(" (define-fun |<mod>_i| ((state |<mod>_s|)) Bool (...))\n");
1162 log(" This function must be asserted 'true' for initial states. For\n");
1163 log(" non-initial states it must be left unconstrained.\n");
1164 log("\n");
1165 log(" (define-fun |<mod>_t| ((state |<mod>_s|) (next_state |<mod>_s|)) Bool (...))\n");
1166 log(" This function evaluates to 'true' if the states 'state' and\n");
1167 log(" 'next_state' form a valid state transition.\n");
1168 log("\n");
1169 log(" (define-fun |<mod>_a| ((state |<mod>_s|)) Bool (...))\n");
1170 log(" This function evaluates to 'true' if all assertions hold in the state.\n");
1171 log("\n");
1172 log(" (define-fun |<mod>_u| ((state |<mod>_s|)) Bool (...))\n");
1173 log(" This function evaluates to 'true' if all assumptions hold in the state.\n");
1174 log("\n");
1175 log(" ; yosys-smt2-assert <id> <filename:linenum>\n");
1176 log(" (define-fun |<mod>_a <id>| ((state |<mod>_s|)) Bool (...))\n");
1177 log(" Each $assert cell is converted into one of this functions. The function\n");
1178 log(" evaluates to 'true' if the assert statement holds in the state.\n");
1179 log("\n");
1180 log(" ; yosys-smt2-assume <id> <filename:linenum>\n");
1181 log(" (define-fun |<mod>_u <id>| ((state |<mod>_s|)) Bool (...))\n");
1182 log(" Each $assume cell is converted into one of this functions. The function\n");
1183 log(" evaluates to 'true' if the assume statement holds in the state.\n");
1184 log("\n");
1185 log(" ; yosys-smt2-cover <id> <filename:linenum>\n");
1186 log(" (define-fun |<mod>_c <id>| ((state |<mod>_s|)) Bool (...))\n");
1187 log(" Each $cover cell is converted into one of this functions. The function\n");
1188 log(" evaluates to 'true' if the cover statement is activated in the state.\n");
1189 log("\n");
1190 log("Options:\n");
1191 log("\n");
1192 log(" -verbose\n");
1193 log(" this will print the recursive walk used to export the modules.\n");
1194 log("\n");
1195 log(" -stbv\n");
1196 log(" Use a BitVec sort to represent a state instead of an uninterpreted\n");
1197 log(" sort. As a side-effect this will prevent use of arrays to model\n");
1198 log(" memories.\n");
1199 log("\n");
1200 log(" -stdt\n");
1201 log(" Use SMT-LIB 2.6 style datatypes to represent a state instead of an\n");
1202 log(" uninterpreted sort.\n");
1203 log("\n");
1204 log(" -nobv\n");
1205 log(" disable support for BitVec (FixedSizeBitVectors theory). without this\n");
1206 log(" option multi-bit wires are represented using the BitVec sort and\n");
1207 log(" support for coarse grain cells (incl. arithmetic) is enabled.\n");
1208 log("\n");
1209 log(" -nomem\n");
1210 log(" disable support for memories (via ArraysEx theory). this option is\n");
1211 log(" implied by -nobv. only $mem cells without merged registers in\n");
1212 log(" read ports are supported. call \"memory\" with -nordff to make sure\n");
1213 log(" that no registers are merged into $mem read ports. '<mod>_m' functions\n");
1214 log(" will be generated for accessing the arrays that are used to represent\n");
1215 log(" memories.\n");
1216 log("\n");
1217 log(" -wires\n");
1218 log(" create '<mod>_n' functions for all public wires. by default only ports,\n");
1219 log(" registers, and wires with the 'keep' attribute are exported.\n");
1220 log("\n");
1221 log(" -tpl <template_file>\n");
1222 log(" use the given template file. the line containing only the token '%%%%'\n");
1223 log(" is replaced with the regular output of this command.\n");
1224 log("\n");
1225 log("[1] For more information on SMT-LIBv2 visit http://smt-lib.org/ or read David\n");
1226 log("R. Cok's tutorial: http://www.grammatech.com/resources/smt/SMTLIBTutorial.pdf\n");
1227 log("\n");
1228 log("---------------------------------------------------------------------------\n");
1229 log("\n");
1230 log("Example:\n");
1231 log("\n");
1232 log("Consider the following module (test.v). We want to prove that the output can\n");
1233 log("never transition from a non-zero value to a zero value.\n");
1234 log("\n");
1235 log(" module test(input clk, output reg [3:0] y);\n");
1236 log(" always @(posedge clk)\n");
1237 log(" y <= (y << 1) | ^y;\n");
1238 log(" endmodule\n");
1239 log("\n");
1240 log("For this proof we create the following template (test.tpl).\n");
1241 log("\n");
1242 log(" ; we need QF_UFBV for this poof\n");
1243 log(" (set-logic QF_UFBV)\n");
1244 log("\n");
1245 log(" ; insert the auto-generated code here\n");
1246 log(" %%%%\n");
1247 log("\n");
1248 log(" ; declare two state variables s1 and s2\n");
1249 log(" (declare-fun s1 () test_s)\n");
1250 log(" (declare-fun s2 () test_s)\n");
1251 log("\n");
1252 log(" ; state s2 is the successor of state s1\n");
1253 log(" (assert (test_t s1 s2))\n");
1254 log("\n");
1255 log(" ; we are looking for a model with y non-zero in s1\n");
1256 log(" (assert (distinct (|test_n y| s1) #b0000))\n");
1257 log("\n");
1258 log(" ; we are looking for a model with y zero in s2\n");
1259 log(" (assert (= (|test_n y| s2) #b0000))\n");
1260 log("\n");
1261 log(" ; is there such a model?\n");
1262 log(" (check-sat)\n");
1263 log("\n");
1264 log("The following yosys script will create a 'test.smt2' file for our proof:\n");
1265 log("\n");
1266 log(" read_verilog test.v\n");
1267 log(" hierarchy -check; proc; opt; check -assert\n");
1268 log(" write_smt2 -bv -tpl test.tpl test.smt2\n");
1269 log("\n");
1270 log("Running 'cvc4 test.smt2' will print 'unsat' because y can never transition\n");
1271 log("from non-zero to zero in the test design.\n");
1272 log("\n");
1273 }
1274 virtual void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design)
1275 {
1276 std::ifstream template_f;
1277 bool bvmode = true, memmode = true, wiresmode = false, verbose = false, statebv = false, statedt = false;
1278
1279 log_header(design, "Executing SMT2 backend.\n");
1280
1281 size_t argidx;
1282 for (argidx = 1; argidx < args.size(); argidx++)
1283 {
1284 if (args[argidx] == "-tpl" && argidx+1 < args.size()) {
1285 template_f.open(args[++argidx]);
1286 if (template_f.fail())
1287 log_error("Can't open template file `%s'.\n", args[argidx].c_str());
1288 continue;
1289 }
1290 if (args[argidx] == "-bv" || args[argidx] == "-mem") {
1291 log_warning("Options -bv and -mem are now the default. Support for -bv and -mem will be removed in the future.\n");
1292 continue;
1293 }
1294 if (args[argidx] == "-stbv") {
1295 statebv = true;
1296 statedt = false;
1297 continue;
1298 }
1299 if (args[argidx] == "-stdt") {
1300 statebv = false;
1301 statedt = true;
1302 continue;
1303 }
1304 if (args[argidx] == "-nobv") {
1305 bvmode = false;
1306 memmode = false;
1307 continue;
1308 }
1309 if (args[argidx] == "-nomem") {
1310 memmode = false;
1311 continue;
1312 }
1313 if (args[argidx] == "-wires") {
1314 wiresmode = true;
1315 continue;
1316 }
1317 if (args[argidx] == "-verbose") {
1318 verbose = true;
1319 continue;
1320 }
1321 break;
1322 }
1323 extra_args(f, filename, args, argidx);
1324
1325 if (template_f.is_open()) {
1326 std::string line;
1327 while (std::getline(template_f, line)) {
1328 int indent = 0;
1329 while (indent < GetSize(line) && (line[indent] == ' ' || line[indent] == '\t'))
1330 indent++;
1331 if (line.substr(indent, 2) == "%%")
1332 break;
1333 *f << line << std::endl;
1334 }
1335 }
1336
1337 *f << stringf("; SMT-LIBv2 description generated by %s\n", yosys_version_str);
1338
1339 if (!bvmode)
1340 *f << stringf("; yosys-smt2-nobv\n");
1341
1342 if (!memmode)
1343 *f << stringf("; yosys-smt2-nomem\n");
1344
1345 if (statebv)
1346 *f << stringf("; yosys-smt2-stbv\n");
1347
1348 if (statedt)
1349 *f << stringf("; yosys-smt2-stdt\n");
1350
1351 std::vector<RTLIL::Module*> sorted_modules;
1352
1353 // extract module dependencies
1354 std::map<RTLIL::Module*, std::set<RTLIL::Module*>> module_deps;
1355 for (auto &mod_it : design->modules_) {
1356 module_deps[mod_it.second] = std::set<RTLIL::Module*>();
1357 for (auto &cell_it : mod_it.second->cells_)
1358 if (design->modules_.count(cell_it.second->type) > 0)
1359 module_deps[mod_it.second].insert(design->modules_.at(cell_it.second->type));
1360 }
1361
1362 // simple good-enough topological sort
1363 // (O(n*m) on n elements and depth m)
1364 while (module_deps.size() > 0) {
1365 size_t sorted_modules_idx = sorted_modules.size();
1366 for (auto &it : module_deps) {
1367 for (auto &dep : it.second)
1368 if (module_deps.count(dep) > 0)
1369 goto not_ready_yet;
1370 // log("Next in topological sort: %s\n", RTLIL::id2cstr(it.first->name));
1371 sorted_modules.push_back(it.first);
1372 not_ready_yet:;
1373 }
1374 if (sorted_modules_idx == sorted_modules.size())
1375 log_error("Cyclic dependency between modules found! Cycle includes module %s.\n", RTLIL::id2cstr(module_deps.begin()->first->name));
1376 while (sorted_modules_idx < sorted_modules.size())
1377 module_deps.erase(sorted_modules.at(sorted_modules_idx++));
1378 }
1379
1380 dict<IdString, int> mod_stbv_width;
1381 Module *topmod = design->top_module();
1382 std::string topmod_id;
1383
1384 for (auto module : sorted_modules)
1385 {
1386 if (module->get_bool_attribute("\\blackbox") || module->has_memories_warn() || module->has_processes_warn())
1387 continue;
1388
1389 log("Creating SMT-LIBv2 representation of module %s.\n", log_id(module));
1390
1391 Smt2Worker worker(module, bvmode, memmode, wiresmode, verbose, statebv, statedt, mod_stbv_width);
1392 worker.run();
1393 worker.write(*f);
1394
1395 if (module == topmod)
1396 topmod_id = worker.get_id(module);
1397 }
1398
1399 if (topmod)
1400 *f << stringf("; yosys-smt2-topmod %s\n", topmod_id.c_str());
1401
1402 *f << stringf("; end of yosys output\n");
1403
1404 if (template_f.is_open()) {
1405 std::string line;
1406 while (std::getline(template_f, line))
1407 *f << line << std::endl;
1408 }
1409 }
1410 } Smt2Backend;
1411
1412 PRIVATE_NAMESPACE_END