projects / yosys.git / blob
? search:
summary | shortlog | log | commit | commitdiff | tree
history | raw | HEAD
Merge pull request #55 from ahmedirfan1983/master
[yosys.git] / backends / btor / btor.cc
1 /*
2 * yosys -- Yosys Open SYnthesis Suite
3 *
4 * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
5 * Copyright (C) 2014 Ahmed Irfan <irfan@fbk.eu>
6 *
7 * Permission to use, copy, modify, and/or distribute this software for any
8 * purpose with or without fee is hereby granted, provided that the above
9 * copyright notice and this permission notice appear in all copies.
10 *
11 * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
12 * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
13 * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
14 * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
15 * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
16 * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
17 * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
18 *
19 */
20
21 // [[CITE]] BTOR: Bit-Precise Modelling of Word-Level Problems for Model Checking
22 // Johannes Kepler University, Linz, Austria
23 // http://fmv.jku.at/papers/BrummayerBiereLonsing-BPR08.pdf
24
25 #include "kernel/rtlil.h"
26 #include "kernel/register.h"
27 #include "kernel/sigtools.h"
28 #include "kernel/celltypes.h"
29 #include "kernel/log.h"
30 #include <string>
31 #include <math.h>
32
33 USING_YOSYS_NAMESPACE
34 PRIVATE_NAMESPACE_BEGIN
35
36 struct BtorDumperConfig
37 {
38 bool subckt_mode;
39 bool conn_mode;
40 bool impltf_mode;
41
42 std::string buf_type, buf_in, buf_out;
43 std::string true_type, true_out, false_type, false_out;
44
45 BtorDumperConfig() : subckt_mode(false), conn_mode(false), impltf_mode(false) { }
46 };
47
48 struct WireInfo
49 {
50 RTLIL::IdString cell_name;
51 const RTLIL::SigChunk *chunk;
52
53 WireInfo(RTLIL::IdString c, const RTLIL::SigChunk* ch) : cell_name(c), chunk(ch) { }
54 };
55
56 struct WireInfoOrder
57 {
58 bool operator() (const WireInfo& x, const WireInfo& y)
59 {
60 return x.chunk < y.chunk;
61 }
62 };
63
64 struct BtorDumper
65 {
66 std::ostream &f;
67 RTLIL::Module *module;
68 RTLIL::Design *design;
69 BtorDumperConfig *config;
70 CellTypes ct;
71
72 SigMap sigmap;
73 std::map<RTLIL::IdString, std::set<WireInfo,WireInfoOrder>> inter_wire_map;//<wire, dependency list> for maping the intermediate wires that are output of some cell
74 std::map<RTLIL::IdString, int> line_ref;//mapping of ids to line_num of the btor file
75 std::map<RTLIL::SigSpec, int> sig_ref;//mapping of sigspec to the line_num of the btor file
76 int line_num;//last line number of btor file
77 std::string str;//temp string for writing file
78 std::map<RTLIL::IdString, bool> basic_wires;//input wires and registers
79 RTLIL::IdString curr_cell; //current cell being dumped
80 std::map<std::string, std::string> cell_type_translation, s_cell_type_translation; //RTLIL to BTOR translation
81 std::map<int, std::set<std::pair<int,int>>> mem_next; // memory (line_number)'s set of condition and write
82 BtorDumper(std::ostream &f, RTLIL::Module *module, RTLIL::Design *design, BtorDumperConfig *config) :
83 f(f), module(module), design(design), config(config), ct(design), sigmap(module)
84 {
85 line_num=0;
86 str.clear();
87 for(auto it=module->wires_.begin(); it!=module->wires_.end(); ++it)
88 {
89 if(it->second->port_input)
90 {
91 basic_wires[it->first]=true;
92 }
93 else
94 {
95 basic_wires[it->first]=false;
96 }
97 inter_wire_map[it->first].clear();
98 }
99 curr_cell.clear();
100 //assert
101 cell_type_translation["$assert"] = "root";
102 //unary
103 cell_type_translation["$not"] = "not";
104 cell_type_translation["$neg"] = "neg";
105 cell_type_translation["$reduce_and"] = "redand";
106 cell_type_translation["$reduce_or"] = "redor";
107 cell_type_translation["$reduce_xor"] = "redxor";
108 cell_type_translation["$reduce_bool"] = "redor";
109 //binary
110 cell_type_translation["$and"] = "and";
111 cell_type_translation["$or"] = "or";
112 cell_type_translation["$xor"] = "xor";
113 cell_type_translation["$xnor"] = "xnor";
114 cell_type_translation["$shr"] = "srl";
115 cell_type_translation["$shl"] = "sll";
116 cell_type_translation["$sshr"] = "sra";
117 cell_type_translation["$sshl"] = "sll";
118 cell_type_translation["$shift"] = "srl";
119 cell_type_translation["$shiftx"] = "srl";
120 cell_type_translation["$lt"] = "ult";
121 cell_type_translation["$le"] = "ulte";
122 cell_type_translation["$gt"] = "ugt";
123 cell_type_translation["$ge"] = "ugte";
124 cell_type_translation["$eq"] = "eq";
125 cell_type_translation["$eqx"] = "eq";
126 cell_type_translation["$ne"] = "ne";
127 cell_type_translation["$nex"] = "ne";
128 cell_type_translation["$add"] = "add";
129 cell_type_translation["$sub"] = "sub";
130 cell_type_translation["$mul"] = "mul";
131 cell_type_translation["$mod"] = "urem";
132 cell_type_translation["$div"] = "udiv";
133 //mux
134 cell_type_translation["$mux"] = "cond";
135 //reg
136 cell_type_translation["$dff"] = "next";
137 cell_type_translation["$adff"] = "next";
138 cell_type_translation["$dffsr"] = "next";
139 //memories
140 //nothing here
141 //slice
142 cell_type_translation["$slice"] = "slice";
143 //concat
144 cell_type_translation["$concat"] = "concat";
145
146 //signed cell type translation
147 //binary
148 s_cell_type_translation["$modx"] = "srem";
149 s_cell_type_translation["$mody"] = "smod";
150 s_cell_type_translation["$div"] = "sdiv";
151 s_cell_type_translation["$lt"] = "slt";
152 s_cell_type_translation["$le"] = "slte";
153 s_cell_type_translation["$gt"] = "sgt";
154 s_cell_type_translation["$ge"] = "sgte";
155
156 }
157
158 std::vector<std::string> cstr_buf;
159
160 const char *cstr(const RTLIL::IdString id)
161 {
162 str = RTLIL::unescape_id(id);
163 for (size_t i = 0; i < str.size(); ++i)
164 if (str[i] == '#' || str[i] == '=')
165 str[i] = '?';
166 cstr_buf.push_back(str);
167 return cstr_buf.back().c_str();
168 }
169
170 int dump_wire(RTLIL::Wire* wire)
171 {
172 if(basic_wires[wire->name])
173 {
174 log("writing wire %s\n", cstr(wire->name));
175 auto it = line_ref.find(wire->name);
176 if(it==std::end(line_ref))
177 {
178 ++line_num;
179 line_ref[wire->name]=line_num;
180 str = stringf("%d var %d %s", line_num, wire->width, cstr(wire->name));
181 f << stringf("%s\n", str.c_str());
182 return line_num;
183 }
184 else return it->second;
185 }
186 else // case when the wire is not basic wire
187 {
188 log("case of non-basic wire - %s\n", cstr(wire->name));
189 auto it = line_ref.find(wire->name);
190 if(it==std::end(line_ref))
191 {
192 std::set<WireInfo, WireInfoOrder>& dep_set = inter_wire_map.at(wire->name);
193 int wire_line = 0;
194 int wire_width = 0;
195 for(auto dep_set_it=dep_set.begin(); dep_set_it!=dep_set.end(); ++dep_set_it)
196 {
197 RTLIL::IdString cell_id = dep_set_it->cell_name;
198 if(cell_id == curr_cell)
199 break;
200 log(" -- found cell %s\n", cstr(cell_id));
201 RTLIL::Cell* cell = module->cells_.at(cell_id);
202 const RTLIL::SigSpec* cell_output = get_cell_output(cell);
203 int cell_line = dump_cell(cell);
204
205 if(dep_set.size()==1 && wire->width == cell_output->size())
206 {
207 wire_line = cell_line;
208 break;
209 }
210 else
211 {
212 int prev_wire_line=0; //previously dumped wire line
213 int start_bit=0;
214 for(unsigned j=0; j<cell_output->chunks().size(); ++j)
215 {
216 start_bit+=cell_output->chunks().at(j).width;
217 if(cell_output->chunks().at(j).wire->name == wire->name)
218 {
219 prev_wire_line = wire_line;
220 wire_line = ++line_num;
221 str = stringf("%d slice %d %d %d %d;1", line_num, cell_output->chunks().at(j).width,
222 cell_line, start_bit-1, start_bit-cell_output->chunks().at(j).width);
223 f << stringf("%s\n", str.c_str());
224 wire_width += cell_output->chunks().at(j).width;
225 if(prev_wire_line!=0)
226 {
227 ++line_num;
228 str = stringf("%d concat %d %d %d", line_num, wire_width, wire_line, prev_wire_line);
229 f << stringf("%s\n", str.c_str());
230 wire_line = line_num;
231 }
232 }
233 }
234 }
235 }
236 if(dep_set.size()==0)
237 {
238 log(" - checking sigmap\n");
239 RTLIL::SigSpec s = RTLIL::SigSpec(wire);
240 wire_line = dump_sigspec(&s, s.size());
241 line_ref[wire->name]=wire_line;
242 }
243 line_ref[wire->name]=wire_line;
244 return wire_line;
245 }
246 else
247 {
248 log(" -- already processed wire\n");
249 return it->second;
250 }
251 }
252 log_abort();
253 return -1;
254 }
255
256 int dump_memory(const RTLIL::Memory* memory)
257 {
258 log("writing memory %s\n", cstr(memory->name));
259 auto it = line_ref.find(memory->name);
260 if(it==std::end(line_ref))
261 {
262 ++line_num;
263 int address_bits = ceil(log(memory->size)/log(2));
264 str = stringf("%d array %d %d", line_num, memory->width, address_bits);
265 line_ref[memory->name]=line_num;
266 f << stringf("%s\n", str.c_str());
267 return line_num;
268 }
269 else return it->second;
270 }
271
272 int dump_memory_next(const RTLIL::Memory* memory)
273 {
274 auto mem_it = line_ref.find(memory->name);
275 int address_bits = ceil(log(memory->size)/log(2));
276 if(mem_it==std::end(line_ref))
277 {
278 log("can not write next of a memory that is not dumped yet\n");
279 log_abort();
280 }
281 else
282 {
283 auto acond_list_it = mem_next.find(mem_it->second);
284 if(acond_list_it!=std::end(mem_next))
285 {
286 std::set<std::pair<int,int>>& cond_list = acond_list_it->second;
287 if(cond_list.empty())
288 {
289 return 0;
290 }
291 auto it=cond_list.begin();
292 ++line_num;
293 str = stringf("%d acond %d %d %d %d %d", line_num, memory->width, address_bits, it->first, it->second, mem_it->second);
294 f << stringf("%s\n", str.c_str());
295 ++it;
296 for(; it!=cond_list.end(); ++it)
297 {
298 ++line_num;
299 str = stringf("%d acond %d %d %d %d %d", line_num, memory->width, address_bits, it->first, it->second, line_num-1);
300 f << stringf("%s\n", str.c_str());
301 }
302 ++line_num;
303 str = stringf("%d anext %d %d %d %d", line_num, memory->width, address_bits, mem_it->second, line_num-1);
304 f << stringf("%s\n", str.c_str());
305 return 1;
306 }
307 return 0;
308 }
309 }
310
311 int dump_const(const RTLIL::Const* data, int width, int offset)
312 {
313 log("writing const \n");
314 if((data->flags & RTLIL::CONST_FLAG_STRING) == 0)
315 {
316 if(width<0)
317 width = data->bits.size() - offset;
318
319 std::string data_str = data->as_string();
320 //if(offset > 0)
321 data_str = data_str.substr(offset, width);
322
323 ++line_num;
324 str = stringf("%d const %d %s", line_num, width, data_str.c_str());
325 f << stringf("%s\n", str.c_str());
326 return line_num;
327 }
328 else
329 log("writing const error\n");
330 log_abort();
331 return -1;
332 }
333
334 int dump_sigchunk(const RTLIL::SigChunk* chunk)
335 {
336 log("writing sigchunk\n");
337 int l=-1;
338 if(chunk->wire == NULL)
339 {
340 RTLIL::Const data_const(chunk->data);
341 l=dump_const(&data_const, chunk->width, chunk->offset);
342 }
343 else
344 {
345 if (chunk->width == chunk->wire->width && chunk->offset == 0)
346 l = dump_wire(chunk->wire);
347 else
348 {
349 int wire_line_num = dump_wire(chunk->wire);
350 log_assert(wire_line_num>0);
351 ++line_num;
352 str = stringf("%d slice %d %d %d %d;2", line_num, chunk->width, wire_line_num,
353 chunk->width + chunk->offset - 1, chunk->offset);
354 f << stringf("%s\n", str.c_str());
355 l = line_num;
356 }
357 }
358 return l;
359 }
360
361 int dump_sigspec(const RTLIL::SigSpec* sig, int expected_width)
362 {
363 log("writing sigspec\n");
364 RTLIL::SigSpec s = sigmap(*sig);
365 int l = -1;
366 auto it = sig_ref.find(s);
367 if(it == std::end(sig_ref))
368 {
369 if (s.is_chunk())
370 {
371 l = dump_sigchunk(&s.chunks().front());
372 }
373 else
374 {
375 int l1, l2, w1, w2;
376 l1 = dump_sigchunk(&s.chunks().front());
377 log_assert(l1>0);
378 w1 = s.chunks().front().width;
379 for (unsigned i=1; i < s.chunks().size(); ++i)
380 {
381 l2 = dump_sigchunk(&s.chunks().at(i));
382 log_assert(l2>0);
383 w2 = s.chunks().at(i).width;
384 ++line_num;
385 str = stringf("%d concat %d %d %d", line_num, w1+w2, l2, l1);
386 f << stringf("%s\n", str.c_str());
387 l1=line_num;
388 w1+=w2;
389 }
390 l = line_num;
391 }
392 sig_ref[s] = l;
393 }
394 else
395 {
396 l = it->second;
397 }
398
399 if (expected_width != s.size())
400 {
401 log(" - changing width of sigspec\n");
402 //TODO: this block may not be needed anymore, due to explicit type conversion by "splice" command
403 if(expected_width > s.size())
404 {
405 //TODO: case the signal is signed
406 ++line_num;
407 str = stringf ("%d zero %d", line_num, expected_width - s.size());
408 f << stringf("%s\n", str.c_str());
409 ++line_num;
410 str = stringf ("%d concat %d %d %d", line_num, expected_width, line_num-1, l);
411 f << stringf("%s\n", str.c_str());
412 l = line_num;
413 }
414 else if(expected_width < s.size())
415 {
416 ++line_num;
417 str = stringf ("%d slice %d %d %d %d;3", line_num, expected_width, l, expected_width-1, 0);
418 f << stringf("%s\n", str.c_str());
419 l = line_num;
420 }
421 }
422 log_assert(l>0);
423 return l;
424 }
425
426 int dump_cell(const RTLIL::Cell* cell)
427 {
428 auto it = line_ref.find(cell->name);
429 if(it==std::end(line_ref))
430 {
431 curr_cell = cell->name;
432 //assert cell
433 if(cell->type == "$assert")
434 {
435 log("writing assert cell - %s\n", cstr(cell->type));
436 const RTLIL::SigSpec* expr = &cell->getPort(RTLIL::IdString("\\A"));
437 const RTLIL::SigSpec* en = &cell->getPort(RTLIL::IdString("\\EN"));
438 log_assert(expr->size() == 1);
439 log_assert(en->size() == 1);
440 int expr_line = dump_sigspec(expr, 1);
441 int en_line = dump_sigspec(en, 1);
442 int one_line = ++line_num;
443 str = stringf("%d one 1", line_num);
444 f << stringf("%s\n", str.c_str());
445 ++line_num;
446 str = stringf("%d %s %d %d %d", line_num, cell_type_translation.at("$eq").c_str(), 1, en_line, one_line);
447 f << stringf("%s\n", str.c_str());
448 ++line_num;
449 str = stringf("%d %s %d %d %d %d", line_num, cell_type_translation.at("$mux").c_str(), 1, line_num-1,
450 expr_line, one_line);
451 f << stringf("%s\n", str.c_str());
452 int cell_line = ++line_num;
453 str = stringf("%d %s %d %d", line_num, cell_type_translation.at("$assert").c_str(), 1, -1*(line_num-1));
454 //multiplying the line number with -1, which means logical negation
455 //the reason for negative sign is that the properties in btor are given as "negation of the original property"
456 //bug identified by bobosoft
457 //http://www.reddit.com/r/yosys/comments/1w3xig/btor_backend_bug/
458 f << stringf("%s\n", str.c_str());
459 line_ref[cell->name]=cell_line;
460 }
461 //unary cells
462 else if(cell->type == "$not" || cell->type == "$neg" || cell->type == "$pos" || cell->type == "$reduce_and" ||
463 cell->type == "$reduce_or" || cell->type == "$reduce_xor" || cell->type == "$reduce_bool")
464 {
465 log("writing unary cell - %s\n", cstr(cell->type));
466 int w = cell->parameters.at(RTLIL::IdString("\\A_WIDTH")).as_int();
467 int output_width = cell->parameters.at(RTLIL::IdString("\\Y_WIDTH")).as_int();
468 w = w>output_width ? w:output_width; //padding of w
469 int l = dump_sigspec(&cell->getPort(RTLIL::IdString("\\A")), w);
470 int cell_line = l;
471 if(cell->type != "$pos")
472 {
473 cell_line = ++line_num;
474 bool reduced = (cell->type == "$not" || cell->type == "$neg") ? false : true;
475 str = stringf ("%d %s %d %d", cell_line, cell_type_translation.at(cell->type.str()).c_str(), reduced?output_width:w, l);
476 f << stringf("%s\n", str.c_str());
477 }
478 if(output_width < w && (cell->type == "$not" || cell->type == "$neg" || cell->type == "$pos"))
479 {
480 ++line_num;
481 str = stringf ("%d slice %d %d %d %d;4", line_num, output_width, cell_line, output_width-1, 0);
482 f << stringf("%s\n", str.c_str());
483 cell_line = line_num;
484 }
485 line_ref[cell->name]=cell_line;
486 }
487 else if(cell->type == "$reduce_xnor" || cell->type == "$logic_not")//no direct translation in btor
488 {
489 log("writing unary cell - %s\n", cstr(cell->type));
490 int w = cell->parameters.at(RTLIL::IdString("\\A_WIDTH")).as_int();
491 int output_width = cell->parameters.at(RTLIL::IdString("\\Y_WIDTH")).as_int();
492 log_assert(output_width == 1);
493 int l = dump_sigspec(&cell->getPort(RTLIL::IdString("\\A")), w);
494 if(cell->type == "$logic_not" && w > 1)
495 {
496 ++line_num;
497 str = stringf ("%d %s %d %d", line_num, cell_type_translation.at("$reduce_or").c_str(), output_width, l);
498 f << stringf("%s\n", str.c_str());
499 }
500 else if(cell->type == "$reduce_xnor")
501 {
502 ++line_num;
503 str = stringf ("%d %s %d %d", line_num, cell_type_translation.at("$reduce_xor").c_str(), output_width, l);
504 f << stringf("%s\n", str.c_str());
505 }
506 ++line_num;
507 str = stringf ("%d %s %d %d", line_num, cell_type_translation.at("$not").c_str(), output_width, l);
508 f << stringf("%s\n", str.c_str());
509 line_ref[cell->name]=line_num;
510 }
511 //binary cells
512 else if(cell->type == "$and" || cell->type == "$or" || cell->type == "$xor" || cell->type == "$xnor" ||
513 cell->type == "$lt" || cell->type == "$le" || cell->type == "$eq" || cell->type == "$ne" ||
514 cell->type == "$eqx" || cell->type == "$nex" || cell->type == "$ge" || cell->type == "$gt" )
515 {
516 log("writing binary cell - %s\n", cstr(cell->type));
517 int output_width = cell->parameters.at(RTLIL::IdString("\\Y_WIDTH")).as_int();
518 log_assert(!(cell->type == "$eq" || cell->type == "$ne" || cell->type == "$eqx" || cell->type == "$nex" ||
519 cell->type == "$ge" || cell->type == "$gt") || output_width == 1);
520 bool l1_signed = cell->parameters.at(RTLIL::IdString("\\A_SIGNED")).as_bool();
521 bool l2_signed YS_ATTRIBUTE(unused) = cell->parameters.at(RTLIL::IdString("\\B_SIGNED")).as_bool();
522 int l1_width = cell->parameters.at(RTLIL::IdString("\\A_WIDTH")).as_int();
523 int l2_width = cell->parameters.at(RTLIL::IdString("\\B_WIDTH")).as_int();
524
525 log_assert(l1_signed == l2_signed);
526 l1_width = l1_width > output_width ? l1_width : output_width;
527 l1_width = l1_width > l2_width ? l1_width : l2_width;
528 l2_width = l2_width > l1_width ? l2_width : l1_width;
529
530 int l1 = dump_sigspec(&cell->getPort(RTLIL::IdString("\\A")), l1_width);
531 int l2 = dump_sigspec(&cell->getPort(RTLIL::IdString("\\B")), l2_width);
532
533 ++line_num;
534 std::string op = cell_type_translation.at(cell->type.str());
535 if(cell->type == "$lt" || cell->type == "$le" ||
536 cell->type == "$eq" || cell->type == "$ne" || cell->type == "$eqx" || cell->type == "$nex" ||
537 cell->type == "$ge" || cell->type == "$gt")
538 {
539 if(l1_signed)
540 op = s_cell_type_translation.at(cell->type.str());
541 }
542
543 str = stringf ("%d %s %d %d %d", line_num, op.c_str(), output_width, l1, l2);
544 f << stringf("%s\n", str.c_str());
545
546 line_ref[cell->name]=line_num;
547 }
548 else if(cell->type == "$add" || cell->type == "$sub" || cell->type == "$mul" || cell->type == "$div" ||
549 cell->type == "$mod" )
550 {
551 //TODO: division by zero case
552 log("writing binary cell - %s\n", cstr(cell->type));
553 int output_width = cell->parameters.at(RTLIL::IdString("\\Y_WIDTH")).as_int();
554 bool l1_signed = cell->parameters.at(RTLIL::IdString("\\A_SIGNED")).as_bool();
555 bool l2_signed = cell->parameters.at(RTLIL::IdString("\\B_SIGNED")).as_bool();
556 int l1_width = cell->parameters.at(RTLIL::IdString("\\A_WIDTH")).as_int();
557 int l2_width = cell->parameters.at(RTLIL::IdString("\\B_WIDTH")).as_int();
558
559 log_assert(l1_signed == l2_signed);
560 l1_width = l1_width > output_width ? l1_width : output_width;
561 l1_width = l1_width > l2_width ? l1_width : l2_width;
562 l2_width = l2_width > l1_width ? l2_width : l1_width;
563
564 int l1 = dump_sigspec(&cell->getPort(RTLIL::IdString("\\A")), l1_width);
565 int l2 = dump_sigspec(&cell->getPort(RTLIL::IdString("\\B")), l2_width);
566
567 ++line_num;
568 std::string op = cell_type_translation.at(cell->type.str());
569 if(cell->type == "$div" && l1_signed)
570 op = s_cell_type_translation.at(cell->type.str());
571 else if(cell->type == "$mod")
572 {
573 if(l1_signed)
574 op = s_cell_type_translation.at("$modx");
575 else if(l2_signed)
576 op = s_cell_type_translation.at("$mody");
577 }
578 str = stringf ("%d %s %d %d %d", line_num, op.c_str(), l1_width, l1, l2);
579 f << stringf("%s\n", str.c_str());
580
581 if(output_width < l1_width)
582 {
583 ++line_num;
584 str = stringf ("%d slice %d %d %d %d;5", line_num, output_width, line_num-1, output_width-1, 0);
585 f << stringf("%s\n", str.c_str());
586 }
587 line_ref[cell->name]=line_num;
588 }
589 else if(cell->type == "$shr" || cell->type == "$shl" || cell->type == "$sshr" || cell->type == "$sshl" || cell->type == "$shift" || cell->type == "$shiftx")
590 {
591 log("writing binary cell - %s\n", cstr(cell->type));
592 int output_width = cell->parameters.at(RTLIL::IdString("\\Y_WIDTH")).as_int();
593 bool l1_signed = cell->parameters.at(RTLIL::IdString("\\A_SIGNED")).as_bool();
594 //bool l2_signed = cell->parameters.at(RTLIL::IdString("\\B_SIGNED")).as_bool();
595 int l1_width = cell->parameters.at(RTLIL::IdString("\\A_WIDTH")).as_int();
596 l1_width = pow(2, ceil(log(l1_width)/log(2)));
597 int l2_width = cell->parameters.at(RTLIL::IdString("\\B_WIDTH")).as_int();
598 //log_assert(l2_width <= ceil(log(l1_width)/log(2)) );
599 int l1 = dump_sigspec(&cell->getPort(RTLIL::IdString("\\A")), l1_width);
600 int l2 = dump_sigspec(&cell->getPort(RTLIL::IdString("\\B")), ceil(log(l1_width)/log(2)));
601 int cell_output = ++line_num;
602 str = stringf ("%d %s %d %d %d", line_num, cell_type_translation.at(cell->type.str()).c_str(), l1_width, l1, l2);
603 f << stringf("%s\n", str.c_str());
604
605 if(l2_width > ceil(log(l1_width)/log(2)))
606 {
607 int extra_width = l2_width - ceil(log(l1_width)/log(2));
608 l2 = dump_sigspec(&cell->getPort(RTLIL::IdString("\\B")), l2_width);
609 ++line_num;
610 str = stringf ("%d slice %d %d %d %d;6", line_num, extra_width, l2, l2_width-1, l2_width-extra_width);
611 f << stringf("%s\n", str.c_str());
612 ++line_num;
613 str = stringf ("%d one %d", line_num, extra_width);
614 f << stringf("%s\n", str.c_str());
615 int mux = ++line_num;
616 str = stringf ("%d %s %d %d %d", line_num, cell_type_translation.at("$gt").c_str(), 1, line_num-2, line_num-1);
617 f << stringf("%s\n", str.c_str());
618 ++line_num;
619 str = stringf("%d %s %d", line_num, l1_signed && cell->type == "$sshr" ? "ones":"zero", l1_width);
620 f << stringf("%s\n", str.c_str());
621 ++line_num;
622 str = stringf ("%d %s %d %d %d %d", line_num, cell_type_translation.at("$mux").c_str(), l1_width, mux, line_num-1, cell_output);
623 f << stringf("%s\n", str.c_str());
624 cell_output = line_num;
625 }
626
627 if(output_width < l1_width)
628 {
629 ++line_num;
630 str = stringf ("%d slice %d %d %d %d;5", line_num, output_width, cell_output, output_width-1, 0);
631 f << stringf("%s\n", str.c_str());
632 cell_output = line_num;
633 }
634 line_ref[cell->name] = cell_output;
635 }
636 else if(cell->type == "$logic_and" || cell->type == "$logic_or")//no direct translation in btor
637 {
638 log("writing binary cell - %s\n", cstr(cell->type));
639 int output_width = cell->parameters.at(RTLIL::IdString("\\Y_WIDTH")).as_int();
640 log_assert(output_width == 1);
641 int l1 = dump_sigspec(&cell->getPort(RTLIL::IdString("\\A")), output_width);
642 int l2 = dump_sigspec(&cell->getPort(RTLIL::IdString("\\B")), output_width);
643 int l1_width = cell->parameters.at(RTLIL::IdString("\\A_WIDTH")).as_int();
644 int l2_width = cell->parameters.at(RTLIL::IdString("\\B_WIDTH")).as_int();
645 if(l1_width >1)
646 {
647 ++line_num;
648 str = stringf ("%d %s %d %d", line_num, cell_type_translation.at("$reduce_or").c_str(), output_width, l1);
649 f << stringf("%s\n", str.c_str());
650 l1 = line_num;
651 }
652 if(l2_width > 1)
653 {
654 ++line_num;
655 str = stringf ("%d %s %d %d", line_num, cell_type_translation.at("$reduce_or").c_str(), output_width, l2);
656 f << stringf("%s\n", str.c_str());
657 l2 = line_num;
658 }
659 if(cell->type == "$logic_and")
660 {
661 ++line_num;
662 str = stringf ("%d %s %d %d %d", line_num, cell_type_translation.at("$and").c_str(), output_width, l1, l2);
663 }
664 else if(cell->type == "$logic_or")
665 {
666 ++line_num;
667 str = stringf ("%d %s %d %d %d", line_num, cell_type_translation.at("$or").c_str(), output_width, l1, l2);
668 }
669 f << stringf("%s\n", str.c_str());
670 line_ref[cell->name]=line_num;
671 }
672 //multiplexers
673 else if(cell->type == "$mux")
674 {
675 log("writing mux cell\n");
676 int output_width = cell->parameters.at(RTLIL::IdString("\\WIDTH")).as_int();
677 int l1 = dump_sigspec(&cell->getPort(RTLIL::IdString("\\A")), output_width);
678 int l2 = dump_sigspec(&cell->getPort(RTLIL::IdString("\\B")), output_width);
679 int s = dump_sigspec(&cell->getPort(RTLIL::IdString("\\S")), 1);
680 ++line_num;
681 str = stringf ("%d %s %d %d %d %d",
682 line_num, cell_type_translation.at(cell->type.str()).c_str(), output_width, s, l2, l1);
683 //if s is 0 then l1, if s is 1 then l2 //according to the implementation of mux cell
684 f << stringf("%s\n", str.c_str());
685 line_ref[cell->name]=line_num;
686 }
687 else if(cell->type == "$pmux")
688 {
689 log("writing pmux cell\n");
690 int output_width = cell->parameters.at(RTLIL::IdString("\\WIDTH")).as_int();
691 int select_width = cell->parameters.at(RTLIL::IdString("\\S_WIDTH")).as_int();
692 int default_case = dump_sigspec(&cell->getPort(RTLIL::IdString("\\A")), output_width);
693 int cases = dump_sigspec(&cell->getPort(RTLIL::IdString("\\B")), output_width*select_width);
694 int select = dump_sigspec(&cell->getPort(RTLIL::IdString("\\S")), select_width);
695 int *c = new int[select_width];
696
697 for (int i=0; i<select_width; ++i)
698 {
699 ++line_num;
700 str = stringf ("%d slice 1 %d %d %d", line_num, select, i, i);
701 f << stringf("%s\n", str.c_str());
702 c[i] = line_num;
703 ++line_num;
704 str = stringf ("%d slice %d %d %d %d", line_num, output_width, cases, i*output_width+output_width-1,
705 i*output_width);
706 f << stringf("%s\n", str.c_str());
707 }
708
709 ++line_num;
710 str = stringf ("%d cond %d %d %d %d", line_num, output_width, c[select_width-1], c[select_width-1]+1, default_case);
711 f << stringf("%s\n", str.c_str());
712
713 for (int i=select_width-2; i>=0; --i)
714 {
715 ++line_num;
716 str = stringf ("%d cond %d %d %d %d", line_num, output_width, c[i], c[i]+1, line_num-1);
717 f << stringf("%s\n", str.c_str());
718 }
719
720 line_ref[cell->name]=line_num;
721 }
722 //registers
723 else if(cell->type == "$dff" || cell->type == "$adff" || cell->type == "$dffsr")
724 {
725 //TODO: remodelling fo adff cells
726 log("writing cell - %s\n", cstr(cell->type));
727 int output_width = cell->parameters.at(RTLIL::IdString("\\WIDTH")).as_int();
728 log(" - width is %d\n", output_width);
729 int cond = dump_sigspec(&cell->getPort(RTLIL::IdString("\\CLK")), 1);
730 bool polarity = cell->parameters.at(RTLIL::IdString("\\CLK_POLARITY")).as_bool();
731 const RTLIL::SigSpec* cell_output = &cell->getPort(RTLIL::IdString("\\Q"));
732 int value = dump_sigspec(&cell->getPort(RTLIL::IdString("\\D")), output_width);
733 unsigned start_bit = 0;
734 for(unsigned i=0; i<cell_output->chunks().size(); ++i)
735 {
736 output_width = cell_output->chunks().at(i).width;
737 log_assert( output_width == cell_output->chunks().at(i).wire->width);//full reg is given the next value
738 int reg = dump_wire(cell_output->chunks().at(i).wire);//register
739 int slice = value;
740 if(cell_output->chunks().size()>1)
741 {
742 start_bit+=output_width;
743 slice = ++line_num;
744 str = stringf ("%d slice %d %d %d %d;", line_num, output_width, value, start_bit-1,
745 start_bit-output_width);
746 f << stringf("%s\n", str.c_str());
747 }
748 if(cell->type == "$dffsr")
749 {
750 int sync_reset = dump_sigspec(&cell->getPort(RTLIL::IdString("\\CLR")), 1);
751 bool sync_reset_pol = cell->parameters.at(RTLIL::IdString("\\CLR_POLARITY")).as_bool();
752 int sync_reset_value = dump_sigspec(&cell->getPort(RTLIL::IdString("\\SET")),
753 output_width);
754 bool sync_reset_value_pol = cell->parameters.at(RTLIL::IdString("\\SET_POLARITY")).as_bool();
755 ++line_num;
756 str = stringf ("%d %s %d %s%d %s%d %d", line_num, cell_type_translation.at("$mux").c_str(),
757 output_width, sync_reset_pol ? "":"-", sync_reset, sync_reset_value_pol? "":"-",
758 sync_reset_value, slice);
759 f << stringf("%s\n", str.c_str());
760 slice = line_num;
761 }
762 ++line_num;
763 str = stringf ("%d %s %d %s%d %d %d", line_num, cell_type_translation.at("$mux").c_str(),
764 output_width, polarity?"":"-", cond, slice, reg);
765
766 f << stringf("%s\n", str.c_str());
767 int next = line_num;
768 if(cell->type == "$adff")
769 {
770 int async_reset = dump_sigspec(&cell->getPort(RTLIL::IdString("\\ARST")), 1);
771 bool async_reset_pol = cell->parameters.at(RTLIL::IdString("\\ARST_POLARITY")).as_bool();
772 int async_reset_value = dump_const(&cell->parameters.at(RTLIL::IdString("\\ARST_VALUE")),
773 output_width, 0);
774 ++line_num;
775 str = stringf ("%d %s %d %s%d %d %d", line_num, cell_type_translation.at("$mux").c_str(),
776 output_width, async_reset_pol ? "":"-", async_reset, async_reset_value, next);
777 f << stringf("%s\n", str.c_str());
778 }
779 ++line_num;
780 str = stringf ("%d %s %d %d %d", line_num, cell_type_translation.at(cell->type.str()).c_str(),
781 output_width, reg, next);
782 f << stringf("%s\n", str.c_str());
783 }
784 line_ref[cell->name]=line_num;
785 }
786 //memories
787 else if(cell->type == "$memrd")
788 {
789 log("writing memrd cell\n");
790 if (cell->parameters.at("\\CLK_ENABLE").as_bool() == true)
791 log_error("The btor backen does not support $memrd cells with built-in registers. Run memory_dff with -wr_only.\n");
792 str = cell->parameters.at(RTLIL::IdString("\\MEMID")).decode_string();
793 int mem = dump_memory(module->memories.at(RTLIL::IdString(str.c_str())));
794 int address_width = cell->parameters.at(RTLIL::IdString("\\ABITS")).as_int();
795 int address = dump_sigspec(&cell->getPort(RTLIL::IdString("\\ADDR")), address_width);
796 int data_width = cell->parameters.at(RTLIL::IdString("\\WIDTH")).as_int();
797 ++line_num;
798 str = stringf("%d read %d %d %d", line_num, data_width, mem, address);
799 f << stringf("%s\n", str.c_str());
800 line_ref[cell->name]=line_num;
801 }
802 else if(cell->type == "$memwr")
803 {
804 log("writing memwr cell\n");
805 if (cell->parameters.at("\\CLK_ENABLE").as_bool() == false)
806 log_error("The btor backen does not support $memwr cells without built-in registers. Run memory_dff (but with -wr_only).\n");
807 int clk = dump_sigspec(&cell->getPort(RTLIL::IdString("\\CLK")), 1);
808 bool polarity = cell->parameters.at(RTLIL::IdString("\\CLK_POLARITY")).as_bool();
809 int enable = dump_sigspec(&cell->getPort(RTLIL::IdString("\\EN")), 1);
810 int address_width = cell->parameters.at(RTLIL::IdString("\\ABITS")).as_int();
811 int address = dump_sigspec(&cell->getPort(RTLIL::IdString("\\ADDR")), address_width);
812 int data_width = cell->parameters.at(RTLIL::IdString("\\WIDTH")).as_int();
813 int data = dump_sigspec(&cell->getPort(RTLIL::IdString("\\DATA")), data_width);
814 str = cell->parameters.at(RTLIL::IdString("\\MEMID")).decode_string();
815 int mem = dump_memory(module->memories.at(RTLIL::IdString(str.c_str())));
816 //check if the memory has already next
817 /*
818 auto it = mem_next.find(mem);
819 if(it != std::end(mem_next))
820 {
821 ++line_num;
822 str = cell->parameters.at(RTLIL::IdString("\\MEMID")).decode_string();
823 RTLIL::Memory *memory = module->memories.at(RTLIL::IdString(str.c_str()));
824 int address_bits = ceil(log(memory->size)/log(2));
825 str = stringf("%d array %d %d", line_num, memory->width, address_bits);
826 f << stringf("%s\n", str.c_str());
827 ++line_num;
828 str = stringf("%d eq 1 %d %d; mem invar", line_num, mem, line_num - 1);
829 f << stringf("%s\n", str.c_str());
830 mem = line_num - 1;
831 }
832 */
833 ++line_num;
834 if(polarity)
835 str = stringf("%d one 1", line_num);
836 else
837 str = stringf("%d zero 1", line_num);
838 f << stringf("%s\n", str.c_str());
839 ++line_num;
840 str = stringf("%d eq 1 %d %d", line_num, clk, line_num-1);
841 f << stringf("%s\n", str.c_str());
842 ++line_num;
843 str = stringf("%d and 1 %d %d", line_num, line_num-1, enable);
844 f << stringf("%s\n", str.c_str());
845 ++line_num;
846 str = stringf("%d write %d %d %d %d %d", line_num, data_width, address_width, mem, address, data);
847 f << stringf("%s\n", str.c_str());
848 /*
849 ++line_num;
850 str = stringf("%d acond %d %d %d %d %d", line_num, data_width, address_width, line_num-2, line_num-1, mem);
851 f << stringf("%s\n", str.c_str());
852 ++line_num;
853 str = stringf("%d anext %d %d %d %d", line_num, data_width, address_width, mem, line_num-1);
854 f << stringf("%s\n", str.c_str());
855 */
856 mem_next[mem].insert(std::make_pair(line_num-1, line_num));
857 }
858 else if(cell->type == "$slice")
859 {
860 log("writing slice cell\n");
861 const RTLIL::SigSpec* input = &cell->getPort(RTLIL::IdString("\\A"));
862 int input_width = cell->parameters.at(RTLIL::IdString("\\A_WIDTH")).as_int();
863 log_assert(input->size() == input_width);
864 int input_line = dump_sigspec(input, input_width);
865 const RTLIL::SigSpec* output YS_ATTRIBUTE(unused) = &cell->getPort(RTLIL::IdString("\\Y"));
866 int output_width = cell->parameters.at(RTLIL::IdString("\\Y_WIDTH")).as_int();
867 log_assert(output->size() == output_width);
868 int offset = cell->parameters.at(RTLIL::IdString("\\OFFSET")).as_int();
869 ++line_num;
870 str = stringf("%d %s %d %d %d %d", line_num, cell_type_translation.at(cell->type.str()).c_str(), output_width, input_line, output_width+offset-1, offset);
871 f << stringf("%s\n", str.c_str());
872 line_ref[cell->name]=line_num;
873 }
874 else if(cell->type == "$concat")
875 {
876 log("writing concat cell\n");
877 const RTLIL::SigSpec* input_a = &cell->getPort(RTLIL::IdString("\\A"));
878 int input_a_width = cell->parameters.at(RTLIL::IdString("\\A_WIDTH")).as_int();
879 log_assert(input_a->size() == input_a_width);
880 int input_a_line = dump_sigspec(input_a, input_a_width);
881 const RTLIL::SigSpec* input_b = &cell->getPort(RTLIL::IdString("\\B"));
882 int input_b_width = cell->parameters.at(RTLIL::IdString("\\B_WIDTH")).as_int();
883 log_assert(input_b->size() == input_b_width);
884 int input_b_line = dump_sigspec(input_b, input_b_width);
885 ++line_num;
886 str = stringf("%d %s %d %d %d", line_num, cell_type_translation.at(cell->type.str()).c_str(), input_a_width+input_b_width,
887 input_a_line, input_b_line);
888 f << stringf("%s\n", str.c_str());
889 line_ref[cell->name]=line_num;
890 }
891 curr_cell.clear();
892 return line_num;
893 }
894 else
895 {
896 return it->second;
897 }
898 }
899
900 const RTLIL::SigSpec* get_cell_output(RTLIL::Cell* cell)
901 {
902 const RTLIL::SigSpec *output_sig = nullptr;
903 if (cell->type == "$memrd")
904 {
905 output_sig = &cell->getPort(RTLIL::IdString("\\DATA"));
906 }
907 else if(cell->type == "$memwr" || cell->type == "$assert")
908 {
909 //no output
910 }
911 else if(cell->type == "$dff" || cell->type == "$adff" || cell->type == "$dffsr")
912 {
913 output_sig = &cell->getPort(RTLIL::IdString("\\Q"));
914 }
915 else
916 {
917 output_sig = &cell->getPort(RTLIL::IdString("\\Y"));
918 }
919 return output_sig;
920 }
921
922 void dump_property(RTLIL::Wire *wire)
923 {
924 int l = dump_wire(wire);
925 ++line_num;
926 str = stringf("%d root 1 %d", line_num, l);
927 f << stringf("%s\n", str.c_str());
928 }
929
930 void dump()
931 {
932 f << stringf(";module %s\n", cstr(module->name));
933
934 log("creating intermediate wires map\n");
935 //creating map of intermediate wires as output of some cell
936 for (auto it = module->cells_.begin(); it != module->cells_.end(); ++it)
937 {
938 RTLIL::Cell *cell = it->second;
939 const RTLIL::SigSpec* output_sig = get_cell_output(cell);
940 if(output_sig==nullptr)
941 continue;
942 RTLIL::SigSpec s = sigmap(*output_sig);
943 output_sig = &s;
944 log(" - %s\n", cstr(it->second->type));
945 if (cell->type == "$memrd")
946 {
947 for(unsigned i=0; i<output_sig->chunks().size(); ++i)
948 {
949 RTLIL::Wire *w = output_sig->chunks().at(i).wire;
950 RTLIL::IdString wire_id = w->name;
951 inter_wire_map[wire_id].insert(WireInfo(cell->name,&output_sig->chunks().at(i)));
952 }
953 }
954 else if(cell->type == "$memwr")
955 {
956 continue;//nothing to do
957 }
958 else if(cell->type == "$dff" || cell->type == "$adff" || cell->type == "$dffsr")
959 {
960 RTLIL::IdString wire_id = output_sig->chunks().front().wire->name;
961 for(unsigned i=0; i<output_sig->chunks().size(); ++i)
962 {
963 RTLIL::Wire *w = output_sig->chunks().at(i).wire;
964 RTLIL::IdString wire_id = w->name;
965 inter_wire_map[wire_id].insert(WireInfo(cell->name,&output_sig->chunks().at(i)));
966 basic_wires[wire_id] = true;
967 }
968 }
969 else
970 {
971 for(unsigned i=0; i<output_sig->chunks().size(); ++i)
972 {
973 RTLIL::Wire *w = output_sig->chunks().at(i).wire;
974 RTLIL::IdString wire_id = w->name;
975 inter_wire_map[wire_id].insert(WireInfo(cell->name,&output_sig->chunks().at(i)));
976 }
977 }
978 }
979
980 log("writing input\n");
981 std::map<int, RTLIL::Wire*> inputs, outputs;
982 std::vector<RTLIL::Wire*> safety;
983
984 for (auto &wire_it : module->wires_) {
985 RTLIL::Wire *wire = wire_it.second;
986 if (wire->port_input)
987 inputs[wire->port_id] = wire;
988 if (wire->port_output) {
989 outputs[wire->port_id] = wire;
990 if (wire->name.str().find("safety") != std::string::npos )
991 safety.push_back(wire);
992 }
993 }
994
995 f << stringf(";inputs\n");
996 for (auto &it : inputs) {
997 RTLIL::Wire *wire = it.second;
998 dump_wire(wire);
999 }
1000 f << stringf("\n");
1001
1002 log("writing memories\n");
1003 for(auto mem_it = module->memories.begin(); mem_it != module->memories.end(); ++mem_it)
1004 {
1005 dump_memory(mem_it->second);
1006 }
1007
1008 log("writing output wires\n");
1009 for (auto &it : outputs) {
1010 RTLIL::Wire *wire = it.second;
1011 dump_wire(wire);
1012 }
1013
1014 log("writing cells\n");
1015 for(auto cell_it = module->cells_.begin(); cell_it != module->cells_.end(); ++cell_it)
1016 {
1017 dump_cell(cell_it->second);
1018 }
1019
1020 log("writing memory next");
1021 for(auto mem_it = module->memories.begin(); mem_it != module->memories.end(); ++mem_it)
1022 {
1023 dump_memory_next(mem_it->second);
1024 }
1025
1026 for(auto it: safety)
1027 dump_property(it);
1028
1029 f << stringf("\n");
1030
1031 log("writing outputs info\n");
1032 f << stringf(";outputs\n");
1033 for (auto &it : outputs) {
1034 RTLIL::Wire *wire = it.second;
1035 int l = dump_wire(wire);
1036 f << stringf(";%d %s", l, cstr(wire->name));
1037 }
1038 f << stringf("\n");
1039 }
1040
1041 static void dump(std::ostream &f, RTLIL::Module *module, RTLIL::Design *design, BtorDumperConfig &config)
1042 {
1043 BtorDumper dumper(f, module, design, &config);
1044 dumper.dump();
1045 }
1046 };
1047
1048 struct BtorBackend : public Backend {
1049 BtorBackend() : Backend("btor", "write design to BTOR file") { }
1050
1051 virtual void help()
1052 {
1053 // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
1054 log("\n");
1055 log(" write_btor [filename]\n");
1056 log("\n");
1057 log("Write the current design to an BTOR file.\n");
1058 }
1059
1060 virtual void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design)
1061 {
1062 std::string top_module_name;
1063 std::string buf_type, buf_in, buf_out;
1064 std::string true_type, true_out;
1065 std::string false_type, false_out;
1066 BtorDumperConfig config;
1067
1068 log_header("Executing BTOR backend.\n");
1069
1070 size_t argidx=1;
1071 extra_args(f, filename, args, argidx);
1072
1073 if (top_module_name.empty())
1074 for (auto & mod_it:design->modules_)
1075 if (mod_it.second->get_bool_attribute("\\top"))
1076 top_module_name = mod_it.first.str();
1077
1078 *f << stringf("; Generated by %s\n", yosys_version_str);
1079 *f << stringf("; %s developed and maintained by Clifford Wolf <clifford@clifford.at>\n", yosys_version_str);
1080 *f << stringf("; BTOR Backend developed by Ahmed Irfan <irfan@fbk.eu> - Fondazione Bruno Kessler, Trento, Italy\n");
1081 *f << stringf(";;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;\n");
1082
1083 std::vector<RTLIL::Module*> mod_list;
1084
1085 for (auto module_it : design->modules_)
1086 {
1087 RTLIL::Module *module = module_it.second;
1088 if (module->get_bool_attribute("\\blackbox"))
1089 continue;
1090
1091 if (module->processes.size() != 0)
1092 log_error("Found unmapped processes in module %s: unmapped processes are not supported in BTOR backend!\n", RTLIL::id2cstr(module->name));
1093
1094 if (module->name == RTLIL::escape_id(top_module_name)) {
1095 BtorDumper::dump(*f, module, design, config);
1096 top_module_name.clear();
1097 continue;
1098 }
1099
1100 mod_list.push_back(module);
1101 }
1102
1103 if (!top_module_name.empty())
1104 log_error("Can't find top module `%s'!\n", top_module_name.c_str());
1105
1106 for (auto module : mod_list)
1107 BtorDumper::dump(*f, module, design, config);
1108 }
1109 } BtorBackend;
1110
1111 PRIVATE_NAMESPACE_END