2 * yosys -- Yosys Open SYnthesis Suite
4 * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
5 * Copyright (C) 2014 Ahmed Irfan <irfan@fbk.eu>
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.
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.
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
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"
34 PRIVATE_NAMESPACE_BEGIN
36 struct BtorDumperConfig
42 std::string buf_type
, buf_in
, buf_out
;
43 std::string true_type
, true_out
, false_type
, false_out
;
45 BtorDumperConfig() : subckt_mode(false), conn_mode(false), impltf_mode(false) { }
50 RTLIL::IdString cell_name
;
51 const RTLIL::SigChunk
*chunk
;
53 WireInfo(RTLIL::IdString c
, const RTLIL::SigChunk
* ch
) : cell_name(c
), chunk(ch
) { }
58 bool operator() (const WireInfo
& x
, const WireInfo
& y
)
60 return x
.chunk
< y
.chunk
;
67 RTLIL::Module
*module
;
68 RTLIL::Design
*design
;
69 BtorDumperConfig
*config
;
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
)
87 for(auto it
=module
->wires_
.begin(); it
!=module
->wires_
.end(); ++it
)
89 if(it
->second
->port_input
)
91 basic_wires
[it
->first
]=true;
95 basic_wires
[it
->first
]=false;
97 inter_wire_map
[it
->first
].clear();
101 cell_type_translation
["$assert"] = "root";
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";
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";
134 cell_type_translation
["$mux"] = "cond";
136 cell_type_translation
["$dff"] = "next";
137 cell_type_translation
["$adff"] = "next";
138 cell_type_translation
["$dffsr"] = "next";
142 cell_type_translation
["$slice"] = "slice";
144 cell_type_translation
["$concat"] = "concat";
146 //signed cell type translation
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";
158 std::vector
<std::string
> cstr_buf
;
160 const char *cstr(const RTLIL::IdString id
)
162 str
= RTLIL::unescape_id(id
);
163 for (size_t i
= 0; i
< str
.size(); ++i
)
164 if (str
[i
] == '#' || str
[i
] == '=')
166 cstr_buf
.push_back(str
);
167 return cstr_buf
.back().c_str();
170 int dump_wire(RTLIL::Wire
* wire
)
172 if(basic_wires
[wire
->name
])
174 log("writing wire %s\n", cstr(wire
->name
));
175 auto it
= line_ref
.find(wire
->name
);
176 if(it
==std::end(line_ref
))
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());
184 else return it
->second
;
186 else // case when the wire is not basic wire
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
))
192 std::set
<WireInfo
, WireInfoOrder
>& dep_set
= inter_wire_map
.at(wire
->name
);
195 for(auto dep_set_it
=dep_set
.begin(); dep_set_it
!=dep_set
.end(); ++dep_set_it
)
197 RTLIL::IdString cell_id
= dep_set_it
->cell_name
;
198 if(cell_id
== curr_cell
)
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
);
205 if(dep_set
.size()==1 && wire
->width
== cell_output
->size())
207 wire_line
= cell_line
;
212 int prev_wire_line
=0; //previously dumped wire line
214 for(unsigned j
=0; j
<cell_output
->chunks().size(); ++j
)
216 start_bit
+=cell_output
->chunks().at(j
).width
;
217 if(cell_output
->chunks().at(j
).wire
->name
== wire
->name
)
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)
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
;
236 if(dep_set
.size()==0)
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
;
243 line_ref
[wire
->name
]=wire_line
;
248 log(" -- already processed wire\n");
256 int dump_memory(const RTLIL::Memory
* memory
)
258 log("writing memory %s\n", cstr(memory
->name
));
259 auto it
= line_ref
.find(memory
->name
);
260 if(it
==std::end(line_ref
))
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());
269 else return it
->second
;
272 int dump_memory_next(const RTLIL::Memory
* memory
)
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
))
278 log("can not write next of a memory that is not dumped yet\n");
283 auto acond_list_it
= mem_next
.find(mem_it
->second
);
284 if(acond_list_it
!=std::end(mem_next
))
286 std::set
<std::pair
<int,int>>& cond_list
= acond_list_it
->second
;
287 if(cond_list
.empty())
291 auto it
=cond_list
.begin();
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());
296 for(; it
!=cond_list
.end(); ++it
)
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());
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());
311 int dump_const(const RTLIL::Const
* data
, int width
, int offset
)
313 log("writing const \n");
314 if((data
->flags
& RTLIL::CONST_FLAG_STRING
) == 0)
317 width
= data
->bits
.size() - offset
;
319 std::string data_str
= data
->as_string();
321 data_str
= data_str
.substr(offset
, width
);
324 str
= stringf("%d const %d %s", line_num
, width
, data_str
.c_str());
325 f
<< stringf("%s\n", str
.c_str());
329 log("writing const error\n");
334 int dump_sigchunk(const RTLIL::SigChunk
* chunk
)
336 log("writing sigchunk\n");
338 if(chunk
->wire
== NULL
)
340 RTLIL::Const
data_const(chunk
->data
);
341 l
=dump_const(&data_const
, chunk
->width
, chunk
->offset
);
345 if (chunk
->width
== chunk
->wire
->width
&& chunk
->offset
== 0)
346 l
= dump_wire(chunk
->wire
);
349 int wire_line_num
= dump_wire(chunk
->wire
);
350 log_assert(wire_line_num
>0);
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());
361 int dump_sigspec(const RTLIL::SigSpec
* sig
, int expected_width
)
363 log("writing sigspec\n");
364 RTLIL::SigSpec s
= sigmap(*sig
);
366 auto it
= sig_ref
.find(s
);
367 if(it
== std::end(sig_ref
))
371 l
= dump_sigchunk(&s
.chunks().front());
376 l1
= dump_sigchunk(&s
.chunks().front());
378 w1
= s
.chunks().front().width
;
379 for (unsigned i
=1; i
< s
.chunks().size(); ++i
)
381 l2
= dump_sigchunk(&s
.chunks().at(i
));
383 w2
= s
.chunks().at(i
).width
;
385 str
= stringf("%d concat %d %d %d", line_num
, w1
+w2
, l2
, l1
);
386 f
<< stringf("%s\n", str
.c_str());
399 if (expected_width
!= s
.size())
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())
405 //TODO: case the signal is signed
407 str
= stringf ("%d zero %d", line_num
, expected_width
- s
.size());
408 f
<< stringf("%s\n", str
.c_str());
410 str
= stringf ("%d concat %d %d %d", line_num
, expected_width
, line_num
-1, l
);
411 f
<< stringf("%s\n", str
.c_str());
414 else if(expected_width
< s
.size())
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());
426 int dump_cell(const RTLIL::Cell
* cell
)
428 auto it
= line_ref
.find(cell
->name
);
429 if(it
==std::end(line_ref
))
431 curr_cell
= cell
->name
;
433 if(cell
->type
== "$assert")
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());
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());
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
;
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")
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
);
471 if(cell
->type
!= "$pos")
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());
478 if(output_width
< w
&& (cell
->type
== "$not" || cell
->type
== "$neg" || cell
->type
== "$pos"))
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
;
485 line_ref
[cell
->name
]=cell_line
;
487 else if(cell
->type
== "$reduce_xnor" || cell
->type
== "$logic_not")//no direct translation in btor
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)
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());
500 else if(cell
->type
== "$reduce_xnor")
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());
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
;
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" )
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();
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
;
530 int l1
= dump_sigspec(&cell
->getPort(RTLIL::IdString("\\A")), l1_width
);
531 int l2
= dump_sigspec(&cell
->getPort(RTLIL::IdString("\\B")), l2_width
);
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")
540 op
= s_cell_type_translation
.at(cell
->type
.str());
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());
546 line_ref
[cell
->name
]=line_num
;
548 else if(cell
->type
== "$add" || cell
->type
== "$sub" || cell
->type
== "$mul" || cell
->type
== "$div" ||
549 cell
->type
== "$mod" )
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();
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
;
564 int l1
= dump_sigspec(&cell
->getPort(RTLIL::IdString("\\A")), l1_width
);
565 int l2
= dump_sigspec(&cell
->getPort(RTLIL::IdString("\\B")), l2_width
);
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")
574 op
= s_cell_type_translation
.at("$modx");
576 op
= s_cell_type_translation
.at("$mody");
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());
581 if(output_width
< l1_width
)
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());
587 line_ref
[cell
->name
]=line_num
;
589 else if(cell
->type
== "$shr" || cell
->type
== "$shl" || cell
->type
== "$sshr" || cell
->type
== "$sshl" || cell
->type
== "$shift" || cell
->type
== "$shiftx")
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());
605 if(l2_width
> ceil(log(l1_width
)/log(2)))
607 int extra_width
= l2_width
- ceil(log(l1_width
)/log(2));
608 l2
= dump_sigspec(&cell
->getPort(RTLIL::IdString("\\B")), l2_width
);
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());
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());
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());
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
;
627 if(output_width
< l1_width
)
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
;
634 line_ref
[cell
->name
] = cell_output
;
636 else if(cell
->type
== "$logic_and" || cell
->type
== "$logic_or")//no direct translation in btor
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();
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());
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());
659 if(cell
->type
== "$logic_and")
662 str
= stringf ("%d %s %d %d %d", line_num
, cell_type_translation
.at("$and").c_str(), output_width
, l1
, l2
);
664 else if(cell
->type
== "$logic_or")
667 str
= stringf ("%d %s %d %d %d", line_num
, cell_type_translation
.at("$or").c_str(), output_width
, l1
, l2
);
669 f
<< stringf("%s\n", str
.c_str());
670 line_ref
[cell
->name
]=line_num
;
673 else if(cell
->type
== "$mux")
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);
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
;
687 else if(cell
->type
== "$pmux")
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
];
697 for (int i
=0; i
<select_width
; ++i
)
700 str
= stringf ("%d slice 1 %d %d %d", line_num
, select
, i
, i
);
701 f
<< stringf("%s\n", str
.c_str());
704 str
= stringf ("%d slice %d %d %d %d", line_num
, output_width
, cases
, i
*output_width
+output_width
-1,
706 f
<< stringf("%s\n", str
.c_str());
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());
713 for (int i
=select_width
-2; i
>=0; --i
)
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());
720 line_ref
[cell
->name
]=line_num
;
723 else if(cell
->type
== "$dff" || cell
->type
== "$adff" || cell
->type
== "$dffsr")
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
)
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
740 if(cell_output
->chunks().size()>1)
742 start_bit
+=output_width
;
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());
748 if(cell
->type
== "$dffsr")
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")),
754 bool sync_reset_value_pol
= cell
->parameters
.at(RTLIL::IdString("\\SET_POLARITY")).as_bool();
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());
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
);
766 f
<< stringf("%s\n", str
.c_str());
768 if(cell
->type
== "$adff")
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")),
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());
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());
784 line_ref
[cell
->name
]=line_num
;
787 else if(cell
->type
== "$memrd")
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();
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
;
802 else if(cell
->type
== "$memwr")
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
818 auto it = mem_next.find(mem);
819 if(it != std::end(mem_next))
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());
828 str = stringf("%d eq 1 %d %d; mem invar", line_num, mem, line_num - 1);
829 f << stringf("%s\n", str.c_str());
835 str
= stringf("%d one 1", line_num
);
837 str
= stringf("%d zero 1", line_num
);
838 f
<< stringf("%s\n", str
.c_str());
840 str
= stringf("%d eq 1 %d %d", line_num
, clk
, line_num
-1);
841 f
<< stringf("%s\n", str
.c_str());
843 str
= stringf("%d and 1 %d %d", line_num
, line_num
-1, enable
);
844 f
<< stringf("%s\n", str
.c_str());
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());
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());
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());
856 mem_next
[mem
].insert(std::make_pair(line_num
-1, line_num
));
858 else if(cell
->type
== "$slice")
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();
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
;
874 else if(cell
->type
== "$concat")
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
);
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
;
900 const RTLIL::SigSpec
* get_cell_output(RTLIL::Cell
* cell
)
902 const RTLIL::SigSpec
*output_sig
= nullptr;
903 if (cell
->type
== "$memrd")
905 output_sig
= &cell
->getPort(RTLIL::IdString("\\DATA"));
907 else if(cell
->type
== "$memwr" || cell
->type
== "$assert")
911 else if(cell
->type
== "$dff" || cell
->type
== "$adff" || cell
->type
== "$dffsr")
913 output_sig
= &cell
->getPort(RTLIL::IdString("\\Q"));
917 output_sig
= &cell
->getPort(RTLIL::IdString("\\Y"));
922 void dump_property(RTLIL::Wire
*wire
)
924 int l
= dump_wire(wire
);
926 str
= stringf("%d root 1 %d", line_num
, l
);
927 f
<< stringf("%s\n", str
.c_str());
932 f
<< stringf(";module %s\n", cstr(module
->name
));
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
)
938 RTLIL::Cell
*cell
= it
->second
;
939 const RTLIL::SigSpec
* output_sig
= get_cell_output(cell
);
940 if(output_sig
==nullptr)
942 RTLIL::SigSpec s
= sigmap(*output_sig
);
944 log(" - %s\n", cstr(it
->second
->type
));
945 if (cell
->type
== "$memrd")
947 for(unsigned i
=0; i
<output_sig
->chunks().size(); ++i
)
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
)));
954 else if(cell
->type
== "$memwr")
956 continue;//nothing to do
958 else if(cell
->type
== "$dff" || cell
->type
== "$adff" || cell
->type
== "$dffsr")
960 RTLIL::IdString wire_id
= output_sig
->chunks().front().wire
->name
;
961 for(unsigned i
=0; i
<output_sig
->chunks().size(); ++i
)
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;
971 for(unsigned i
=0; i
<output_sig
->chunks().size(); ++i
)
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
)));
980 log("writing input\n");
981 std::map
<int, RTLIL::Wire
*> inputs
, outputs
;
982 std::vector
<RTLIL::Wire
*> safety
;
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
);
995 f
<< stringf(";inputs\n");
996 for (auto &it
: inputs
) {
997 RTLIL::Wire
*wire
= it
.second
;
1002 log("writing memories\n");
1003 for(auto mem_it
= module
->memories
.begin(); mem_it
!= module
->memories
.end(); ++mem_it
)
1005 dump_memory(mem_it
->second
);
1008 log("writing output wires\n");
1009 for (auto &it
: outputs
) {
1010 RTLIL::Wire
*wire
= it
.second
;
1014 log("writing cells\n");
1015 for(auto cell_it
= module
->cells_
.begin(); cell_it
!= module
->cells_
.end(); ++cell_it
)
1017 dump_cell(cell_it
->second
);
1020 log("writing memory next");
1021 for(auto mem_it
= module
->memories
.begin(); mem_it
!= module
->memories
.end(); ++mem_it
)
1023 dump_memory_next(mem_it
->second
);
1026 for(auto it
: safety
)
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
));
1041 static void dump(std::ostream
&f
, RTLIL::Module
*module
, RTLIL::Design
*design
, BtorDumperConfig
&config
)
1043 BtorDumper
dumper(f
, module
, design
, &config
);
1048 struct BtorBackend
: public Backend
{
1049 BtorBackend() : Backend("btor", "write design to BTOR file") { }
1053 // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
1055 log(" write_btor [filename]\n");
1057 log("Write the current design to an BTOR file.\n");
1060 virtual void execute(std::ostream
*&f
, std::string filename
, std::vector
<std::string
> args
, RTLIL::Design
*design
)
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
;
1068 log_header("Executing BTOR backend.\n");
1071 extra_args(f
, filename
, args
, argidx
);
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();
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");
1083 std::vector
<RTLIL::Module
*> mod_list
;
1085 for (auto module_it
: design
->modules_
)
1087 RTLIL::Module
*module
= module_it
.second
;
1088 if (module
->get_bool_attribute("\\blackbox"))
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
));
1094 if (module
->name
== RTLIL::escape_id(top_module_name
)) {
1095 BtorDumper::dump(*f
, module
, design
, config
);
1096 top_module_name
.clear();
1100 mod_list
.push_back(module
);
1103 if (!top_module_name
.empty())
1104 log_error("Can't find top module `%s'!\n", top_module_name
.c_str());
1106 for (auto module
: mod_list
)
1107 BtorDumper::dump(*f
, module
, design
, config
);
1111 PRIVATE_NAMESPACE_END