projects / yosys.git / blob
? search:
summary | shortlog | log | commit | commitdiff | tree
history | raw | HEAD
Progress in SMV back-end
[yosys.git] / backends / smv / smv.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 SmvWorker
31 {
32 CellTypes ct;
33 SigMap sigmap;
34 RTLIL::Module *module;
35 std::ostream &f;
36 bool verbose;
37
38 int idcounter;
39 dict<IdString, shared_str> idcache;
40 pool<shared_str> used_names;
41 vector<shared_str> strbuf;
42
43 pool<Wire*> partial_assignment_wires;
44 dict<SigBit, std::pair<const char*, int>> partial_assignment_bits;
45 vector<string> assignments;
46
47 const char *cid()
48 {
49 while (true) {
50 shared_str s(stringf("_%d", idcounter++));
51 if (!used_names.count(s)) {
52 used_names.insert(s);
53 return s.c_str();
54 }
55 }
56 }
57
58 const char *cid(IdString id, bool precache = false)
59 {
60 if (!idcache.count(id))
61 {
62 string name = stringf("_%s", id.c_str());
63
64 if (name.substr(0, 2) == "_\\")
65 name = "_" + name.substr(2);
66
67 for (auto &c : name) {
68 if (c == '|' || c == '$' || c == '_') continue;
69 if (c >= 'a' && c <='z') continue;
70 if (c >= 'A' && c <='Z') continue;
71 if (c >= '0' && c <='9') continue;
72 if (precache) return nullptr;
73 c = '#';
74 }
75
76 if (name == "_main")
77 name = "main";
78
79 while (used_names.count(name))
80 name += "_";
81
82 shared_str s(name);
83 used_names.insert(s);
84 idcache[id] = s;
85 }
86
87 return idcache.at(id).c_str();
88 }
89
90 SmvWorker(RTLIL::Module *module, bool verbose, std::ostream &f) :
91 ct(module->design), sigmap(module), module(module), f(f), verbose(verbose), idcounter(0)
92 {
93 for (auto mod : module->design->modules())
94 cid(mod->name, true);
95
96 for (auto wire : module->wires())
97 cid(wire->name, true);
98
99 for (auto cell : module->cells()) {
100 cid(cell->name, true);
101 cid(cell->type, true);
102 for (auto &conn : cell->connections())
103 cid(conn.first, true);
104 }
105 }
106
107 const char *rvalue(SigSpec sig, int width = -1, bool is_signed = false)
108 {
109 string s;
110 int count_chunks = 0;
111 sigmap.apply(sig);
112
113 for (int i = 0; i < GetSize(sig); i++)
114 if (partial_assignment_bits.count(sig[i]))
115 {
116 int width = 1;
117 const auto &bit_a = partial_assignment_bits.at(sig[i]);
118
119 while (i+width < GetSize(sig))
120 {
121 if (!partial_assignment_bits.count(sig[i+width]))
122 break;
123
124 const auto &bit_b = partial_assignment_bits.at(sig[i+width]);
125 if (strcmp(bit_a.first, bit_b.first))
126 break;
127 if (bit_a.second+width != bit_b.second)
128 break;
129
130 width++;
131 }
132
133 if (i+width < GetSize(sig))
134 s = stringf("%s :: ", rvalue(sig.extract(i+width, GetSize(sig)-(width+i))));
135
136 s += stringf("%s[%d:%d]", bit_a.first, bit_a.second+width-1, bit_a.second);
137
138 if (i > 0)
139 s += stringf(" :: %s", rvalue(sig.extract(0, i)));
140
141 count_chunks = 3;
142 goto continue_with_resize;
143 }
144
145 for (auto &c : sig.chunks()) {
146 count_chunks++;
147 if (!s.empty())
148 s = " :: " + s;
149 if (c.wire) {
150 if (c.offset != 0 || c.width != c.wire->width)
151 s = stringf("%s[%d:%d]", cid(c.wire->name), c.offset+c.width-1, c.offset) + s;
152 else
153 s = cid(c.wire->name) + s;
154 } else {
155 string v = stringf("0ub%d_", c.width);
156 for (int i = c.width-1; i >= 0; i--)
157 v += c.data.at(i) == State::S1 ? '1' : '0';
158 s = v + s;
159 }
160 }
161
162 continue_with_resize:;
163 if (width >= 0) {
164 if (is_signed) {
165 if (GetSize(sig) > width)
166 s = stringf("signed(resize(%s, %d))", s.c_str(), width);
167 else
168 s = stringf("resize(signed(%s), %d)", s.c_str(), width);
169 } else
170 s = stringf("resize(%s, %d)", s.c_str(), width);
171 } else if (is_signed)
172 s = stringf("signed(%s)", s.c_str());
173 else if (count_chunks > 1)
174 s = stringf("(%s)", s.c_str());
175
176 strbuf.push_back(s);
177 return strbuf.back().c_str();
178 }
179
180 const char *rvalue_u(SigSpec sig, int width = -1)
181 {
182 return rvalue(sig, width, false);
183 }
184
185 const char *rvalue_s(SigSpec sig, int width = -1, bool is_signed = true)
186 {
187 return rvalue(sig, width, is_signed);
188 }
189
190 const char *lvalue(SigSpec sig)
191 {
192 sigmap.apply(sig);
193
194 if (sig.is_wire())
195 return rvalue(sig);
196
197 const char *temp_id = cid();
198 f << stringf(" %s : unsigned word[%d]; -- %s\n", temp_id, GetSize(sig), log_signal(sig));
199
200 int offset = 0;
201 for (auto bit : sig) {
202 log_assert(bit.wire != nullptr);
203 partial_assignment_wires.insert(bit.wire);
204 partial_assignment_bits[bit] = std::pair<const char*, int>(temp_id, offset++);
205 }
206
207 return temp_id;
208 }
209
210 void run()
211 {
212 f << stringf("MODULE %s\n", cid(module->name));
213 f << stringf(" VAR\n");
214
215 for (auto wire : module->wires())
216 {
217 if (SigSpec(wire) != sigmap(wire))
218 partial_assignment_wires.insert(wire);
219
220 f << stringf(" %s : unsigned word[%d]; -- %s\n", cid(wire->name), wire->width, log_id(wire));
221 }
222
223 for (auto cell : module->cells())
224 {
225 // FIXME: $slice, $concat, $mem
226
227 if (cell->type.in("$shl", "$shr", "$sshl", "$sshr", "$shift", "$shiftx"))
228 {
229 SigSpec sig_a = cell->getPort("\\A");
230 SigSpec sig_b = cell->getPort("\\B");
231
232 int width_y = GetSize(cell->getPort("\\Y"));
233 int shift_b_width = GetSize(sig_b);
234 int width_ay = std::max(GetSize(sig_a), width_y);
235 int width = width_ay;
236
237 for (int i = 1, j = 0;; i <<= 1, j++)
238 if (width_ay < i) {
239 width = i-1;
240 shift_b_width = std::min(shift_b_width, j);
241 break;
242 }
243
244 bool signed_a = cell->getParam("\\A_SIGNED").as_bool();
245 bool signed_b = cell->getParam("\\B_SIGNED").as_bool();
246 string op = cell->type.in("$shl", "$sshl") ? "<<" : ">>";
247 string expr, expr_a;
248
249 if (cell->type == "$sshr" && signed_a)
250 {
251 expr_a = rvalue_s(sig_a, width);
252 expr = stringf("resize(unsigned(%s %s %s), %d)", expr_a.c_str(), op.c_str(), rvalue(sig_b.extract(0, shift_b_width)), width_y);
253 if (shift_b_width < GetSize(sig_b))
254 expr = stringf("%s != 0ud%d_0 ? (bool(%s) ? !0ud%d_0 : 0ud%d_0) : %s",
255 rvalue(sig_b.extract(shift_b_width, GetSize(sig_b) - shift_b_width)), GetSize(sig_b) - shift_b_width,
256 rvalue(sig_a[GetSize(sig_a)-1]), width_y, width_y, expr.c_str());
257 }
258 else if (cell->type.in("$shift", "$shiftx") && signed_b)
259 {
260 expr_a = rvalue_u(sig_a, width);
261
262 const char *b_shr = rvalue_u(sig_b);
263 const char *b_shl = cid();
264
265 f << stringf(" %s : unsigned word[%d]; -- neg(%s)\n", b_shl, GetSize(sig_b), log_signal(sig_b));
266 assignments.push_back(stringf("%s := unsigned(-%s);", b_shl, rvalue_s(sig_b)));
267
268 string expr_shl = stringf("resize(%s << %s[%d:0], %d)", expr_a.c_str(), b_shl, shift_b_width-1, width_y);
269 string expr_shr = stringf("resize(%s >> %s[%d:0], %d)", expr_a.c_str(), b_shr, shift_b_width-1, width_y);
270
271 if (shift_b_width < GetSize(sig_b)) {
272 expr_shl = stringf("%s[%d:%d] != 0ud%d_0 ? 0ud%d_0 : %s", b_shl, GetSize(sig_b)-1, shift_b_width,
273 GetSize(sig_b)-shift_b_width, width_y, expr_shl.c_str());
274 expr_shr = stringf("%s[%d:%d] != 0ud%d_0 ? 0ud%d_0 : %s", b_shr, GetSize(sig_b)-1, shift_b_width,
275 GetSize(sig_b)-shift_b_width, width_y, expr_shr.c_str());
276 }
277
278 expr = stringf("bool(%s) ? %s : %s", rvalue(sig_b[GetSize(sig_b)-1]), expr_shl.c_str(), expr_shr.c_str());
279 }
280 else
281 {
282 if (cell->type.in("$shift", "$shiftx") || !signed_a)
283 expr_a = rvalue_u(sig_a, width);
284 else
285 expr_a = stringf("resize(unsigned(%s), %d)", rvalue_s(sig_a, width_ay), width);
286
287 expr = stringf("resize(%s %s %s[%d:0], %d)", expr_a.c_str(), op.c_str(), rvalue_u(sig_b), shift_b_width-1, width_y);
288 if (shift_b_width < GetSize(sig_b))
289 expr = stringf("%s[%d:%d] != 0ud%d_0 ? 0ud%d_0 : %s", rvalue_u(sig_b), GetSize(sig_b)-1, shift_b_width,
290 GetSize(sig_b)-shift_b_width, width_y, expr.c_str());
291 }
292
293 assignments.push_back(stringf("%s := %s;", lvalue(cell->getPort("\\Y")), expr.c_str()));
294
295 continue;
296 }
297
298 if (cell->type.in("$not", "$pos", "$neg"))
299 {
300 int width = GetSize(cell->getPort("\\Y"));
301 string expr_a, op;
302
303 if (cell->type == "$not") op = "!";
304 if (cell->type == "$pos") op = "";
305 if (cell->type == "$neg") op = "-";
306
307 if (cell->getParam("\\A_SIGNED").as_bool())
308 {
309 assignments.push_back(stringf("%s := unsigned(%s%s);", lvalue(cell->getPort("\\Y")),
310 op.c_str(), rvalue_s(cell->getPort("\\A"), width)));
311 }
312 else
313 {
314 assignments.push_back(stringf("%s := %s%s;", lvalue(cell->getPort("\\Y")),
315 op.c_str(), rvalue_u(cell->getPort("\\A"), width)));
316 }
317
318 continue;
319 }
320
321 if (cell->type.in("$add", "$sub", "$mul", "$and", "$or", "$xor", "$xnor"))
322 {
323 int width = GetSize(cell->getPort("\\Y"));
324 string expr_a, expr_b, op;
325
326 if (cell->type == "$add") op = "+";
327 if (cell->type == "$sub") op = "-";
328 if (cell->type == "$mul") op = "*";
329 if (cell->type == "$and") op = "&";
330 if (cell->type == "$or") op = "|";
331 if (cell->type == "$xor") op = "xor";
332 if (cell->type == "$xnor") op = "xnor";
333
334 if (cell->getParam("\\A_SIGNED").as_bool())
335 {
336 assignments.push_back(stringf("%s := unsigned(%s %s %s);", lvalue(cell->getPort("\\Y")),
337 rvalue_s(cell->getPort("\\A"), width), op.c_str(), rvalue_s(cell->getPort("\\B"), width)));
338 }
339 else
340 {
341 assignments.push_back(stringf("%s := %s %s %s;", lvalue(cell->getPort("\\Y")),
342 rvalue_u(cell->getPort("\\A"), width), op.c_str(), rvalue_u(cell->getPort("\\B"), width)));
343 }
344
345 continue;
346 }
347
348 if (cell->type.in("$div", "$mod"))
349 {
350 int width_y = GetSize(cell->getPort("\\Y"));
351 int width = std::max(width_y, GetSize(cell->getPort("\\A")));
352 width = std::max(width, GetSize(cell->getPort("\\B")));
353 string expr_a, expr_b, op;
354
355 if (cell->type == "$div") op = "/";
356 if (cell->type == "$mod") op = "mod";
357
358 if (cell->getParam("\\A_SIGNED").as_bool())
359 {
360 assignments.push_back(stringf("%s := resize(unsigned(%s %s %s), %d);", lvalue(cell->getPort("\\Y")),
361 rvalue_s(cell->getPort("\\A"), width), op.c_str(), rvalue_s(cell->getPort("\\B"), width), width_y));
362 }
363 else
364 {
365 assignments.push_back(stringf("%s := resize(%s %s %s, %d);", lvalue(cell->getPort("\\Y")),
366 rvalue_u(cell->getPort("\\A"), width), op.c_str(), rvalue_u(cell->getPort("\\B"), width), width_y));
367 }
368
369 continue;
370 }
371
372 if (cell->type.in("$eq", "$ne", "$eqx", "$nex", "$lt", "$le", "$ge", "$gt"))
373 {
374 int width = std::max(GetSize(cell->getPort("\\A")), GetSize(cell->getPort("\\B")));
375 string expr_a, expr_b, op;
376
377 if (cell->type == "$eq") op = "=";
378 if (cell->type == "$ne") op = "!=";
379 if (cell->type == "$eqx") op = "=";
380 if (cell->type == "$nex") op = "!=";
381 if (cell->type == "$lt") op = "<";
382 if (cell->type == "$le") op = "<=";
383 if (cell->type == "$ge") op = ">=";
384 if (cell->type == "$gt") op = ">";
385
386 if (cell->getParam("\\A_SIGNED").as_bool())
387 {
388 expr_a = stringf("resize(signed(%s), %d)", rvalue(cell->getPort("\\A")), width);
389 expr_b = stringf("resize(signed(%s), %d)", rvalue(cell->getPort("\\B")), width);
390 }
391 else
392 {
393 expr_a = stringf("resize(%s, %d)", rvalue(cell->getPort("\\A")), width);
394 expr_b = stringf("resize(%s, %d)", rvalue(cell->getPort("\\B")), width);
395 }
396
397 assignments.push_back(stringf("%s := resize(word1(%s %s %s), %d);", lvalue(cell->getPort("\\Y")),
398 expr_a.c_str(), op.c_str(), expr_b.c_str(), GetSize(cell->getPort("\\Y"))));
399
400 continue;
401 }
402
403 if (cell->type.in("$reduce_and", "$reduce_or", "$reduce_bool"))
404 {
405 int width_a = GetSize(cell->getPort("\\A"));
406 int width_y = GetSize(cell->getPort("\\Y"));
407 const char *expr_a = rvalue(cell->getPort("\\A"));
408 const char *expr_y = lvalue(cell->getPort("\\Y"));
409 string expr;
410
411 if (cell->type == "$reduce_and") expr = stringf("%s = !0ub%d_0", expr_a, width_a);
412 if (cell->type == "$reduce_or") expr = stringf("%s != 0ub%d_0", expr_a, width_a);
413 if (cell->type == "$reduce_bool") expr = stringf("%s != 0ub%d_0", expr_a, width_a);
414
415 assignments.push_back(stringf("%s := resize(word1(%s), %d);", expr_y, expr.c_str(), width_y));
416 continue;
417 }
418
419 if (cell->type.in("$reduce_xor", "$reduce_xnor"))
420 {
421 int width_y = GetSize(cell->getPort("\\Y"));
422 const char *expr_y = lvalue(cell->getPort("\\Y"));
423 string expr;
424
425 for (auto bit : cell->getPort("\\A")) {
426 if (!expr.empty())
427 expr += " xor ";
428 expr += rvalue(bit);
429 }
430
431 if (cell->type == "$reduce_xnor")
432 expr = "!(" + expr + ")";
433
434 assignments.push_back(stringf("%s := resize(%s, %d);", expr_y, expr.c_str(), width_y));
435 continue;
436 }
437
438 if (cell->type.in("$logic_and", "$logic_or"))
439 {
440 int width_a = GetSize(cell->getPort("\\A"));
441 int width_b = GetSize(cell->getPort("\\B"));
442 int width_y = GetSize(cell->getPort("\\Y"));
443
444 string expr_a = stringf("(%s != 0ub%d_0)", rvalue(cell->getPort("\\A")), width_a);
445 string expr_b = stringf("(%s != 0ub%d_0)", rvalue(cell->getPort("\\B")), width_b);
446 const char *expr_y = lvalue(cell->getPort("\\Y"));
447
448 string expr;
449 if (cell->type == "$logic_and") expr = expr_a + " & " + expr_b;
450 if (cell->type == "$logic_or") expr = expr_a + " | " + expr_b;
451
452 assignments.push_back(stringf("%s := resize(word1(%s), %d);", expr_y, expr.c_str(), width_y));
453 continue;
454 }
455
456 if (cell->type.in("$logic_not"))
457 {
458 int width_a = GetSize(cell->getPort("\\A"));
459 int width_y = GetSize(cell->getPort("\\Y"));
460
461 string expr_a = stringf("(%s = 0ub%d_0)", rvalue(cell->getPort("\\A")), width_a);
462 const char *expr_y = lvalue(cell->getPort("\\Y"));
463
464 assignments.push_back(stringf("%s := resize(word1(%s), %d);", expr_y, expr_a.c_str(), width_y));
465 continue;
466 }
467
468 if (cell->type.in("$mux", "$pmux"))
469 {
470 int width = GetSize(cell->getPort("\\Y"));
471 SigSpec sig_a = cell->getPort("\\A");
472 SigSpec sig_b = cell->getPort("\\B");
473 SigSpec sig_s = cell->getPort("\\S");
474
475 string expr;
476 for (int i = 0; i < GetSize(sig_s); i++)
477 expr += stringf("bool(%s) ? %s : ", rvalue(sig_s[i]), rvalue(sig_b.extract(i*width, width)));
478 expr += rvalue(sig_a);
479
480 assignments.push_back(stringf("%s := %s;", lvalue(cell->getPort("\\Y")), expr.c_str()));
481 continue;
482 }
483
484 if (cell->type == "$dff")
485 {
486 // FIXME: use init property
487 assignments.push_back(stringf("next(%s) := %s;", lvalue(cell->getPort("\\Q")), rvalue(cell->getPort("\\D"))));
488 continue;
489 }
490
491 if (cell->type.in("$_BUF_", "$_NOT_"))
492 {
493 string op = cell->type == "$_NOT_" ? "!" : "";
494 assignments.push_back(stringf("%s := %s%s;", lvalue(cell->getPort("\\Y")), op.c_str(), rvalue(cell->getPort("\\A"))));
495 continue;
496 }
497
498 if (cell->type.in("$_AND_", "$_NAND_", "$_OR_", "$_NOR_", "$_XOR_", "$_XNOR_"))
499 {
500 string op;
501
502 if (cell->type.in("$_AND_", "$_NAND_")) op = "&";
503 if (cell->type.in("$_OR_", "$_NOR_")) op = "|";
504 if (cell->type.in("$_XOR_")) op = "xor";
505 if (cell->type.in("$_XNOR_")) op = "xnor";
506
507 if (cell->type.in("$_NAND_", "$_NOR_"))
508 assignments.push_back(stringf("%s := !(%s %s %s);", lvalue(cell->getPort("\\Y")),
509 rvalue(cell->getPort("\\A")), op.c_str(), rvalue(cell->getPort("\\B"))));
510 else
511 assignments.push_back(stringf("%s := %s %s %s;", lvalue(cell->getPort("\\Y")),
512 rvalue(cell->getPort("\\A")), op.c_str(), rvalue(cell->getPort("\\B"))));
513 continue;
514 }
515
516 if (cell->type == "$_MUX_")
517 {
518 assignments.push_back(stringf("%s := bool(%s) ? %s : %s;", lvalue(cell->getPort("\\Y")),
519 rvalue(cell->getPort("\\S")), rvalue(cell->getPort("\\B")), rvalue(cell->getPort("\\A"))));
520 continue;
521 }
522
523 if (cell->type == "$_AOI3_")
524 {
525 assignments.push_back(stringf("%s := !((%s & %s) | %s);", lvalue(cell->getPort("\\Y")),
526 rvalue(cell->getPort("\\A")), rvalue(cell->getPort("\\B")), rvalue(cell->getPort("\\C"))));
527 continue;
528 }
529
530 if (cell->type == "$_OAI3_")
531 {
532 assignments.push_back(stringf("%s := !((%s | %s) & %s);", lvalue(cell->getPort("\\Y")),
533 rvalue(cell->getPort("\\A")), rvalue(cell->getPort("\\B")), rvalue(cell->getPort("\\C"))));
534 continue;
535 }
536
537 if (cell->type == "$_AOI4_")
538 {
539 assignments.push_back(stringf("%s := !((%s & %s) | (%s & %s));", lvalue(cell->getPort("\\Y")),
540 rvalue(cell->getPort("\\A")), rvalue(cell->getPort("\\B")), rvalue(cell->getPort("\\C")), rvalue(cell->getPort("\\D"))));
541 continue;
542 }
543
544 if (cell->type == "$_OAI4_")
545 {
546 assignments.push_back(stringf("%s := !((%s | %s) & (%s | %s));", lvalue(cell->getPort("\\Y")),
547 rvalue(cell->getPort("\\A")), rvalue(cell->getPort("\\B")), rvalue(cell->getPort("\\C")), rvalue(cell->getPort("\\D"))));
548 continue;
549 }
550
551 if (cell->type[0] == '$')
552 log_error("Found currently unsupported cell type %s (%s.%s).\n", log_id(cell->type), log_id(module), log_id(cell));
553
554 f << stringf(" %s : %s;\n", cid(cell->name), cid(cell->type));
555
556 for (auto &conn : cell->connections())
557 if (cell->output(conn.first))
558 assignments.push_back(stringf("%s := %s.%s;", lvalue(conn.second), cid(cell->name), cid(conn.first)));
559 else
560 assignments.push_back(stringf("%s.%s := %s;", cid(cell->name), cid(conn.first), rvalue(conn.second)));
561 }
562
563 for (Wire *wire : partial_assignment_wires)
564 {
565 string expr;
566
567 for (int i = 0; i < wire->width; i++)
568 {
569 SigBit bit = sigmap(SigBit(wire, i));
570
571 if (!expr.empty())
572 expr = " :: " + expr;
573
574 if (partial_assignment_bits.count(bit))
575 {
576 int width = 1;
577 const auto &bit_a = partial_assignment_bits.at(bit);
578
579 while (i+1 < wire->width)
580 {
581 SigBit next_bit = sigmap(SigBit(wire, i+1));
582
583 if (!partial_assignment_bits.count(next_bit))
584 break;
585
586 const auto &bit_b = partial_assignment_bits.at(next_bit);
587 if (strcmp(bit_a.first, bit_b.first))
588 break;
589 if (bit_a.second+width != bit_b.second)
590 break;
591
592 width++, i++;
593 }
594
595 expr = stringf("%s[%d:%d]", bit_a.first, bit_a.second+width-1, bit_a.second) + expr;
596 }
597 else if (sigmap(SigBit(wire, i)).wire == nullptr)
598 {
599 string bits;
600 SigSpec sig = sigmap(SigSpec(wire, i));
601
602 while (i+1 < wire->width) {
603 SigBit next_bit = sigmap(SigBit(wire, i+1));
604 if (next_bit.wire != nullptr)
605 break;
606 sig.append(next_bit);
607 i++;
608 }
609
610 for (int k = GetSize(sig)-1; k >= 0; k--)
611 bits += sig[k] == State::S1 ? '1' : '0';
612
613 expr = stringf("0ub%d_%s", GetSize(bits), bits.c_str()) + expr;
614 }
615 else
616 {
617 string bits;
618 SigSpec sig = sigmap(SigSpec(wire, i));
619
620 while (i+1 < wire->width) {
621 SigBit next_bit = sigmap(SigBit(wire, i+1));
622 if (next_bit.wire == nullptr || partial_assignment_bits.count(next_bit))
623 break;
624 sig.append(next_bit);
625 i++;
626 }
627
628 expr = rvalue(sig) + expr;
629 }
630 }
631
632 assignments.push_back(stringf("%s := %s;", cid(wire->name), expr.c_str()));
633 }
634
635 f << stringf(" ASSIGN\n");
636 for (const string &line : assignments)
637 f << stringf(" %s\n", line.c_str());
638 }
639 };
640
641 struct SmvBackend : public Backend {
642 SmvBackend() : Backend("smv", "write design to SMV file") { }
643 virtual void help()
644 {
645 // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
646 log("\n");
647 log(" write_smv [options] [filename]\n");
648 log("\n");
649 log("Write an SMV description of the current design.\n");
650 log("\n");
651 log(" -verbose\n");
652 log(" this will print the recursive walk used to export the modules.\n");
653 log("\n");
654 log(" -tpl <template_file>\n");
655 log(" use the given template file. the line containing only the token '%%%%'\n");
656 log(" is replaced with the regular output of this command.\n");
657 log("\n");
658 log("THIS COMMAND IS UNDER CONSTRUCTION\n");
659 log("\n");
660 }
661 virtual void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design)
662 {
663 std::ifstream template_f;
664 bool verbose = false;
665
666 log_header("Executing SMV backend.\n");
667
668 size_t argidx;
669 for (argidx = 1; argidx < args.size(); argidx++)
670 {
671 if (args[argidx] == "-tpl" && argidx+1 < args.size()) {
672 template_f.open(args[++argidx]);
673 if (template_f.fail())
674 log_error("Can't open template file `%s'.\n", args[argidx].c_str());
675 continue;
676 }
677 if (args[argidx] == "-verbose") {
678 verbose = true;
679 continue;
680 }
681 break;
682 }
683 extra_args(f, filename, args, argidx);
684
685 pool<Module*> modules;
686
687 for (auto module : design->modules())
688 if (!module->get_bool_attribute("\\blackbox") && !module->has_memories_warn() && !module->has_processes_warn())
689 modules.insert(module);
690
691 if (template_f.is_open())
692 {
693 std::string line;
694 while (std::getline(template_f, line))
695 {
696 int indent = 0;
697 while (indent < GetSize(line) && (line[indent] == ' ' || line[indent] == '\t'))
698 indent++;
699
700 if (line[indent] == '%')
701 {
702 vector<string> stmt = split_tokens(line);
703
704 if (GetSize(stmt) == 1 && stmt[0] == "%%")
705 break;
706
707 if (GetSize(stmt) == 2 && stmt[0] == "%module")
708 {
709 Module *module = design->module(RTLIL::escape_id(stmt[1]));
710 modules.erase(module);
711
712 if (module == nullptr)
713 log_error("Module '%s' not found.\n", stmt[1].c_str());
714
715 *f << stringf("-- SMV description generated by %s\n", yosys_version_str);
716
717 log("Creating SMV representation of module %s.\n", log_id(module));
718 SmvWorker worker(module, verbose, *f);
719 worker.run();
720
721 *f << stringf("-- end of yosys output\n");
722 continue;
723 }
724
725 log_error("Unknown template statement: '%s'", line.c_str() + indent);
726 }
727
728 *f << line << std::endl;
729 }
730 }
731
732 if (!modules.empty())
733 {
734 *f << stringf("-- SMV description generated by %s\n", yosys_version_str);
735
736 for (auto module : modules) {
737 log("Creating SMV representation of module %s.\n", log_id(module));
738 SmvWorker worker(module, verbose, *f);
739 worker.run();
740 }
741
742 *f << stringf("-- end of yosys output\n");
743 }
744
745 if (template_f.is_open()) {
746 std::string line;
747 while (std::getline(template_f, line))
748 *f << line << std::endl;
749 }
750 }
751 } SmvBackend;
752
753 PRIVATE_NAMESPACE_END