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
;
56 int get_bv_sid(int width
)
58 if (sorts_bv
.count(width
) == 0) {
60 f
<< stringf("%d sort bitvec %d\n", nid
, width
);
61 sorts_bv
[width
] = nid
;
63 return sorts_bv
.at(width
);
66 int get_sig_nid(SigSpec sig
)
70 if (sig_nid
.count(sig
) == 0)
73 vector
<pair
<int, int>> nidbits
;
76 for (int i
= 0; i
< GetSize(sig
); i
++)
80 if (bit_nid
.count(bit
) == 0)
86 nidbits
.push_back(bit_nid
.at(bit
));
92 // group bits and emit slice-concat chain
93 for (int i
= 0; i
< GetSize(nidbits
); i
++)
95 int nid2
= nidbits
[i
].first
;
96 int lower
= nidbits
[i
].second
;
99 while (i
+1 < GetSize(nidbits
) && nidbits
[i
+1].first
== nidbits
[i
].first
&&
100 nidbits
[i
+1].second
== nidbits
[i
].second
+1)
105 if (lower
!= 0 && upper
+1 != nid_width
.at(nid2
)) {
106 int sid
= get_bv_sid(upper
-lower
+1);
108 f
<< stringf("%d slice %d %d %d %d\n", nid3
, sid
, nid
, upper
, lower
);
114 int sid
= get_bv_sid(width
+upper
-lower
+1);
115 int nid4
= next_nid
++;
116 f
<< stringf("%d concat %d %d %d\n", nid4
, sid
, nid
, nid3
);
119 width
+= upper
-lower
+1;
124 nid_width
[nid
] = width
;
127 return sig_nid
.at(sig
);
130 BtorWorker(std::ostream
&f
, RTLIL::Module
*module
, bool verbose
) :
131 f(f
), sigmap(module
), module(module
), verbose(verbose
), next_nid(1)
133 for (auto wire
: module
->wires())
135 if (!wire
->port_id
|| !wire
->port_input
)
138 SigSpec sig
= sigmap(wire
);
139 int sid
= get_bv_sid(GetSize(sig
));
140 int nid
= next_nid
++;
142 f
<< stringf("%d input %d %s\n", nid
, sid
, log_id(wire
));
144 for (int i
= 0; i
< GetSize(sig
); i
++)
145 bit_nid
[sig
[i
]] = make_pair(nid
, i
);
147 nid_width
[nid
] = GetSize(sig
);
150 for (auto cell
: module
->cells())
151 for (auto &conn
: cell
->connections())
153 if (!cell
->output(conn
.first
))
156 for (auto bit
: sigmap(conn
.second
))
157 bit_cell
[bit
] = cell
;
160 for (auto wire
: module
->wires())
162 if (!wire
->port_id
|| !wire
->port_output
)
165 int nid
= get_sig_nid(wire
);
166 f
<< stringf("%d output %d %s\n", next_nid
++, nid
, log_id(wire
));
171 struct BtorBackend
: public Backend
{
172 BtorBackend() : Backend("btor", "write design to BTOR file") { }
175 // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
177 log(" write_btor [options] [filename]\n");
179 log("Write a BTOR description of the current design.\n");
182 virtual void execute(std::ostream
*&f
, std::string filename
, std::vector
<std::string
> args
, RTLIL::Design
*design
)
184 bool verbose
= false;
186 log_header(design
, "Executing BTOR backend.\n");
189 for (argidx
= 1; argidx
< args
.size(); argidx
++)
191 if (args
[argidx
] == "-verbose") {
197 extra_args(f
, filename
, args
, argidx
);
199 RTLIL::Module
*topmod
= design
->top_module();
201 if (topmod
== nullptr)
202 log_cmd_error("No top module found.\n");
204 *f
<< stringf("; BTOR description generated by %s for module %s.\n",
205 yosys_version_str
, log_id(topmod
));
207 BtorWorker(*f
, topmod
, verbose
);
209 *f
<< stringf("; end of yosys output\n");
213 PRIVATE_NAMESPACE_END