2 * yosys -- Yosys Open SYnthesis Suite
4 * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
6 * Permission to use, copy, modify, and/or distribute this software for any
7 * purpose with or without fee is hereby granted, provided that the above
8 * copyright notice and this permission notice appear in all copies.
10 * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
11 * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
12 * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
13 * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
14 * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
15 * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
16 * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
20 #include "kernel/rtlil.h"
21 #include "kernel/register.h"
22 #include "kernel/sigtools.h"
23 #include "kernel/celltypes.h"
24 #include "kernel/log.h"
28 PRIVATE_NAMESPACE_BEGIN
34 RTLIL::Module
*module
;
39 dict
<int, int> sorts_bv
;
41 // (<address-width>, <data-width>) => <sid>
42 dict
<pair
<int, int>, int> sorts_mem
;
44 // SigBit => (<nid>, <bitidx>)
45 dict
<SigBit
, pair
<int, int>> bit_nid
;
48 dict
<int, int> nid_width
;
51 dict
<SigSpec
, int> sig_nid
;
53 // bit to driving cell
54 dict
<SigBit
, Cell
*> bit_cell
;
57 dict
<Const
, int> consts
;
59 // ff inputs that need to be evaluated (<nid>, <d>)
60 vector
<pair
<int, SigSpec
>> ff_todo
;
62 pool
<Cell
*> cell_recursion_guard
;
64 int get_bv_sid(int width
)
66 if (sorts_bv
.count(width
) == 0) {
68 f
<< stringf("%d sort bitvec %d\n", nid
, width
);
69 sorts_bv
[width
] = nid
;
71 return sorts_bv
.at(width
);
74 void add_nid_sig(int nid
, const SigSpec
&sig
)
76 for (int i
= 0; i
< GetSize(sig
); i
++)
77 bit_nid
[sig
[i
]] = make_pair(nid
, i
);
80 nid_width
[nid
] = GetSize(sig
);
83 void export_cell(Cell
*cell
)
85 log_assert(cell_recursion_guard
.count(cell
) == 0);
86 cell_recursion_guard
.insert(cell
);
88 if (cell
->type
.in("$add", "$sub", "$xor"))
91 if (cell
->type
== "$add") btor_op
= "add";
92 if (cell
->type
== "$sub") btor_op
= "sub";
93 if (cell
->type
== "$xor") btor_op
= "xor";
94 log_assert(!btor_op
.empty());
96 int width
= GetSize(cell
->getPort("\\Y"));
97 width
= std::max(width
, GetSize(cell
->getPort("\\A")));
98 width
= std::max(width
, GetSize(cell
->getPort("\\B")));
100 bool a_signed
= cell
->hasParam("\\A_SIGNED") ? cell
->getParam("\\A_SIGNED").as_bool() : false;
101 bool b_signed
= cell
->hasParam("\\B_SIGNED") ? cell
->getParam("\\B_SIGNED").as_bool() : false;
103 int sid
= get_bv_sid(width
);
104 int nid_a
= get_sig_nid(cell
->getPort("\\A"), width
, a_signed
);
105 int nid_b
= get_sig_nid(cell
->getPort("\\B"), width
, b_signed
);
107 int nid
= next_nid
++;
108 f
<< stringf("%d %s %d %d %d ; %s\n", nid
, btor_op
.c_str(), sid
, nid_a
, nid_b
, log_id(cell
));
110 SigSpec sig
= sigmap(cell
->getPort("\\Y"));
112 if (GetSize(sig
) < width
) {
113 int sid
= get_bv_sid(GetSize(sig
));
114 int nid2
= next_nid
++;
115 f
<< stringf("%d slice %d %d %d 0 ; %s\n", nid2
, sid
, nid
, GetSize(sig
)-1, log_id(cell
));
119 add_nid_sig(nid
, sig
);
123 if (cell
->type
.in("$mux", "$_MUX_"))
125 SigSpec sig_a
= sigmap(cell
->getPort("\\A"));
126 SigSpec sig_b
= sigmap(cell
->getPort("\\B"));
127 SigSpec sig_s
= sigmap(cell
->getPort("\\S"));
128 SigSpec sig_y
= sigmap(cell
->getPort("\\Y"));
130 int nid_a
= get_sig_nid(sig_a
);
131 int nid_b
= get_sig_nid(sig_b
);
132 int nid_s
= get_sig_nid(sig_s
);
134 int sid
= get_bv_sid(GetSize(sig_y
));
135 int nid
= next_nid
++;
136 f
<< stringf("%d ite %d %d %d %d ; %s\n", nid
, sid
, nid_s
, nid_b
, nid_a
, log_id(cell
));
138 add_nid_sig(nid
, sig_y
);
142 if (cell
->type
.in("$dff", "$ff", "$_DFF_P_", "$_DFF_N", "$_FF_"))
144 SigSpec sig_d
= sigmap(cell
->getPort("\\D"));
145 SigSpec sig_q
= sigmap(cell
->getPort("\\Q"));
147 string symbol
= log_signal(sig_q
);
148 if (symbol
.find(' ') != string::npos
)
149 symbol
= log_id(cell
);
151 if (symbol
[0] == '\\')
152 symbol
= symbol
.substr(1);
154 int sid
= get_bv_sid(GetSize(sig_q
));
155 int nid
= next_nid
++;
156 f
<< stringf("%d state %d %s ; %s\n", nid
, sid
, symbol
.c_str(), log_id(cell
));
158 ff_todo
.push_back(make_pair(nid
, sig_d
));
159 add_nid_sig(nid
, sig_q
);
163 log_error("Unsupported cell type: %s (%s)\n", log_id(cell
->type
), log_id(cell
));
166 cell_recursion_guard
.erase(cell
);
169 int get_sig_nid(SigSpec sig
, int to_width
= -1, bool is_signed
= false)
173 if (sig_nid
.count(sig
) == 0)
176 vector
<pair
<int, int>> nidbits
;
179 for (int i
= 0; i
< GetSize(sig
); i
++)
183 if (bit_nid
.count(bit
) == 0)
185 if (bit
.wire
== nullptr)
189 while (i
+GetSize(c
) < GetSize(sig
) && sig
[i
+GetSize(c
)].wire
== nullptr)
190 c
.bits
.push_back(sig
[i
+GetSize(c
)].data
);
192 if (consts
.count(c
) == 0) {
193 int sid
= get_bv_sid(GetSize(c
));
194 int nid
= next_nid
++;
195 f
<< stringf("%d const %d %s\n", nid
, sid
, c
.as_string().c_str());
197 nid_width
[nid
] = GetSize(c
);
200 int nid
= consts
.at(c
);
202 for (int j
= 0; j
< GetSize(c
); j
++)
203 nidbits
.push_back(make_pair(nid
, j
));
210 export_cell(bit_cell
.at(bit
));
211 log_assert(bit_nid
.count(bit
));
215 nidbits
.push_back(bit_nid
.at(bit
));
221 // group bits and emit slice-concat chain
222 for (int i
= 0; i
< GetSize(nidbits
); i
++)
224 int nid2
= nidbits
[i
].first
;
225 int lower
= nidbits
[i
].second
;
228 while (i
+1 < GetSize(nidbits
) && nidbits
[i
+1].first
== nidbits
[i
].first
&&
229 nidbits
[i
+1].second
== nidbits
[i
].second
+1)
234 if (lower
!= 0 || upper
+1 != nid_width
.at(nid2
)) {
235 int sid
= get_bv_sid(upper
-lower
+1);
237 f
<< stringf("%d slice %d %d %d %d\n", nid3
, sid
, nid
, upper
, lower
);
243 int sid
= get_bv_sid(width
+upper
-lower
+1);
244 int nid4
= next_nid
++;
245 f
<< stringf("%d concat %d %d %d\n", nid4
, sid
, nid
, nid3
);
248 width
+= upper
-lower
+1;
253 nid_width
[nid
] = width
;
256 int nid
= sig_nid
.at(sig
);
258 if (to_width
>= 0 && to_width
!= GetSize(sig
))
260 if (to_width
< GetSize(sig
))
262 int sid
= get_bv_sid(to_width
);
263 int nid2
= next_nid
++;
264 f
<< stringf("%d slice %d %d %d 0\n", nid2
, sid
, nid
, to_width
-1);
269 int sid
= get_bv_sid(to_width
);
270 int nid2
= next_nid
++;
271 f
<< stringf("%d %s %d %d %d\n", nid2
, is_signed
? "sext" : "uext",
272 sid
, nid
, to_width
- GetSize(sig
));
280 BtorWorker(std::ostream
&f
, RTLIL::Module
*module
, bool verbose
) :
281 f(f
), sigmap(module
), module(module
), verbose(verbose
), next_nid(1)
283 for (auto wire
: module
->wires())
285 if (!wire
->port_id
|| !wire
->port_input
)
288 SigSpec sig
= sigmap(wire
);
289 int sid
= get_bv_sid(GetSize(sig
));
290 int nid
= next_nid
++;
292 f
<< stringf("%d input %d %s\n", nid
, sid
, log_id(wire
));
293 add_nid_sig(nid
, sig
);
296 for (auto cell
: module
->cells())
297 for (auto &conn
: cell
->connections())
299 if (!cell
->output(conn
.first
))
302 for (auto bit
: sigmap(conn
.second
))
303 bit_cell
[bit
] = cell
;
306 for (auto wire
: module
->wires())
308 if (!wire
->port_id
|| !wire
->port_output
)
311 int nid
= get_sig_nid(wire
);
312 f
<< stringf("%d output %d %s\n", next_nid
++, nid
, log_id(wire
));
315 while (!ff_todo
.empty())
317 vector
<pair
<int, SigSpec
>> todo
;
320 for (auto &it
: todo
)
322 int nid
= get_sig_nid(it
.second
);
323 int sid
= get_bv_sid(GetSize(it
.second
));
324 f
<< stringf("%d next %d %d %d\n", next_nid
++, sid
, it
.first
, nid
);
330 struct BtorBackend
: public Backend
{
331 BtorBackend() : Backend("btor", "write design to BTOR file") { }
334 // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
336 log(" write_btor [options] [filename]\n");
338 log("Write a BTOR description of the current design.\n");
341 virtual void execute(std::ostream
*&f
, std::string filename
, std::vector
<std::string
> args
, RTLIL::Design
*design
)
343 bool verbose
= false;
345 log_header(design
, "Executing BTOR backend.\n");
348 for (argidx
= 1; argidx
< args
.size(); argidx
++)
350 // if (args[argidx] == "-verbose") {
356 extra_args(f
, filename
, args
, argidx
);
358 RTLIL::Module
*topmod
= design
->top_module();
360 if (topmod
== nullptr)
361 log_cmd_error("No top module found.\n");
363 *f
<< stringf("; BTOR description generated by %s for module %s.\n",
364 yosys_version_str
, log_id(topmod
));
366 BtorWorker(*f
, topmod
, verbose
);
368 *f
<< stringf("; end of yosys output\n");
372 PRIVATE_NAMESPACE_END