e41582fea4af14e03cf4bc5a9b6ec160f9d9bed6
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
> inputvars
, vars
, definitions
, 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
.compare(0, 2, "_\\") == 0)
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
));
214 for (auto wire
: module
->wires())
216 if (SigSpec(wire
) != sigmap(wire
))
217 partial_assignment_wires
.insert(wire
);
219 if (wire
->port_input
)
220 inputvars
.push_back(stringf("%s : unsigned word[%d]; -- %s", cid(wire
->name
), wire
->width
, log_id(wire
)));
222 if (wire
->attributes
.count(ID::init
))
223 assignments
.push_back(stringf("init(%s) := %s;", lvalue(wire
), rvalue(wire
->attributes
.at(ID::init
))));
226 for (auto cell
: module
->cells())
228 // FIXME: $slice, $concat, $mem
230 if (cell
->type
.in(ID($
assert)))
232 SigSpec sig_a
= cell
->getPort(ID::A
);
233 SigSpec sig_en
= cell
->getPort(ID::EN
);
235 invarspecs
.push_back(stringf("!bool(%s) | bool(%s);", rvalue(sig_en
), rvalue(sig_a
)));
240 if (cell
->type
.in(ID($shl
), ID($shr
), ID($sshl
), ID($sshr
), ID($shift
), ID($shiftx
)))
242 SigSpec sig_a
= cell
->getPort(ID::A
);
243 SigSpec sig_b
= cell
->getPort(ID::B
);
245 int width_y
= GetSize(cell
->getPort(ID::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(ID::A_SIGNED
).as_bool();
258 bool signed_b
= cell
->getParam(ID::B_SIGNED
).as_bool();
259 string op
= cell
->type
.in(ID($shl
), ID($sshl
)) ? "<<" : ">>";
262 if (cell
->type
== ID($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(ID($shift
), ID($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 definitions
.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(ID($shift
), ID($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 definitions
.push_back(stringf("%s := %s;", lvalue(cell
->getPort(ID::Y
)), expr
.c_str()));
311 if (cell
->type
.in(ID($
not), ID($pos
), ID($neg
)))
313 int width
= GetSize(cell
->getPort(ID::Y
));
316 if (cell
->type
== ID($
not)) op
= "!";
317 if (cell
->type
== ID($pos
)) op
= "";
318 if (cell
->type
== ID($neg
)) op
= "-";
320 if (cell
->getParam(ID::A_SIGNED
).as_bool())
322 definitions
.push_back(stringf("%s := unsigned(%s%s);", lvalue(cell
->getPort(ID::Y
)),
323 op
.c_str(), rvalue_s(cell
->getPort(ID::A
), width
)));
327 definitions
.push_back(stringf("%s := %s%s;", lvalue(cell
->getPort(ID::Y
)),
328 op
.c_str(), rvalue_u(cell
->getPort(ID::A
), width
)));
334 if (cell
->type
.in(ID($add
), ID($sub
), ID($mul
), ID($
and), ID($
or), ID($
xor), ID($xnor
)))
336 int width
= GetSize(cell
->getPort(ID::Y
));
337 string expr_a
, expr_b
, op
;
339 if (cell
->type
== ID($add
)) op
= "+";
340 if (cell
->type
== ID($sub
)) op
= "-";
341 if (cell
->type
== ID($mul
)) op
= "*";
342 if (cell
->type
== ID($
and)) op
= "&";
343 if (cell
->type
== ID($
or)) op
= "|";
344 if (cell
->type
== ID($
xor)) op
= "xor";
345 if (cell
->type
== ID($xnor
)) op
= "xnor";
347 if (cell
->getParam(ID::A_SIGNED
).as_bool())
349 definitions
.push_back(stringf("%s := unsigned(%s %s %s);", lvalue(cell
->getPort(ID::Y
)),
350 rvalue_s(cell
->getPort(ID::A
), width
), op
.c_str(), rvalue_s(cell
->getPort(ID::B
), width
)));
354 definitions
.push_back(stringf("%s := %s %s %s;", lvalue(cell
->getPort(ID::Y
)),
355 rvalue_u(cell
->getPort(ID::A
), width
), op
.c_str(), rvalue_u(cell
->getPort(ID::B
), width
)));
361 // SMV has a "mod" operator, but its semantics don't seem to be well-defined - to be safe, don't generate it at all
362 if (cell
->type
.in(ID($div
)/*, ID($mod), ID($modfloor)*/))
364 int width_y
= GetSize(cell
->getPort(ID::Y
));
365 int width
= max(width_y
, GetSize(cell
->getPort(ID::A
)));
366 width
= max(width
, GetSize(cell
->getPort(ID::B
)));
367 string expr_a
, expr_b
, op
;
369 if (cell
->type
== ID($div
)) op
= "/";
370 //if (cell->type == ID($mod)) op = "mod";
372 if (cell
->getParam(ID::A_SIGNED
).as_bool())
374 definitions
.push_back(stringf("%s := resize(unsigned(%s %s %s), %d);", lvalue(cell
->getPort(ID::Y
)),
375 rvalue_s(cell
->getPort(ID::A
), width
), op
.c_str(), rvalue_s(cell
->getPort(ID::B
), width
), width_y
));
379 definitions
.push_back(stringf("%s := resize(%s %s %s, %d);", lvalue(cell
->getPort(ID::Y
)),
380 rvalue_u(cell
->getPort(ID::A
), width
), op
.c_str(), rvalue_u(cell
->getPort(ID::B
), width
), width_y
));
386 if (cell
->type
.in(ID($eq
), ID($ne
), ID($eqx
), ID($nex
), ID($lt
), ID($le
), ID($ge
), ID($gt
)))
388 int width
= max(GetSize(cell
->getPort(ID::A
)), GetSize(cell
->getPort(ID::B
)));
389 string expr_a
, expr_b
, op
;
391 if (cell
->type
== ID($eq
)) op
= "=";
392 if (cell
->type
== ID($ne
)) op
= "!=";
393 if (cell
->type
== ID($eqx
)) op
= "=";
394 if (cell
->type
== ID($nex
)) op
= "!=";
395 if (cell
->type
== ID($lt
)) op
= "<";
396 if (cell
->type
== ID($le
)) op
= "<=";
397 if (cell
->type
== ID($ge
)) op
= ">=";
398 if (cell
->type
== ID($gt
)) op
= ">";
400 if (cell
->getParam(ID::A_SIGNED
).as_bool())
402 expr_a
= stringf("resize(signed(%s), %d)", rvalue(cell
->getPort(ID::A
)), width
);
403 expr_b
= stringf("resize(signed(%s), %d)", rvalue(cell
->getPort(ID::B
)), width
);
407 expr_a
= stringf("resize(%s, %d)", rvalue(cell
->getPort(ID::A
)), width
);
408 expr_b
= stringf("resize(%s, %d)", rvalue(cell
->getPort(ID::B
)), width
);
411 definitions
.push_back(stringf("%s := resize(word1(%s %s %s), %d);", lvalue(cell
->getPort(ID::Y
)),
412 expr_a
.c_str(), op
.c_str(), expr_b
.c_str(), GetSize(cell
->getPort(ID::Y
))));
417 if (cell
->type
.in(ID($reduce_and
), ID($reduce_or
), ID($reduce_bool
)))
419 int width_a
= GetSize(cell
->getPort(ID::A
));
420 int width_y
= GetSize(cell
->getPort(ID::Y
));
421 const char *expr_a
= rvalue(cell
->getPort(ID::A
));
422 const char *expr_y
= lvalue(cell
->getPort(ID::Y
));
425 if (cell
->type
== ID($reduce_and
)) expr
= stringf("%s = !0ub%d_0", expr_a
, width_a
);
426 if (cell
->type
== ID($reduce_or
)) expr
= stringf("%s != 0ub%d_0", expr_a
, width_a
);
427 if (cell
->type
== ID($reduce_bool
)) expr
= stringf("%s != 0ub%d_0", expr_a
, width_a
);
429 definitions
.push_back(stringf("%s := resize(word1(%s), %d);", expr_y
, expr
.c_str(), width_y
));
433 if (cell
->type
.in(ID($reduce_xor
), ID($reduce_xnor
)))
435 int width_y
= GetSize(cell
->getPort(ID::Y
));
436 const char *expr_y
= lvalue(cell
->getPort(ID::Y
));
439 for (auto bit
: cell
->getPort(ID::A
)) {
445 if (cell
->type
== ID($reduce_xnor
))
446 expr
= "!(" + expr
+ ")";
448 definitions
.push_back(stringf("%s := resize(%s, %d);", expr_y
, expr
.c_str(), width_y
));
452 if (cell
->type
.in(ID($logic_and
), ID($logic_or
)))
454 int width_a
= GetSize(cell
->getPort(ID::A
));
455 int width_b
= GetSize(cell
->getPort(ID::B
));
456 int width_y
= GetSize(cell
->getPort(ID::Y
));
458 string expr_a
= stringf("(%s != 0ub%d_0)", rvalue(cell
->getPort(ID::A
)), width_a
);
459 string expr_b
= stringf("(%s != 0ub%d_0)", rvalue(cell
->getPort(ID::B
)), width_b
);
460 const char *expr_y
= lvalue(cell
->getPort(ID::Y
));
463 if (cell
->type
== ID($logic_and
)) expr
= expr_a
+ " & " + expr_b
;
464 if (cell
->type
== ID($logic_or
)) expr
= expr_a
+ " | " + expr_b
;
466 definitions
.push_back(stringf("%s := resize(word1(%s), %d);", expr_y
, expr
.c_str(), width_y
));
470 if (cell
->type
.in(ID($logic_not
)))
472 int width_a
= GetSize(cell
->getPort(ID::A
));
473 int width_y
= GetSize(cell
->getPort(ID::Y
));
475 string expr_a
= stringf("(%s = 0ub%d_0)", rvalue(cell
->getPort(ID::A
)), width_a
);
476 const char *expr_y
= lvalue(cell
->getPort(ID::Y
));
478 definitions
.push_back(stringf("%s := resize(word1(%s), %d);", expr_y
, expr_a
.c_str(), width_y
));
482 if (cell
->type
.in(ID($mux
), ID($pmux
)))
484 int width
= GetSize(cell
->getPort(ID::Y
));
485 SigSpec sig_a
= cell
->getPort(ID::A
);
486 SigSpec sig_b
= cell
->getPort(ID::B
);
487 SigSpec sig_s
= cell
->getPort(ID::S
);
490 for (int i
= 0; i
< GetSize(sig_s
); i
++)
491 expr
+= stringf("bool(%s) ? %s : ", rvalue(sig_s
[i
]), rvalue(sig_b
.extract(i
*width
, width
)));
492 expr
+= rvalue(sig_a
);
494 definitions
.push_back(stringf("%s := %s;", lvalue(cell
->getPort(ID::Y
)), expr
.c_str()));
498 if (cell
->type
== ID($dff
))
500 vars
.push_back(stringf("%s : unsigned word[%d]; -- %s", lvalue(cell
->getPort(ID::Q
)), GetSize(cell
->getPort(ID::Q
)), log_signal(cell
->getPort(ID::Q
))));
501 assignments
.push_back(stringf("next(%s) := %s;", lvalue(cell
->getPort(ID::Q
)), rvalue(cell
->getPort(ID::D
))));
505 if (cell
->type
.in(ID($_BUF_
), ID($_NOT_
)))
507 string op
= cell
->type
== ID($_NOT_
) ? "!" : "";
508 definitions
.push_back(stringf("%s := %s%s;", lvalue(cell
->getPort(ID::Y
)), op
.c_str(), rvalue(cell
->getPort(ID::A
))));
512 if (cell
->type
.in(ID($_AND_
), ID($_NAND_
), ID($_OR_
), ID($_NOR_
), ID($_XOR_
), ID($_XNOR_
), ID($_ANDNOT_
), ID($_ORNOT_
)))
516 if (cell
->type
.in(ID($_AND_
), ID($_NAND_
), ID($_ANDNOT_
))) op
= "&";
517 if (cell
->type
.in(ID($_OR_
), ID($_NOR_
), ID($_ORNOT_
))) op
= "|";
518 if (cell
->type
.in(ID($_XOR_
))) op
= "xor";
519 if (cell
->type
.in(ID($_XNOR_
))) op
= "xnor";
521 if (cell
->type
.in(ID($_ANDNOT_
), ID($_ORNOT_
)))
522 definitions
.push_back(stringf("%s := %s %s (!%s);", lvalue(cell
->getPort(ID::Y
)),
523 rvalue(cell
->getPort(ID::A
)), op
.c_str(), rvalue(cell
->getPort(ID::B
))));
525 if (cell
->type
.in(ID($_NAND_
), ID($_NOR_
)))
526 definitions
.push_back(stringf("%s := !(%s %s %s);", lvalue(cell
->getPort(ID::Y
)),
527 rvalue(cell
->getPort(ID::A
)), op
.c_str(), rvalue(cell
->getPort(ID::B
))));
529 definitions
.push_back(stringf("%s := %s %s %s;", lvalue(cell
->getPort(ID::Y
)),
530 rvalue(cell
->getPort(ID::A
)), op
.c_str(), rvalue(cell
->getPort(ID::B
))));
534 if (cell
->type
== ID($_MUX_
))
536 definitions
.push_back(stringf("%s := bool(%s) ? %s : %s;", lvalue(cell
->getPort(ID::Y
)),
537 rvalue(cell
->getPort(ID::S
)), rvalue(cell
->getPort(ID::B
)), rvalue(cell
->getPort(ID::A
))));
541 if (cell
->type
== ID($_NMUX_
))
543 definitions
.push_back(stringf("%s := !(bool(%s) ? %s : %s);", lvalue(cell
->getPort(ID::Y
)),
544 rvalue(cell
->getPort(ID::S
)), rvalue(cell
->getPort(ID::B
)), rvalue(cell
->getPort(ID::A
))));
548 if (cell
->type
== ID($_AOI3_
))
550 definitions
.push_back(stringf("%s := !((%s & %s) | %s);", lvalue(cell
->getPort(ID::Y
)),
551 rvalue(cell
->getPort(ID::A
)), rvalue(cell
->getPort(ID::B
)), rvalue(cell
->getPort(ID::C
))));
555 if (cell
->type
== ID($_OAI3_
))
557 definitions
.push_back(stringf("%s := !((%s | %s) & %s);", lvalue(cell
->getPort(ID::Y
)),
558 rvalue(cell
->getPort(ID::A
)), rvalue(cell
->getPort(ID::B
)), rvalue(cell
->getPort(ID::C
))));
562 if (cell
->type
== ID($_AOI4_
))
564 definitions
.push_back(stringf("%s := !((%s & %s) | (%s & %s));", lvalue(cell
->getPort(ID::Y
)),
565 rvalue(cell
->getPort(ID::A
)), rvalue(cell
->getPort(ID::B
)), rvalue(cell
->getPort(ID::C
)), rvalue(cell
->getPort(ID::D
))));
569 if (cell
->type
== ID($_OAI4_
))
571 definitions
.push_back(stringf("%s := !((%s | %s) & (%s | %s));", lvalue(cell
->getPort(ID::Y
)),
572 rvalue(cell
->getPort(ID::A
)), rvalue(cell
->getPort(ID::B
)), rvalue(cell
->getPort(ID::C
)), rvalue(cell
->getPort(ID::D
))));
576 if (cell
->type
[0] == '$') {
577 if (cell
->type
.in(ID($dffe
), ID($sdff
), ID($sdffe
), ID($sdffce
)) || cell
->type
.str().substr(0, 6) == "$_SDFF" || (cell
->type
.str().substr(0, 6) == "$_DFFE" && cell
->type
.str().size() == 10)) {
578 log_error("Unsupported cell type %s for cell %s.%s -- please run `dffunmap` before `write_smv`.\n",
579 log_id(cell
->type
), log_id(module
), log_id(cell
));
581 if (cell
->type
.in(ID($adff
), ID($adffe
), ID($dffsr
), ID($dffsre
)) || cell
->type
.str().substr(0, 5) == "$_DFF") {
582 log_error("Unsupported cell type %s for cell %s.%s -- please run `async2sync; dffunmap` or `clk2fflogic` before `write_smv`.\n",
583 log_id(cell
->type
), log_id(module
), log_id(cell
));
585 if (cell
->type
.in(ID($sr
), ID($dlatch
), ID($adlatch
), ID($dlatchsr
)) || cell
->type
.str().substr(0, 8) == "$_DLATCH" || cell
->type
.str().substr(0, 5) == "$_SR_") {
586 log_error("Unsupported cell type %s for cell %s.%s -- please run `clk2fflogic` before `write_smv`.\n",
587 log_id(cell
->type
), log_id(module
), log_id(cell
));
589 log_error("Unsupported cell type %s for cell %s.%s.\n",
590 log_id(cell
->type
), log_id(module
), log_id(cell
));
593 // f << stringf(" %s : %s;\n", cid(cell->name), cid(cell->type));
595 for (auto &conn
: cell
->connections())
596 if (cell
->output(conn
.first
))
597 definitions
.push_back(stringf("%s := %s.%s;", lvalue(conn
.second
), cid(cell
->name
), cid(conn
.first
)));
599 definitions
.push_back(stringf("%s.%s := %s;", cid(cell
->name
), cid(conn
.first
), rvalue(conn
.second
)));
602 for (Wire
*wire
: partial_assignment_wires
)
606 for (int i
= 0; i
< wire
->width
; i
++)
609 expr
= " :: " + expr
;
611 if (partial_assignment_bits
.count(sigmap(SigBit(wire
, i
))))
614 const auto &bit_a
= partial_assignment_bits
.at(sigmap(SigBit(wire
, i
)));
616 while (i
+1 < wire
->width
)
618 SigBit next_bit
= sigmap(SigBit(wire
, i
+1));
620 if (!partial_assignment_bits
.count(next_bit
))
623 const auto &bit_b
= partial_assignment_bits
.at(next_bit
);
624 if (strcmp(bit_a
.first
, bit_b
.first
))
626 if (bit_a
.second
+width
!= bit_b
.second
)
632 expr
= stringf("%s[%d:%d]", bit_a
.first
, bit_a
.second
+width
-1, bit_a
.second
) + expr
;
634 else if (sigmap(SigBit(wire
, i
)).wire
== nullptr)
637 SigSpec sig
= sigmap(SigSpec(wire
, i
));
639 while (i
+1 < wire
->width
) {
640 SigBit next_bit
= sigmap(SigBit(wire
, i
+1));
641 if (next_bit
.wire
!= nullptr)
643 sig
.append(next_bit
);
647 for (int k
= GetSize(sig
)-1; k
>= 0; k
--)
648 bits
+= sig
[k
] == State::S1
? '1' : '0';
650 expr
= stringf("0ub%d_%s", GetSize(bits
), bits
.c_str()) + expr
;
652 else if (sigmap(SigBit(wire
, i
)) == SigBit(wire
, i
))
656 while (i
+1 < wire
->width
) {
657 if (partial_assignment_bits
.count(sigmap(SigBit(wire
, i
+1))))
659 if (sigmap(SigBit(wire
, i
+1)) != SigBit(wire
, i
+1))
664 expr
= stringf("0ub%d_0", length
) + expr
;
669 SigSpec sig
= sigmap(SigSpec(wire
, i
));
671 while (i
+1 < wire
->width
) {
672 SigBit next_bit
= sigmap(SigBit(wire
, i
+1));
673 if (next_bit
.wire
== nullptr || partial_assignment_bits
.count(next_bit
))
675 sig
.append(next_bit
);
679 expr
= rvalue(sig
) + expr
;
683 definitions
.push_back(stringf("%s := %s;", cid(wire
->name
), expr
.c_str()));
686 if (!inputvars
.empty()) {
687 f
<< stringf(" IVAR\n");
688 for (const string
&line
: inputvars
)
689 f
<< stringf(" %s\n", line
.c_str());
693 f
<< stringf(" VAR\n");
694 for (const string
&line
: vars
)
695 f
<< stringf(" %s\n", line
.c_str());
698 if (!definitions
.empty()) {
699 f
<< stringf(" DEFINE\n");
700 for (const string
&line
: definitions
)
701 f
<< stringf(" %s\n", line
.c_str());
704 if (!assignments
.empty()) {
705 f
<< stringf(" ASSIGN\n");
706 for (const string
&line
: assignments
)
707 f
<< stringf(" %s\n", line
.c_str());
710 if (!invarspecs
.empty()) {
711 for (const string
&line
: invarspecs
)
712 f
<< stringf(" INVARSPEC %s\n", line
.c_str());
717 struct SmvBackend
: public Backend
{
718 SmvBackend() : Backend("smv", "write design to SMV file") { }
721 // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
723 log(" write_smv [options] [filename]\n");
725 log("Write an SMV description of the current design.\n");
728 log(" this will print the recursive walk used to export the modules.\n");
730 log(" -tpl <template_file>\n");
731 log(" use the given template file. the line containing only the token '%%%%'\n");
732 log(" is replaced with the regular output of this command.\n");
734 log("THIS COMMAND IS UNDER CONSTRUCTION\n");
737 void execute(std::ostream
*&f
, std::string filename
, std::vector
<std::string
> args
, RTLIL::Design
*design
) override
739 std::ifstream template_f
;
740 bool verbose
= false;
742 log_header(design
, "Executing SMV backend.\n");
745 for (argidx
= 1; argidx
< args
.size(); argidx
++)
747 if (args
[argidx
] == "-tpl" && argidx
+1 < args
.size()) {
748 template_f
.open(args
[++argidx
]);
749 if (template_f
.fail())
750 log_error("Can't open template file `%s'.\n", args
[argidx
].c_str());
753 if (args
[argidx
] == "-verbose") {
759 extra_args(f
, filename
, args
, argidx
);
761 pool
<Module
*> modules
;
763 for (auto module
: design
->modules())
764 if (!module
->get_blackbox_attribute() && !module
->has_memories_warn() && !module
->has_processes_warn())
765 modules
.insert(module
);
767 if (template_f
.is_open())
770 while (std::getline(template_f
, line
))
773 while (indent
< GetSize(line
) && (line
[indent
] == ' ' || line
[indent
] == '\t'))
776 if (line
[indent
] == '%')
778 vector
<string
> stmt
= split_tokens(line
);
780 if (GetSize(stmt
) == 1 && stmt
[0] == "%%")
783 if (GetSize(stmt
) == 2 && stmt
[0] == "%module")
785 Module
*module
= design
->module(RTLIL::escape_id(stmt
[1]));
786 modules
.erase(module
);
788 if (module
== nullptr)
789 log_error("Module '%s' not found.\n", stmt
[1].c_str());
791 *f
<< stringf("-- SMV description generated by %s\n", yosys_version_str
);
793 log("Creating SMV representation of module %s.\n", log_id(module
));
794 SmvWorker
worker(module
, verbose
, *f
);
797 *f
<< stringf("-- end of yosys output\n");
801 log_error("Unknown template statement: '%s'", line
.c_str() + indent
);
804 *f
<< line
<< std::endl
;
808 if (!modules
.empty())
810 *f
<< stringf("-- SMV description generated by %s\n", yosys_version_str
);
812 for (auto module
: modules
) {
813 log("Creating SMV representation of module %s.\n", log_id(module
));
814 SmvWorker
worker(module
, verbose
, *f
);
818 *f
<< stringf("-- end of yosys output\n");
821 if (template_f
.is_open()) {
823 while (std::getline(template_f
, line
))
824 *f
<< line
<< std::endl
;
829 PRIVATE_NAMESPACE_END