2 * yosys -- Yosys Open SYnthesis Suite
4 * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
6 * Permission to use, copy, modify, and/or distribute this software for any
7 * purpose with or without fee is hereby granted, provided that the above
8 * copyright notice and this permission notice appear in all copies.
10 * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
11 * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
12 * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
13 * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
14 * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
15 * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
16 * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
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"
28 PRIVATE_NAMESPACE_BEGIN
34 RTLIL::Module
*module
;
39 dict
<IdString
, shared_str
> idcache
;
40 pool
<shared_str
> used_names
;
41 vector
<shared_str
> strbuf
;
43 pool
<Wire
*> partial_assignment_wires
;
44 dict
<SigBit
, std::pair
<const char*, int>> partial_assignment_bits
;
45 vector
<string
> assignments
, invarspecs
;
50 shared_str
s(stringf("_%d", idcounter
++));
51 if (!used_names
.count(s
)) {
58 const char *cid(IdString id
, bool precache
= false)
60 if (!idcache
.count(id
))
62 string name
= stringf("_%s", id
.c_str());
64 if (name
.substr(0, 2) == "_\\")
65 name
= "_" + name
.substr(2);
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;
79 while (used_names
.count(name
))
87 return idcache
.at(id
).c_str();
90 SmvWorker(RTLIL::Module
*module
, bool verbose
, std::ostream
&f
) :
91 ct(module
->design
), sigmap(module
), module(module
), f(f
), verbose(verbose
), idcounter(0)
93 for (auto mod
: module
->design
->modules())
96 for (auto wire
: module
->wires())
97 cid(wire
->name
, true);
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);
107 const char *rvalue(SigSpec sig
, int width
= -1, bool is_signed
= false)
110 int count_chunks
= 0;
113 for (int i
= 0; i
< GetSize(sig
); i
++)
114 if (partial_assignment_bits
.count(sig
[i
]))
117 const auto &bit_a
= partial_assignment_bits
.at(sig
[i
]);
119 while (i
+width
< GetSize(sig
))
121 if (!partial_assignment_bits
.count(sig
[i
+width
]))
124 const auto &bit_b
= partial_assignment_bits
.at(sig
[i
+width
]);
125 if (strcmp(bit_a
.first
, bit_b
.first
))
127 if (bit_a
.second
+width
!= bit_b
.second
)
133 if (i
+width
< GetSize(sig
))
134 s
= stringf("%s :: ", rvalue(sig
.extract(i
+width
, GetSize(sig
)-(width
+i
))));
136 s
+= stringf("%s[%d:%d]", bit_a
.first
, bit_a
.second
+width
-1, bit_a
.second
);
139 s
+= stringf(" :: %s", rvalue(sig
.extract(0, i
)));
142 goto continue_with_resize
;
145 for (auto &c
: sig
.chunks()) {
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
;
153 s
= cid(c
.wire
->name
) + s
;
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';
162 continue_with_resize
:;
165 if (GetSize(sig
) > width
)
166 s
= stringf("signed(resize(%s, %d))", s
.c_str(), width
);
168 s
= stringf("resize(signed(%s), %d)", s
.c_str(), width
);
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());
177 return strbuf
.back().c_str();
180 const char *rvalue_u(SigSpec sig
, int width
= -1)
182 return rvalue(sig
, width
, false);
185 const char *rvalue_s(SigSpec sig
, int width
= -1, bool is_signed
= true)
187 return rvalue(sig
, width
, is_signed
);
190 const char *lvalue(SigSpec sig
)
197 const char *temp_id
= cid();
198 f
<< stringf(" %s : unsigned word[%d]; -- %s\n", temp_id
, GetSize(sig
), log_signal(sig
));
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
++);
212 f
<< stringf("MODULE %s\n", cid(module
->name
));
213 f
<< stringf(" VAR\n");
215 for (auto wire
: module
->wires())
217 if (SigSpec(wire
) != sigmap(wire
))
218 partial_assignment_wires
.insert(wire
);
220 f
<< stringf(" %s : unsigned word[%d]; -- %s\n", cid(wire
->name
), wire
->width
, log_id(wire
));
222 if (wire
->attributes
.count("\\init"))
223 assignments
.push_back(stringf("init(%s) := %s;", lvalue(wire
), rvalue(wire
->attributes
.at("\\init"))));
226 for (auto cell
: module
->cells())
228 // FIXME: $slice, $concat, $mem
230 if (cell
->type
.in("$assert"))
232 SigSpec sig_a
= cell
->getPort("\\A");
233 SigSpec sig_en
= cell
->getPort("\\EN");
235 invarspecs
.push_back(stringf("!bool(%s) | bool(%s);", rvalue(sig_en
), rvalue(sig_a
)));
240 if (cell
->type
.in("$shl", "$shr", "$sshl", "$sshr", "$shift", "$shiftx"))
242 SigSpec sig_a
= cell
->getPort("\\A");
243 SigSpec sig_b
= cell
->getPort("\\B");
245 int width_y
= GetSize(cell
->getPort("\\Y"));
246 int shift_b_width
= GetSize(sig_b
);
247 int width_ay
= max(GetSize(sig_a
), width_y
);
248 int width
= width_ay
;
250 for (int i
= 1, j
= 0;; i
<<= 1, j
++)
253 shift_b_width
= min(shift_b_width
, j
);
257 bool signed_a
= cell
->getParam("\\A_SIGNED").as_bool();
258 bool signed_b
= cell
->getParam("\\B_SIGNED").as_bool();
259 string op
= cell
->type
.in("$shl", "$sshl") ? "<<" : ">>";
262 if (cell
->type
== "$sshr" && signed_a
)
264 expr_a
= rvalue_s(sig_a
, width
);
265 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
);
266 if (shift_b_width
< GetSize(sig_b
))
267 expr
= stringf("%s != 0ud%d_0 ? (bool(%s) ? !0ud%d_0 : 0ud%d_0) : %s",
268 rvalue(sig_b
.extract(shift_b_width
, GetSize(sig_b
) - shift_b_width
)), GetSize(sig_b
) - shift_b_width
,
269 rvalue(sig_a
[GetSize(sig_a
)-1]), width_y
, width_y
, expr
.c_str());
271 else if (cell
->type
.in("$shift", "$shiftx") && signed_b
)
273 expr_a
= rvalue_u(sig_a
, width
);
275 const char *b_shr
= rvalue_u(sig_b
);
276 const char *b_shl
= cid();
278 f
<< stringf(" %s : unsigned word[%d]; -- neg(%s)\n", b_shl
, GetSize(sig_b
), log_signal(sig_b
));
279 assignments
.push_back(stringf("%s := unsigned(-%s);", b_shl
, rvalue_s(sig_b
)));
281 string expr_shl
= stringf("resize(%s << %s[%d:0], %d)", expr_a
.c_str(), b_shl
, shift_b_width
-1, width_y
);
282 string expr_shr
= stringf("resize(%s >> %s[%d:0], %d)", expr_a
.c_str(), b_shr
, shift_b_width
-1, width_y
);
284 if (shift_b_width
< GetSize(sig_b
)) {
285 expr_shl
= stringf("%s[%d:%d] != 0ud%d_0 ? 0ud%d_0 : %s", b_shl
, GetSize(sig_b
)-1, shift_b_width
,
286 GetSize(sig_b
)-shift_b_width
, width_y
, expr_shl
.c_str());
287 expr_shr
= stringf("%s[%d:%d] != 0ud%d_0 ? 0ud%d_0 : %s", b_shr
, GetSize(sig_b
)-1, shift_b_width
,
288 GetSize(sig_b
)-shift_b_width
, width_y
, expr_shr
.c_str());
291 expr
= stringf("bool(%s) ? %s : %s", rvalue(sig_b
[GetSize(sig_b
)-1]), expr_shl
.c_str(), expr_shr
.c_str());
295 if (cell
->type
.in("$shift", "$shiftx") || !signed_a
)
296 expr_a
= rvalue_u(sig_a
, width
);
298 expr_a
= stringf("resize(unsigned(%s), %d)", rvalue_s(sig_a
, width_ay
), width
);
300 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
);
301 if (shift_b_width
< GetSize(sig_b
))
302 expr
= stringf("%s[%d:%d] != 0ud%d_0 ? 0ud%d_0 : %s", rvalue_u(sig_b
), GetSize(sig_b
)-1, shift_b_width
,
303 GetSize(sig_b
)-shift_b_width
, width_y
, expr
.c_str());
306 assignments
.push_back(stringf("%s := %s;", lvalue(cell
->getPort("\\Y")), expr
.c_str()));
311 if (cell
->type
.in("$not", "$pos", "$neg"))
313 int width
= GetSize(cell
->getPort("\\Y"));
316 if (cell
->type
== "$not") op
= "!";
317 if (cell
->type
== "$pos") op
= "";
318 if (cell
->type
== "$neg") op
= "-";
320 if (cell
->getParam("\\A_SIGNED").as_bool())
322 assignments
.push_back(stringf("%s := unsigned(%s%s);", lvalue(cell
->getPort("\\Y")),
323 op
.c_str(), rvalue_s(cell
->getPort("\\A"), width
)));
327 assignments
.push_back(stringf("%s := %s%s;", lvalue(cell
->getPort("\\Y")),
328 op
.c_str(), rvalue_u(cell
->getPort("\\A"), width
)));
334 if (cell
->type
.in("$add", "$sub", "$mul", "$and", "$or", "$xor", "$xnor"))
336 int width
= GetSize(cell
->getPort("\\Y"));
337 string expr_a
, expr_b
, op
;
339 if (cell
->type
== "$add") op
= "+";
340 if (cell
->type
== "$sub") op
= "-";
341 if (cell
->type
== "$mul") op
= "*";
342 if (cell
->type
== "$and") op
= "&";
343 if (cell
->type
== "$or") op
= "|";
344 if (cell
->type
== "$xor") op
= "xor";
345 if (cell
->type
== "$xnor") op
= "xnor";
347 if (cell
->getParam("\\A_SIGNED").as_bool())
349 assignments
.push_back(stringf("%s := unsigned(%s %s %s);", lvalue(cell
->getPort("\\Y")),
350 rvalue_s(cell
->getPort("\\A"), width
), op
.c_str(), rvalue_s(cell
->getPort("\\B"), width
)));
354 assignments
.push_back(stringf("%s := %s %s %s;", lvalue(cell
->getPort("\\Y")),
355 rvalue_u(cell
->getPort("\\A"), width
), op
.c_str(), rvalue_u(cell
->getPort("\\B"), width
)));
361 if (cell
->type
.in("$div", "$mod"))
363 int width_y
= GetSize(cell
->getPort("\\Y"));
364 int width
= max(width_y
, GetSize(cell
->getPort("\\A")));
365 width
= max(width
, GetSize(cell
->getPort("\\B")));
366 string expr_a
, expr_b
, op
;
368 if (cell
->type
== "$div") op
= "/";
369 if (cell
->type
== "$mod") op
= "mod";
371 if (cell
->getParam("\\A_SIGNED").as_bool())
373 assignments
.push_back(stringf("%s := resize(unsigned(%s %s %s), %d);", lvalue(cell
->getPort("\\Y")),
374 rvalue_s(cell
->getPort("\\A"), width
), op
.c_str(), rvalue_s(cell
->getPort("\\B"), width
), width_y
));
378 assignments
.push_back(stringf("%s := resize(%s %s %s, %d);", lvalue(cell
->getPort("\\Y")),
379 rvalue_u(cell
->getPort("\\A"), width
), op
.c_str(), rvalue_u(cell
->getPort("\\B"), width
), width_y
));
385 if (cell
->type
.in("$eq", "$ne", "$eqx", "$nex", "$lt", "$le", "$ge", "$gt"))
387 int width
= max(GetSize(cell
->getPort("\\A")), GetSize(cell
->getPort("\\B")));
388 string expr_a
, expr_b
, op
;
390 if (cell
->type
== "$eq") op
= "=";
391 if (cell
->type
== "$ne") op
= "!=";
392 if (cell
->type
== "$eqx") op
= "=";
393 if (cell
->type
== "$nex") op
= "!=";
394 if (cell
->type
== "$lt") op
= "<";
395 if (cell
->type
== "$le") op
= "<=";
396 if (cell
->type
== "$ge") op
= ">=";
397 if (cell
->type
== "$gt") op
= ">";
399 if (cell
->getParam("\\A_SIGNED").as_bool())
401 expr_a
= stringf("resize(signed(%s), %d)", rvalue(cell
->getPort("\\A")), width
);
402 expr_b
= stringf("resize(signed(%s), %d)", rvalue(cell
->getPort("\\B")), width
);
406 expr_a
= stringf("resize(%s, %d)", rvalue(cell
->getPort("\\A")), width
);
407 expr_b
= stringf("resize(%s, %d)", rvalue(cell
->getPort("\\B")), width
);
410 assignments
.push_back(stringf("%s := resize(word1(%s %s %s), %d);", lvalue(cell
->getPort("\\Y")),
411 expr_a
.c_str(), op
.c_str(), expr_b
.c_str(), GetSize(cell
->getPort("\\Y"))));
416 if (cell
->type
.in("$reduce_and", "$reduce_or", "$reduce_bool"))
418 int width_a
= GetSize(cell
->getPort("\\A"));
419 int width_y
= GetSize(cell
->getPort("\\Y"));
420 const char *expr_a
= rvalue(cell
->getPort("\\A"));
421 const char *expr_y
= lvalue(cell
->getPort("\\Y"));
424 if (cell
->type
== "$reduce_and") expr
= stringf("%s = !0ub%d_0", expr_a
, width_a
);
425 if (cell
->type
== "$reduce_or") expr
= stringf("%s != 0ub%d_0", expr_a
, width_a
);
426 if (cell
->type
== "$reduce_bool") expr
= stringf("%s != 0ub%d_0", expr_a
, width_a
);
428 assignments
.push_back(stringf("%s := resize(word1(%s), %d);", expr_y
, expr
.c_str(), width_y
));
432 if (cell
->type
.in("$reduce_xor", "$reduce_xnor"))
434 int width_y
= GetSize(cell
->getPort("\\Y"));
435 const char *expr_y
= lvalue(cell
->getPort("\\Y"));
438 for (auto bit
: cell
->getPort("\\A")) {
444 if (cell
->type
== "$reduce_xnor")
445 expr
= "!(" + expr
+ ")";
447 assignments
.push_back(stringf("%s := resize(%s, %d);", expr_y
, expr
.c_str(), width_y
));
451 if (cell
->type
.in("$logic_and", "$logic_or"))
453 int width_a
= GetSize(cell
->getPort("\\A"));
454 int width_b
= GetSize(cell
->getPort("\\B"));
455 int width_y
= GetSize(cell
->getPort("\\Y"));
457 string expr_a
= stringf("(%s != 0ub%d_0)", rvalue(cell
->getPort("\\A")), width_a
);
458 string expr_b
= stringf("(%s != 0ub%d_0)", rvalue(cell
->getPort("\\B")), width_b
);
459 const char *expr_y
= lvalue(cell
->getPort("\\Y"));
462 if (cell
->type
== "$logic_and") expr
= expr_a
+ " & " + expr_b
;
463 if (cell
->type
== "$logic_or") expr
= expr_a
+ " | " + expr_b
;
465 assignments
.push_back(stringf("%s := resize(word1(%s), %d);", expr_y
, expr
.c_str(), width_y
));
469 if (cell
->type
.in("$logic_not"))
471 int width_a
= GetSize(cell
->getPort("\\A"));
472 int width_y
= GetSize(cell
->getPort("\\Y"));
474 string expr_a
= stringf("(%s = 0ub%d_0)", rvalue(cell
->getPort("\\A")), width_a
);
475 const char *expr_y
= lvalue(cell
->getPort("\\Y"));
477 assignments
.push_back(stringf("%s := resize(word1(%s), %d);", expr_y
, expr_a
.c_str(), width_y
));
481 if (cell
->type
.in("$mux", "$pmux"))
483 int width
= GetSize(cell
->getPort("\\Y"));
484 SigSpec sig_a
= cell
->getPort("\\A");
485 SigSpec sig_b
= cell
->getPort("\\B");
486 SigSpec sig_s
= cell
->getPort("\\S");
489 for (int i
= 0; i
< GetSize(sig_s
); i
++)
490 expr
+= stringf("bool(%s) ? %s : ", rvalue(sig_s
[i
]), rvalue(sig_b
.extract(i
*width
, width
)));
491 expr
+= rvalue(sig_a
);
493 assignments
.push_back(stringf("%s := %s;", lvalue(cell
->getPort("\\Y")), expr
.c_str()));
497 if (cell
->type
== "$dff")
499 assignments
.push_back(stringf("next(%s) := %s;", lvalue(cell
->getPort("\\Q")), rvalue(cell
->getPort("\\D"))));
503 if (cell
->type
.in("$_BUF_", "$_NOT_"))
505 string op
= cell
->type
== "$_NOT_" ? "!" : "";
506 assignments
.push_back(stringf("%s := %s%s;", lvalue(cell
->getPort("\\Y")), op
.c_str(), rvalue(cell
->getPort("\\A"))));
510 if (cell
->type
.in("$_AND_", "$_NAND_", "$_OR_", "$_NOR_", "$_XOR_", "$_XNOR_"))
514 if (cell
->type
.in("$_AND_", "$_NAND_")) op
= "&";
515 if (cell
->type
.in("$_OR_", "$_NOR_")) op
= "|";
516 if (cell
->type
.in("$_XOR_")) op
= "xor";
517 if (cell
->type
.in("$_XNOR_")) op
= "xnor";
519 if (cell
->type
.in("$_NAND_", "$_NOR_"))
520 assignments
.push_back(stringf("%s := !(%s %s %s);", lvalue(cell
->getPort("\\Y")),
521 rvalue(cell
->getPort("\\A")), op
.c_str(), rvalue(cell
->getPort("\\B"))));
523 assignments
.push_back(stringf("%s := %s %s %s;", lvalue(cell
->getPort("\\Y")),
524 rvalue(cell
->getPort("\\A")), op
.c_str(), rvalue(cell
->getPort("\\B"))));
528 if (cell
->type
== "$_MUX_")
530 assignments
.push_back(stringf("%s := bool(%s) ? %s : %s;", lvalue(cell
->getPort("\\Y")),
531 rvalue(cell
->getPort("\\S")), rvalue(cell
->getPort("\\B")), rvalue(cell
->getPort("\\A"))));
535 if (cell
->type
== "$_AOI3_")
537 assignments
.push_back(stringf("%s := !((%s & %s) | %s);", lvalue(cell
->getPort("\\Y")),
538 rvalue(cell
->getPort("\\A")), rvalue(cell
->getPort("\\B")), rvalue(cell
->getPort("\\C"))));
542 if (cell
->type
== "$_OAI3_")
544 assignments
.push_back(stringf("%s := !((%s | %s) & %s);", lvalue(cell
->getPort("\\Y")),
545 rvalue(cell
->getPort("\\A")), rvalue(cell
->getPort("\\B")), rvalue(cell
->getPort("\\C"))));
549 if (cell
->type
== "$_AOI4_")
551 assignments
.push_back(stringf("%s := !((%s & %s) | (%s & %s));", lvalue(cell
->getPort("\\Y")),
552 rvalue(cell
->getPort("\\A")), rvalue(cell
->getPort("\\B")), rvalue(cell
->getPort("\\C")), rvalue(cell
->getPort("\\D"))));
556 if (cell
->type
== "$_OAI4_")
558 assignments
.push_back(stringf("%s := !((%s | %s) & (%s | %s));", lvalue(cell
->getPort("\\Y")),
559 rvalue(cell
->getPort("\\A")), rvalue(cell
->getPort("\\B")), rvalue(cell
->getPort("\\C")), rvalue(cell
->getPort("\\D"))));
563 if (cell
->type
[0] == '$')
564 log_error("Found currently unsupported cell type %s (%s.%s).\n", log_id(cell
->type
), log_id(module
), log_id(cell
));
566 f
<< stringf(" %s : %s;\n", cid(cell
->name
), cid(cell
->type
));
568 for (auto &conn
: cell
->connections())
569 if (cell
->output(conn
.first
))
570 assignments
.push_back(stringf("%s := %s.%s;", lvalue(conn
.second
), cid(cell
->name
), cid(conn
.first
)));
572 assignments
.push_back(stringf("%s.%s := %s;", cid(cell
->name
), cid(conn
.first
), rvalue(conn
.second
)));
575 for (Wire
*wire
: partial_assignment_wires
)
579 for (int i
= 0; i
< wire
->width
; i
++)
582 expr
= " :: " + expr
;
584 if (partial_assignment_bits
.count(sigmap(SigBit(wire
, i
))))
587 const auto &bit_a
= partial_assignment_bits
.at(sigmap(SigBit(wire
, i
)));
589 while (i
+1 < wire
->width
)
591 SigBit next_bit
= sigmap(SigBit(wire
, i
+1));
593 if (!partial_assignment_bits
.count(next_bit
))
596 const auto &bit_b
= partial_assignment_bits
.at(next_bit
);
597 if (strcmp(bit_a
.first
, bit_b
.first
))
599 if (bit_a
.second
+width
!= bit_b
.second
)
605 expr
= stringf("%s[%d:%d]", bit_a
.first
, bit_a
.second
+width
-1, bit_a
.second
) + expr
;
607 else if (sigmap(SigBit(wire
, i
)).wire
== nullptr)
610 SigSpec sig
= sigmap(SigSpec(wire
, i
));
612 while (i
+1 < wire
->width
) {
613 SigBit next_bit
= sigmap(SigBit(wire
, i
+1));
614 if (next_bit
.wire
!= nullptr)
616 sig
.append(next_bit
);
620 for (int k
= GetSize(sig
)-1; k
>= 0; k
--)
621 bits
+= sig
[k
] == State::S1
? '1' : '0';
623 expr
= stringf("0ub%d_%s", GetSize(bits
), bits
.c_str()) + expr
;
625 else if (sigmap(SigBit(wire
, i
)) == SigBit(wire
, i
))
629 while (i
+1 < wire
->width
) {
630 if (partial_assignment_bits
.count(sigmap(SigBit(wire
, i
+1))))
632 if (sigmap(SigBit(wire
, i
+1)) != SigBit(wire
, i
+1))
637 expr
= stringf("0ub%d_0", length
) + expr
;
642 SigSpec sig
= sigmap(SigSpec(wire
, i
));
644 while (i
+1 < wire
->width
) {
645 SigBit next_bit
= sigmap(SigBit(wire
, i
+1));
646 if (next_bit
.wire
== nullptr || partial_assignment_bits
.count(next_bit
))
648 sig
.append(next_bit
);
652 expr
= rvalue(sig
) + expr
;
656 assignments
.push_back(stringf("%s := %s;", cid(wire
->name
), expr
.c_str()));
659 if (!assignments
.empty()) {
660 f
<< stringf(" ASSIGN\n");
661 for (const string
&line
: assignments
)
662 f
<< stringf(" %s\n", line
.c_str());
665 if (!invarspecs
.empty()) {
666 for (const string
&line
: invarspecs
)
667 f
<< stringf(" INVARSPEC %s\n", line
.c_str());
672 struct SmvBackend
: public Backend
{
673 SmvBackend() : Backend("smv", "write design to SMV file") { }
676 // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
678 log(" write_smv [options] [filename]\n");
680 log("Write an SMV description of the current design.\n");
683 log(" this will print the recursive walk used to export the modules.\n");
685 log(" -tpl <template_file>\n");
686 log(" use the given template file. the line containing only the token '%%%%'\n");
687 log(" is replaced with the regular output of this command.\n");
689 log("THIS COMMAND IS UNDER CONSTRUCTION\n");
692 virtual void execute(std::ostream
*&f
, std::string filename
, std::vector
<std::string
> args
, RTLIL::Design
*design
)
694 std::ifstream template_f
;
695 bool verbose
= false;
697 log_header("Executing SMV backend.\n");
700 for (argidx
= 1; argidx
< args
.size(); argidx
++)
702 if (args
[argidx
] == "-tpl" && argidx
+1 < args
.size()) {
703 template_f
.open(args
[++argidx
]);
704 if (template_f
.fail())
705 log_error("Can't open template file `%s'.\n", args
[argidx
].c_str());
708 if (args
[argidx
] == "-verbose") {
714 extra_args(f
, filename
, args
, argidx
);
716 pool
<Module
*> modules
;
718 for (auto module
: design
->modules())
719 if (!module
->get_bool_attribute("\\blackbox") && !module
->has_memories_warn() && !module
->has_processes_warn())
720 modules
.insert(module
);
722 if (template_f
.is_open())
725 while (std::getline(template_f
, line
))
728 while (indent
< GetSize(line
) && (line
[indent
] == ' ' || line
[indent
] == '\t'))
731 if (line
[indent
] == '%')
733 vector
<string
> stmt
= split_tokens(line
);
735 if (GetSize(stmt
) == 1 && stmt
[0] == "%%")
738 if (GetSize(stmt
) == 2 && stmt
[0] == "%module")
740 Module
*module
= design
->module(RTLIL::escape_id(stmt
[1]));
741 modules
.erase(module
);
743 if (module
== nullptr)
744 log_error("Module '%s' not found.\n", stmt
[1].c_str());
746 *f
<< stringf("-- SMV description generated by %s\n", yosys_version_str
);
748 log("Creating SMV representation of module %s.\n", log_id(module
));
749 SmvWorker
worker(module
, verbose
, *f
);
752 *f
<< stringf("-- end of yosys output\n");
756 log_error("Unknown template statement: '%s'", line
.c_str() + indent
);
759 *f
<< line
<< std::endl
;
763 if (!modules
.empty())
765 *f
<< stringf("-- SMV description generated by %s\n", yosys_version_str
);
767 for (auto module
: modules
) {
768 log("Creating SMV representation of module %s.\n", log_id(module
));
769 SmvWorker
worker(module
, verbose
, *f
);
773 *f
<< stringf("-- end of yosys output\n");
776 if (template_f
.is_open()) {
778 while (std::getline(template_f
, line
))
779 *f
<< line
<< std::endl
;
784 PRIVATE_NAMESPACE_END