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.
23 #include "kernel/rtlil.h"
24 #include "kernel/sigtools.h"
25 #include "kernel/celltypes.h"
27 #ifdef YOSYS_ENABLE_MINISAT
28 # include "libs/ezsat/ezminisat.h"
29 typedef ezMiniSAT ezDefaultSAT
;
31 # include "libs/ezsat/ezsat.h"
32 typedef ezSAT ezDefaultSAT
;
38 RTLIL::Design
*design
;
42 SatGen(ezSAT
*ez
, RTLIL::Design
*design
, SigMap
*sigmap
, std::string prefix
= std::string()) :
43 ez(ez
), design(design
), sigmap(sigmap
), prefix(prefix
)
47 void setContext(RTLIL::Design
*design
, SigMap
*sigmap
, std::string prefix
= std::string())
49 this->design
= design
;
50 this->sigmap
= sigmap
;
51 this->prefix
= prefix
;
58 virtual std::vector
<int> importSigSpec(RTLIL::SigSpec
&sig
)
60 RTLIL::SigSpec s
= sig
;
65 vec
.reserve(s
.chunks
.size());
67 for (auto &c
: s
.chunks
)
69 vec
.push_back(c
.data
.as_bool() ? ez
->TRUE
: ez
->FALSE
);
71 vec
.push_back(ez
->literal(prefix
+ stringf(c
.wire
->width
== 1 ?
72 "%s" : "%s [%d]", RTLIL::id2cstr(c
.wire
->name
), c
.offset
)));
76 void extendSignalWidth(std::vector
<int> &vec_a
, std::vector
<int> &vec_b
, RTLIL::Cell
*cell
)
78 bool is_signed_a
= false, is_signed_b
= false;
79 if (cell
->parameters
.count("\\A_SIGNED") > 0)
80 is_signed_a
= cell
->parameters
["\\A_SIGNED"].as_bool();
81 if (cell
->parameters
.count("\\B_SIGNED") > 0)
82 is_signed_b
= cell
->parameters
["\\B_SIGNED"].as_bool();
83 while (vec_a
.size() < vec_b
.size())
84 vec_a
.push_back(is_signed_a
&& vec_a
.size() > 0 ? vec_a
.back() : ez
->FALSE
);
85 while (vec_b
.size() < vec_a
.size())
86 vec_b
.push_back(is_signed_b
&& vec_b
.size() > 0 ? vec_b
.back() : ez
->FALSE
);
89 void extendSignalWidth(std::vector
<int> &vec_a
, std::vector
<int> &vec_b
, std::vector
<int> &vec_y
, RTLIL::Cell
*cell
)
91 extendSignalWidth(vec_a
, vec_b
, cell
);
92 while (vec_y
.size() < vec_a
.size())
93 vec_y
.push_back(ez
->literal());
96 virtual bool importCell(RTLIL::Cell
*cell
)
98 if (cell
->type
== "$_AND_" || cell
->type
== "$_OR_" || cell
->type
== "$_XOR_" ||
99 cell
->type
== "$and" || cell
->type
== "$or" || cell
->type
== "$xor" || cell
->type
== "$xnor" ||
100 cell
->type
== "$add" || cell
->type
== "$sub") {
101 std::vector
<int> a
= importSigSpec(cell
->connections
.at("\\A"));
102 std::vector
<int> b
= importSigSpec(cell
->connections
.at("\\B"));
103 std::vector
<int> y
= importSigSpec(cell
->connections
.at("\\Y"));
104 extendSignalWidth(a
, b
, y
, cell
);
105 if (cell
->type
== "$and" || cell
->type
== "$_AND_")
106 ez
->assume(ez
->vec_eq(ez
->vec_and(a
, b
), y
));
107 if (cell
->type
== "$or" || cell
->type
== "$_OR_")
108 ez
->assume(ez
->vec_eq(ez
->vec_or(a
, b
), y
));
109 if (cell
->type
== "$xor" || cell
->type
== "$_XOR")
110 ez
->assume(ez
->vec_eq(ez
->vec_xor(a
, b
), y
));
111 if (cell
->type
== "$xnor")
112 ez
->assume(ez
->vec_eq(ez
->vec_not(ez
->vec_xor(a
, b
)), y
));
113 if (cell
->type
== "$add")
114 ez
->assume(ez
->vec_eq(ez
->vec_add(a
, b
), y
));
115 if (cell
->type
== "$sub")
116 ez
->assume(ez
->vec_eq(ez
->vec_sub(a
, b
), y
));
120 if (cell
->type
== "$_INV_" || cell
->type
== "$not") {
121 std::vector
<int> a
= importSigSpec(cell
->connections
.at("\\A"));
122 std::vector
<int> y
= importSigSpec(cell
->connections
.at("\\Y"));
123 ez
->assume(ez
->vec_eq(ez
->vec_not(a
), y
));
127 if (cell
->type
== "$_MUX_" || cell
->type
== "$mux") {
128 std::vector
<int> a
= importSigSpec(cell
->connections
.at("\\A"));
129 std::vector
<int> b
= importSigSpec(cell
->connections
.at("\\B"));
130 std::vector
<int> s
= importSigSpec(cell
->connections
.at("\\S"));
131 std::vector
<int> y
= importSigSpec(cell
->connections
.at("\\Y"));
132 ez
->assume(ez
->vec_eq(ez
->vec_ite(s
.at(0), b
, a
), y
));
136 if (cell
->type
== "$pmux" || cell
->type
== "$safe_pmux") {
137 std::vector
<int> a
= importSigSpec(cell
->connections
.at("\\A"));
138 std::vector
<int> b
= importSigSpec(cell
->connections
.at("\\B"));
139 std::vector
<int> s
= importSigSpec(cell
->connections
.at("\\S"));
140 std::vector
<int> y
= importSigSpec(cell
->connections
.at("\\Y"));
141 std::vector
<int> tmp
= a
;
142 for (size_t i
= 0; i
< s
.size(); i
++) {
143 std::vector
<int> part_of_b(b
.begin()+i
*a
.size(), b
.begin()+(i
+1)*a
.size());
144 tmp
= ez
->vec_ite(s
.at(i
), part_of_b
, tmp
);
146 if (cell
->type
== "$safe_pmux")
147 tmp
= ez
->vec_ite(ez
->onehot(s
, true), tmp
, a
);
148 ez
->assume(ez
->vec_eq(tmp
, y
));
152 if (cell
->type
== "$pos" || cell
->type
== "$neg") {
153 std::vector
<int> a
= importSigSpec(cell
->connections
.at("\\A"));
154 std::vector
<int> y
= importSigSpec(cell
->connections
.at("\\Y"));
155 if (cell
->type
== "$pos") {
156 ez
->assume(ez
->vec_eq(a
, y
));
158 std::vector
<int> zero(a
.size(), ez
->FALSE
);
159 ez
->assume(ez
->vec_eq(ez
->vec_sub(zero
, a
), y
));
164 if (cell
->type
== "$reduce_and" || cell
->type
== "$reduce_or" || cell
->type
== "$reduce_xor" ||
165 cell
->type
== "$reduce_xnor" || cell
->type
== "$reduce_bool" || cell
->type
== "$logic_not") {
166 std::vector
<int> a
= importSigSpec(cell
->connections
.at("\\A"));
167 std::vector
<int> y
= importSigSpec(cell
->connections
.at("\\Y"));
168 if (cell
->type
== "$reduce_and")
169 ez
->SET(ez
->expression(ez
->OpAnd
, a
), y
.at(0));
170 if (cell
->type
== "$reduce_or" || cell
->type
== "$reduce_bool")
171 ez
->SET(ez
->expression(ez
->OpOr
, a
), y
.at(0));
172 if (cell
->type
== "$reduce_xor")
173 ez
->SET(ez
->expression(ez
->OpXor
, a
), y
.at(0));
174 if (cell
->type
== "$reduce_xnor")
175 ez
->SET(ez
->NOT(ez
->expression(ez
->OpXor
, a
)), y
.at(0));
176 if (cell
->type
== "$logic_not")
177 ez
->SET(ez
->NOT(ez
->expression(ez
->OpOr
, a
)), y
.at(0));
178 for (size_t i
= 1; i
< y
.size(); i
++)
183 if (cell
->type
== "$logic_and" || cell
->type
== "$logic_or") {
184 int a
= ez
->expression(ez
->OpOr
, importSigSpec(cell
->connections
.at("\\A")));
185 int b
= ez
->expression(ez
->OpOr
, importSigSpec(cell
->connections
.at("\\B")));
186 std::vector
<int> y
= importSigSpec(cell
->connections
.at("\\Y"));
187 if (cell
->type
== "$logic_and")
188 ez
->SET(ez
->expression(ez
->OpAnd
, a
, b
), y
.at(0));
190 ez
->SET(ez
->expression(ez
->OpOr
, a
, b
), y
.at(0));
191 for (size_t i
= 1; i
< y
.size(); i
++)
196 if (cell
->type
== "$lt" || cell
->type
== "$le" || cell
->type
== "$eq" || cell
->type
== "$ne" || cell
->type
== "$ge" || cell
->type
== "$gt") {
197 bool is_signed
= cell
->parameters
["\\A_SIGNED"].as_bool() && cell
->parameters
["\\B_SIGNED"].as_bool();
198 std::vector
<int> a
= importSigSpec(cell
->connections
.at("\\A"));
199 std::vector
<int> b
= importSigSpec(cell
->connections
.at("\\B"));
200 std::vector
<int> y
= importSigSpec(cell
->connections
.at("\\Y"));
201 extendSignalWidth(a
, b
, cell
);
202 if (cell
->type
== "$lt")
203 ez
->SET(is_signed
? ez
->vec_lt_signed(a
, b
) : ez
->vec_lt_unsigned(a
, b
), y
.at(0));
204 if (cell
->type
== "$le")
205 ez
->SET(is_signed
? ez
->vec_le_signed(a
, b
) : ez
->vec_le_unsigned(a
, b
), y
.at(0));
206 if (cell
->type
== "$eq")
207 ez
->SET(ez
->vec_eq(a
, b
), y
.at(0));
208 if (cell
->type
== "$ne")
209 ez
->SET(ez
->vec_ne(a
, b
), y
.at(0));
210 if (cell
->type
== "$ge")
211 ez
->SET(is_signed
? ez
->vec_ge_signed(a
, b
) : ez
->vec_ge_unsigned(a
, b
), y
.at(0));
212 if (cell
->type
== "$gt")
213 ez
->SET(is_signed
? ez
->vec_gt_signed(a
, b
) : ez
->vec_gt_unsigned(a
, b
), y
.at(0));
214 for (size_t i
= 1; i
< y
.size(); i
++)
219 // Unsupported internal cell types: $shl $shr $sshl $sshr $mul $div $mod $pow