projects / yosys.git / blob
? search:
summary | shortlog | log | commit | commitdiff | tree
history | raw | HEAD
Fixed trailing whitespaces
[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 if (wire->attributes.count("\\init"))
223 assignments.push_back(stringf("init(%s) := %s;", lvalue(wire), rvalue(wire->attributes.at("\\init"))));
224 }
225
226 for (auto cell : module->cells())
227 {
228 // FIXME: $slice, $concat, $mem
229
230 if (cell->type.in("$shl", "$shr", "$sshl", "$sshr", "$shift", "$shiftx"))
231 {
232 SigSpec sig_a = cell->getPort("\\A");
233 SigSpec sig_b = cell->getPort("\\B");
234
235 int width_y = GetSize(cell->getPort("\\Y"));
236 int shift_b_width = GetSize(sig_b);
237 int width_ay = std::max(GetSize(sig_a), width_y);
238 int width = width_ay;
239
240 for (int i = 1, j = 0;; i <<= 1, j++)
241 if (width_ay < i) {
242 width = i-1;
243 shift_b_width = std::min(shift_b_width, j);
244 break;
245 }
246
247 bool signed_a = cell->getParam("\\A_SIGNED").as_bool();
248 bool signed_b = cell->getParam("\\B_SIGNED").as_bool();
249 string op = cell->type.in("$shl", "$sshl") ? "<<" : ">>";
250 string expr, expr_a;
251
252 if (cell->type == "$sshr" && signed_a)
253 {
254 expr_a = rvalue_s(sig_a, width);
255 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);
256 if (shift_b_width < GetSize(sig_b))
257 expr = stringf("%s != 0ud%d_0 ? (bool(%s) ? !0ud%d_0 : 0ud%d_0) : %s",
258 rvalue(sig_b.extract(shift_b_width, GetSize(sig_b) - shift_b_width)), GetSize(sig_b) - shift_b_width,
259 rvalue(sig_a[GetSize(sig_a)-1]), width_y, width_y, expr.c_str());
260 }
261 else if (cell->type.in("$shift", "$shiftx") && signed_b)
262 {
263 expr_a = rvalue_u(sig_a, width);
264
265 const char *b_shr = rvalue_u(sig_b);
266 const char *b_shl = cid();
267
268 f << stringf(" %s : unsigned word[%d]; -- neg(%s)\n", b_shl, GetSize(sig_b), log_signal(sig_b));
269 assignments.push_back(stringf("%s := unsigned(-%s);", b_shl, rvalue_s(sig_b)));
270
271 string expr_shl = stringf("resize(%s << %s[%d:0], %d)", expr_a.c_str(), b_shl, shift_b_width-1, width_y);
272 string expr_shr = stringf("resize(%s >> %s[%d:0], %d)", expr_a.c_str(), b_shr, shift_b_width-1, width_y);
273
274 if (shift_b_width < GetSize(sig_b)) {
275 expr_shl = stringf("%s[%d:%d] != 0ud%d_0 ? 0ud%d_0 : %s", b_shl, GetSize(sig_b)-1, shift_b_width,
276 GetSize(sig_b)-shift_b_width, width_y, expr_shl.c_str());
277 expr_shr = stringf("%s[%d:%d] != 0ud%d_0 ? 0ud%d_0 : %s", b_shr, GetSize(sig_b)-1, shift_b_width,
278 GetSize(sig_b)-shift_b_width, width_y, expr_shr.c_str());
279 }
280
281 expr = stringf("bool(%s) ? %s : %s", rvalue(sig_b[GetSize(sig_b)-1]), expr_shl.c_str(), expr_shr.c_str());
282 }
283 else
284 {
285 if (cell->type.in("$shift", "$shiftx") || !signed_a)
286 expr_a = rvalue_u(sig_a, width);
287 else
288 expr_a = stringf("resize(unsigned(%s), %d)", rvalue_s(sig_a, width_ay), width);
289
290 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);
291 if (shift_b_width < GetSize(sig_b))
292 expr = stringf("%s[%d:%d] != 0ud%d_0 ? 0ud%d_0 : %s", rvalue_u(sig_b), GetSize(sig_b)-1, shift_b_width,
293 GetSize(sig_b)-shift_b_width, width_y, expr.c_str());
294 }
295
296 assignments.push_back(stringf("%s := %s;", lvalue(cell->getPort("\\Y")), expr.c_str()));
297
298 continue;
299 }
300
301 if (cell->type.in("$not", "$pos", "$neg"))
302 {
303 int width = GetSize(cell->getPort("\\Y"));
304 string expr_a, op;
305
306 if (cell->type == "$not") op = "!";
307 if (cell->type == "$pos") op = "";
308 if (cell->type == "$neg") op = "-";
309
310 if (cell->getParam("\\A_SIGNED").as_bool())
311 {
312 assignments.push_back(stringf("%s := unsigned(%s%s);", lvalue(cell->getPort("\\Y")),
313 op.c_str(), rvalue_s(cell->getPort("\\A"), width)));
314 }
315 else
316 {
317 assignments.push_back(stringf("%s := %s%s;", lvalue(cell->getPort("\\Y")),
318 op.c_str(), rvalue_u(cell->getPort("\\A"), width)));
319 }
320
321 continue;
322 }
323
324 if (cell->type.in("$add", "$sub", "$mul", "$and", "$or", "$xor", "$xnor"))
325 {
326 int width = GetSize(cell->getPort("\\Y"));
327 string expr_a, expr_b, op;
328
329 if (cell->type == "$add") op = "+";
330 if (cell->type == "$sub") op = "-";
331 if (cell->type == "$mul") op = "*";
332 if (cell->type == "$and") op = "&";
333 if (cell->type == "$or") op = "|";
334 if (cell->type == "$xor") op = "xor";
335 if (cell->type == "$xnor") op = "xnor";
336
337 if (cell->getParam("\\A_SIGNED").as_bool())
338 {
339 assignments.push_back(stringf("%s := unsigned(%s %s %s);", lvalue(cell->getPort("\\Y")),
340 rvalue_s(cell->getPort("\\A"), width), op.c_str(), rvalue_s(cell->getPort("\\B"), width)));
341 }
342 else
343 {
344 assignments.push_back(stringf("%s := %s %s %s;", lvalue(cell->getPort("\\Y")),
345 rvalue_u(cell->getPort("\\A"), width), op.c_str(), rvalue_u(cell->getPort("\\B"), width)));
346 }
347
348 continue;
349 }
350
351 if (cell->type.in("$div", "$mod"))
352 {
353 int width_y = GetSize(cell->getPort("\\Y"));
354 int width = std::max(width_y, GetSize(cell->getPort("\\A")));
355 width = std::max(width, GetSize(cell->getPort("\\B")));
356 string expr_a, expr_b, op;
357
358 if (cell->type == "$div") op = "/";
359 if (cell->type == "$mod") op = "mod";
360
361 if (cell->getParam("\\A_SIGNED").as_bool())
362 {
363 assignments.push_back(stringf("%s := resize(unsigned(%s %s %s), %d);", lvalue(cell->getPort("\\Y")),
364 rvalue_s(cell->getPort("\\A"), width), op.c_str(), rvalue_s(cell->getPort("\\B"), width), width_y));
365 }
366 else
367 {
368 assignments.push_back(stringf("%s := resize(%s %s %s, %d);", lvalue(cell->getPort("\\Y")),
369 rvalue_u(cell->getPort("\\A"), width), op.c_str(), rvalue_u(cell->getPort("\\B"), width), width_y));
370 }
371
372 continue;
373 }
374
375 if (cell->type.in("$eq", "$ne", "$eqx", "$nex", "$lt", "$le", "$ge", "$gt"))
376 {
377 int width = std::max(GetSize(cell->getPort("\\A")), GetSize(cell->getPort("\\B")));
378 string expr_a, expr_b, op;
379
380 if (cell->type == "$eq") op = "=";
381 if (cell->type == "$ne") op = "!=";
382 if (cell->type == "$eqx") op = "=";
383 if (cell->type == "$nex") op = "!=";
384 if (cell->type == "$lt") op = "<";
385 if (cell->type == "$le") op = "<=";
386 if (cell->type == "$ge") op = ">=";
387 if (cell->type == "$gt") op = ">";
388
389 if (cell->getParam("\\A_SIGNED").as_bool())
390 {
391 expr_a = stringf("resize(signed(%s), %d)", rvalue(cell->getPort("\\A")), width);
392 expr_b = stringf("resize(signed(%s), %d)", rvalue(cell->getPort("\\B")), width);
393 }
394 else
395 {
396 expr_a = stringf("resize(%s, %d)", rvalue(cell->getPort("\\A")), width);
397 expr_b = stringf("resize(%s, %d)", rvalue(cell->getPort("\\B")), width);
398 }
399
400 assignments.push_back(stringf("%s := resize(word1(%s %s %s), %d);", lvalue(cell->getPort("\\Y")),
401 expr_a.c_str(), op.c_str(), expr_b.c_str(), GetSize(cell->getPort("\\Y"))));
402
403 continue;
404 }
405
406 if (cell->type.in("$reduce_and", "$reduce_or", "$reduce_bool"))
407 {
408 int width_a = GetSize(cell->getPort("\\A"));
409 int width_y = GetSize(cell->getPort("\\Y"));
410 const char *expr_a = rvalue(cell->getPort("\\A"));
411 const char *expr_y = lvalue(cell->getPort("\\Y"));
412 string expr;
413
414 if (cell->type == "$reduce_and") expr = stringf("%s = !0ub%d_0", expr_a, width_a);
415 if (cell->type == "$reduce_or") expr = stringf("%s != 0ub%d_0", expr_a, width_a);
416 if (cell->type == "$reduce_bool") expr = stringf("%s != 0ub%d_0", expr_a, width_a);
417
418 assignments.push_back(stringf("%s := resize(word1(%s), %d);", expr_y, expr.c_str(), width_y));
419 continue;
420 }
421
422 if (cell->type.in("$reduce_xor", "$reduce_xnor"))
423 {
424 int width_y = GetSize(cell->getPort("\\Y"));
425 const char *expr_y = lvalue(cell->getPort("\\Y"));
426 string expr;
427
428 for (auto bit : cell->getPort("\\A")) {
429 if (!expr.empty())
430 expr += " xor ";
431 expr += rvalue(bit);
432 }
433
434 if (cell->type == "$reduce_xnor")
435 expr = "!(" + expr + ")";
436
437 assignments.push_back(stringf("%s := resize(%s, %d);", expr_y, expr.c_str(), width_y));
438 continue;
439 }
440
441 if (cell->type.in("$logic_and", "$logic_or"))
442 {
443 int width_a = GetSize(cell->getPort("\\A"));
444 int width_b = GetSize(cell->getPort("\\B"));
445 int width_y = GetSize(cell->getPort("\\Y"));
446
447 string expr_a = stringf("(%s != 0ub%d_0)", rvalue(cell->getPort("\\A")), width_a);
448 string expr_b = stringf("(%s != 0ub%d_0)", rvalue(cell->getPort("\\B")), width_b);
449 const char *expr_y = lvalue(cell->getPort("\\Y"));
450
451 string expr;
452 if (cell->type == "$logic_and") expr = expr_a + " & " + expr_b;
453 if (cell->type == "$logic_or") expr = expr_a + " | " + expr_b;
454
455 assignments.push_back(stringf("%s := resize(word1(%s), %d);", expr_y, expr.c_str(), width_y));
456 continue;
457 }
458
459 if (cell->type.in("$logic_not"))
460 {
461 int width_a = GetSize(cell->getPort("\\A"));
462 int width_y = GetSize(cell->getPort("\\Y"));
463
464 string expr_a = stringf("(%s = 0ub%d_0)", rvalue(cell->getPort("\\A")), width_a);
465 const char *expr_y = lvalue(cell->getPort("\\Y"));
466
467 assignments.push_back(stringf("%s := resize(word1(%s), %d);", expr_y, expr_a.c_str(), width_y));
468 continue;
469 }
470
471 if (cell->type.in("$mux", "$pmux"))
472 {
473 int width = GetSize(cell->getPort("\\Y"));
474 SigSpec sig_a = cell->getPort("\\A");
475 SigSpec sig_b = cell->getPort("\\B");
476 SigSpec sig_s = cell->getPort("\\S");
477
478 string expr;
479 for (int i = 0; i < GetSize(sig_s); i++)
480 expr += stringf("bool(%s) ? %s : ", rvalue(sig_s[i]), rvalue(sig_b.extract(i*width, width)));
481 expr += rvalue(sig_a);
482
483 assignments.push_back(stringf("%s := %s;", lvalue(cell->getPort("\\Y")), expr.c_str()));
484 continue;
485 }
486
487 if (cell->type == "$dff")
488 {
489 assignments.push_back(stringf("next(%s) := %s;", lvalue(cell->getPort("\\Q")), rvalue(cell->getPort("\\D"))));
490 continue;
491 }
492
493 if (cell->type.in("$_BUF_", "$_NOT_"))
494 {
495 string op = cell->type == "$_NOT_" ? "!" : "";
496 assignments.push_back(stringf("%s := %s%s;", lvalue(cell->getPort("\\Y")), op.c_str(), rvalue(cell->getPort("\\A"))));
497 continue;
498 }
499
500 if (cell->type.in("$_AND_", "$_NAND_", "$_OR_", "$_NOR_", "$_XOR_", "$_XNOR_"))
501 {
502 string op;
503
504 if (cell->type.in("$_AND_", "$_NAND_")) op = "&";
505 if (cell->type.in("$_OR_", "$_NOR_")) op = "|";
506 if (cell->type.in("$_XOR_")) op = "xor";
507 if (cell->type.in("$_XNOR_")) op = "xnor";
508
509 if (cell->type.in("$_NAND_", "$_NOR_"))
510 assignments.push_back(stringf("%s := !(%s %s %s);", lvalue(cell->getPort("\\Y")),
511 rvalue(cell->getPort("\\A")), op.c_str(), rvalue(cell->getPort("\\B"))));
512 else
513 assignments.push_back(stringf("%s := %s %s %s;", lvalue(cell->getPort("\\Y")),
514 rvalue(cell->getPort("\\A")), op.c_str(), rvalue(cell->getPort("\\B"))));
515 continue;
516 }
517
518 if (cell->type == "$_MUX_")
519 {
520 assignments.push_back(stringf("%s := bool(%s) ? %s : %s;", lvalue(cell->getPort("\\Y")),
521 rvalue(cell->getPort("\\S")), rvalue(cell->getPort("\\B")), rvalue(cell->getPort("\\A"))));
522 continue;
523 }
524
525 if (cell->type == "$_AOI3_")
526 {
527 assignments.push_back(stringf("%s := !((%s & %s) | %s);", lvalue(cell->getPort("\\Y")),
528 rvalue(cell->getPort("\\A")), rvalue(cell->getPort("\\B")), rvalue(cell->getPort("\\C"))));
529 continue;
530 }
531
532 if (cell->type == "$_OAI3_")
533 {
534 assignments.push_back(stringf("%s := !((%s | %s) & %s);", lvalue(cell->getPort("\\Y")),
535 rvalue(cell->getPort("\\A")), rvalue(cell->getPort("\\B")), rvalue(cell->getPort("\\C"))));
536 continue;
537 }
538
539 if (cell->type == "$_AOI4_")
540 {
541 assignments.push_back(stringf("%s := !((%s & %s) | (%s & %s));", lvalue(cell->getPort("\\Y")),
542 rvalue(cell->getPort("\\A")), rvalue(cell->getPort("\\B")), rvalue(cell->getPort("\\C")), rvalue(cell->getPort("\\D"))));
543 continue;
544 }
545
546 if (cell->type == "$_OAI4_")
547 {
548 assignments.push_back(stringf("%s := !((%s | %s) & (%s | %s));", lvalue(cell->getPort("\\Y")),
549 rvalue(cell->getPort("\\A")), rvalue(cell->getPort("\\B")), rvalue(cell->getPort("\\C")), rvalue(cell->getPort("\\D"))));
550 continue;
551 }
552
553 if (cell->type[0] == '$')
554 log_error("Found currently unsupported cell type %s (%s.%s).\n", log_id(cell->type), log_id(module), log_id(cell));
555
556 f << stringf(" %s : %s;\n", cid(cell->name), cid(cell->type));
557
558 for (auto &conn : cell->connections())
559 if (cell->output(conn.first))
560 assignments.push_back(stringf("%s := %s.%s;", lvalue(conn.second), cid(cell->name), cid(conn.first)));
561 else
562 assignments.push_back(stringf("%s.%s := %s;", cid(cell->name), cid(conn.first), rvalue(conn.second)));
563 }
564
565 for (Wire *wire : partial_assignment_wires)
566 {
567 string expr;
568
569 for (int i = 0; i < wire->width; i++)
570 {
571 SigBit bit = sigmap(SigBit(wire, i));
572
573 if (!expr.empty())
574 expr = " :: " + expr;
575
576 if (partial_assignment_bits.count(bit))
577 {
578 int width = 1;
579 const auto &bit_a = partial_assignment_bits.at(bit);
580
581 while (i+1 < wire->width)
582 {
583 SigBit next_bit = sigmap(SigBit(wire, i+1));
584
585 if (!partial_assignment_bits.count(next_bit))
586 break;
587
588 const auto &bit_b = partial_assignment_bits.at(next_bit);
589 if (strcmp(bit_a.first, bit_b.first))
590 break;
591 if (bit_a.second+width != bit_b.second)
592 break;
593
594 width++, i++;
595 }
596
597 expr = stringf("%s[%d:%d]", bit_a.first, bit_a.second+width-1, bit_a.second) + expr;
598 }
599 else if (sigmap(SigBit(wire, i)).wire == nullptr)
600 {
601 string bits;
602 SigSpec sig = sigmap(SigSpec(wire, i));
603
604 while (i+1 < wire->width) {
605 SigBit next_bit = sigmap(SigBit(wire, i+1));
606 if (next_bit.wire != nullptr)
607 break;
608 sig.append(next_bit);
609 i++;
610 }
611
612 for (int k = GetSize(sig)-1; k >= 0; k--)
613 bits += sig[k] == State::S1 ? '1' : '0';
614
615 expr = stringf("0ub%d_%s", GetSize(bits), bits.c_str()) + expr;
616 }
617 else
618 {
619 string bits;
620 SigSpec sig = sigmap(SigSpec(wire, i));
621
622 while (i+1 < wire->width) {
623 SigBit next_bit = sigmap(SigBit(wire, i+1));
624 if (next_bit.wire == nullptr || partial_assignment_bits.count(next_bit))
625 break;
626 sig.append(next_bit);
627 i++;
628 }
629
630 expr = rvalue(sig) + expr;
631 }
632 }
633
634 assignments.push_back(stringf("%s := %s;", cid(wire->name), expr.c_str()));
635 }
636
637 f << stringf(" ASSIGN\n");
638 for (const string &line : assignments)
639 f << stringf(" %s\n", line.c_str());
640 }
641 };
642
643 struct SmvBackend : public Backend {
644 SmvBackend() : Backend("smv", "write design to SMV file") { }
645 virtual void help()
646 {
647 // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
648 log("\n");
649 log(" write_smv [options] [filename]\n");
650 log("\n");
651 log("Write an SMV description of the current design.\n");
652 log("\n");
653 log(" -verbose\n");
654 log(" this will print the recursive walk used to export the modules.\n");
655 log("\n");
656 log(" -tpl <template_file>\n");
657 log(" use the given template file. the line containing only the token '%%%%'\n");
658 log(" is replaced with the regular output of this command.\n");
659 log("\n");
660 log("THIS COMMAND IS UNDER CONSTRUCTION\n");
661 log("\n");
662 }
663 virtual void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design)
664 {
665 std::ifstream template_f;
666 bool verbose = false;
667
668 log_header("Executing SMV backend.\n");
669
670 size_t argidx;
671 for (argidx = 1; argidx < args.size(); argidx++)
672 {
673 if (args[argidx] == "-tpl" && argidx+1 < args.size()) {
674 template_f.open(args[++argidx]);
675 if (template_f.fail())
676 log_error("Can't open template file `%s'.\n", args[argidx].c_str());
677 continue;
678 }
679 if (args[argidx] == "-verbose") {
680 verbose = true;
681 continue;
682 }
683 break;
684 }
685 extra_args(f, filename, args, argidx);
686
687 pool<Module*> modules;
688
689 for (auto module : design->modules())
690 if (!module->get_bool_attribute("\\blackbox") && !module->has_memories_warn() && !module->has_processes_warn())
691 modules.insert(module);
692
693 if (template_f.is_open())
694 {
695 std::string line;
696 while (std::getline(template_f, line))
697 {
698 int indent = 0;
699 while (indent < GetSize(line) && (line[indent] == ' ' || line[indent] == '\t'))
700 indent++;
701
702 if (line[indent] == '%')
703 {
704 vector<string> stmt = split_tokens(line);
705
706 if (GetSize(stmt) == 1 && stmt[0] == "%%")
707 break;
708
709 if (GetSize(stmt) == 2 && stmt[0] == "%module")
710 {
711 Module *module = design->module(RTLIL::escape_id(stmt[1]));
712 modules.erase(module);
713
714 if (module == nullptr)
715 log_error("Module '%s' not found.\n", stmt[1].c_str());
716
717 *f << stringf("-- SMV description generated by %s\n", yosys_version_str);
718
719 log("Creating SMV representation of module %s.\n", log_id(module));
720 SmvWorker worker(module, verbose, *f);
721 worker.run();
722
723 *f << stringf("-- end of yosys output\n");
724 continue;
725 }
726
727 log_error("Unknown template statement: '%s'", line.c_str() + indent);
728 }
729
730 *f << line << std::endl;
731 }
732 }
733
734 if (!modules.empty())
735 {
736 *f << stringf("-- SMV description generated by %s\n", yosys_version_str);
737
738 for (auto module : modules) {
739 log("Creating SMV representation of module %s.\n", log_id(module));
740 SmvWorker worker(module, verbose, *f);
741 worker.run();
742 }
743
744 *f << stringf("-- end of yosys output\n");
745 }
746
747 if (template_f.is_open()) {
748 std::string line;
749 while (std::getline(template_f, line))
750 *f << line << std::endl;
751 }
752 }
753 } SmvBackend;
754
755 PRIVATE_NAMESPACE_END