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