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/yosys.h"
21 #include "kernel/sigtools.h"
22 #include "kernel/celltypes.h"
25 PRIVATE_NAMESPACE_BEGIN
27 struct EquivMiterWorker
39 Module
*source_module
;
41 dict
<SigBit
, Cell
*> bit_to_driver
;
42 pool
<Cell
*> seed_cells
, miter_cells
;
43 pool
<Wire
*> miter_wires
;
45 void follow_cone(pool
<Cell
*> &cone
, pool
<Cell
*> &leaves
, Cell
*c
, bool gold_mode
)
50 if (c
->type
== "$equiv" && !seed_cells
.count(c
)) {
57 for (auto &conn
: c
->connections()) {
58 if (!ct
.cell_input(c
->type
, conn
.first
))
60 if (c
->type
== "$equiv" && (conn
.first
== "\\A") != gold_mode
)
62 for (auto bit
: sigmap(conn
.second
))
63 if (bit_to_driver
.count(bit
))
64 follow_cone(cone
, leaves
, bit_to_driver
.at(bit
), gold_mode
);
68 void find_miter_cells_wires()
70 sigmap
.set(source_module
);
72 // initialize bit_to_driver
74 for (auto c
: source_module
->cells())
75 for (auto &conn
: c
->connections())
76 if (ct
.cell_output(c
->type
, conn
.first
))
77 for (auto bit
: sigmap(conn
.second
))
79 bit_to_driver
[bit
] = c
;
83 for (auto c
: source_module
->selected_cells())
84 if (c
->type
== "$equiv") {
85 log("Seed $equiv cell: %s\n", log_id(c
));
89 // follow cone from seed cells to next $equiv
93 pool
<Cell
*> gold_cone
, gold_leaves
;
94 pool
<Cell
*> gate_cone
, gate_leaves
;
96 for (auto c
: seed_cells
) {
97 follow_cone(gold_cone
, gold_leaves
, c
, true);
98 follow_cone(gate_cone
, gate_leaves
, c
, false);
101 log("Gold cone: %d cells (%d leaves).\n", GetSize(gold_cone
), GetSize(gold_leaves
));
102 log("Gate cone: %d cells (%d leaves).\n", GetSize(gate_cone
), GetSize(gate_leaves
));
104 // done if all leaves are shared leaves
106 if (gold_leaves
== gate_leaves
) {
107 miter_cells
= gold_cone
;
108 miter_cells
.insert(gate_cone
.begin(), gate_cone
.end());
109 log("Selected %d miter cells.\n", GetSize(miter_cells
));
113 // remove shared leaves
115 for (auto it
= gold_leaves
.begin(); it
!= gold_leaves
.end(); ) {
116 auto it2
= gate_leaves
.find(*it
);
117 if (it2
!= gate_leaves
.end()) {
118 it
= gold_leaves
.erase(it
);
119 gate_leaves
.erase(it2
);
124 // add remaining leaves to seeds and re-run
126 log("Adding %d gold and %d gate seed cells.\n", GetSize(gold_leaves
), GetSize(gate_leaves
));
127 seed_cells
.insert(gold_leaves
.begin(), gold_leaves
.end());
128 seed_cells
.insert(gate_leaves
.begin(), gate_leaves
.end());
131 for (auto c
: miter_cells
)
132 for (auto &conn
: c
->connections())
133 for (auto bit
: sigmap(conn
.second
))
135 miter_wires
.insert(bit
.wire
);
136 log("Selected %d miter wires.\n", GetSize(miter_wires
));
141 // copy wires and cells
143 for (auto w
: miter_wires
)
144 miter_module
->addWire(w
->name
, w
->width
);
145 for (auto c
: miter_cells
) {
146 miter_module
->addCell(c
->name
, c
);
147 auto mc
= miter_module
->cell(c
->name
);
148 for (auto &conn
: mc
->connections())
149 mc
->setPort(conn
.first
, sigmap(conn
.second
));
152 // fixup wire references in cells
156 struct RewriteSigSpecWorker
{
158 void operator()(SigSpec
&sig
) {
159 vector
<SigChunk
> chunks
= sig
.chunks();
160 for (auto &c
: chunks
)
162 c
.wire
= mod
->wires_
.at(c
.wire
->name
);
167 RewriteSigSpecWorker rewriteSigSpecWorker
;
168 rewriteSigSpecWorker
.mod
= miter_module
;
169 miter_module
->rewrite_sigspecs(rewriteSigSpecWorker
);
171 // find undriven or unused wires
173 pool
<SigBit
> driven_bits
, used_bits
;
175 for (auto c
: miter_module
->cells())
176 for (auto &conn
: c
->connections()) {
177 if (ct
.cell_input(c
->type
, conn
.first
))
178 for (auto bit
: conn
.second
)
180 used_bits
.insert(bit
);
181 if (ct
.cell_output(c
->type
, conn
.first
))
182 for (auto bit
: conn
.second
)
184 driven_bits
.insert(bit
);
189 for (auto w
: miter_module
->wires()) {
190 for (auto bit
: SigSpec(w
)) {
191 if (driven_bits
.count(bit
) && !used_bits
.count(bit
))
192 w
->port_output
= true;
193 if (!driven_bits
.count(bit
) && used_bits
.count(bit
))
194 w
->port_input
= true;
196 if (w
->port_output
&& w
->port_input
)
197 log("Created miter inout port %s.\n", log_id(w
));
198 else if (w
->port_output
)
199 log("Created miter output port %s.\n", log_id(w
));
200 else if (w
->port_input
)
201 log("Created miter input port %s.\n", log_id(w
));
204 miter_module
->fixup_ports();
209 if (!mode_trigger
&& !mode_cmp
&& !mode_assert
)
212 SigSpec trigger_signals
;
213 vector
<Cell
*> equiv_cells
;
215 for (auto c
: miter_module
->cells())
216 if (c
->type
== "$equiv" && c
->getPort("\\A") != c
->getPort("\\B"))
217 equiv_cells
.push_back(c
);
219 for (auto c
: equiv_cells
)
221 SigSpec cmp
= mode_undef
?
222 miter_module
->LogicOr(NEW_ID
, miter_module
->Eqx(NEW_ID
, c
->getPort("\\A"), State::Sx
),
223 miter_module
->Eqx(NEW_ID
, c
->getPort("\\A"), c
->getPort("\\B"))) :
224 miter_module
->Eq(NEW_ID
, c
->getPort("\\A"), c
->getPort("\\B"));
227 string cmp_name
= string("\\cmp") + log_signal(c
->getPort("\\Y"));
228 for (int i
= 1; i
< GetSize(cmp_name
); i
++)
229 if (cmp_name
[i
] == '\\')
231 else if (cmp_name
[i
] == ' ')
232 cmp_name
= cmp_name
.substr(0, i
) + cmp_name
.substr(i
+1);
233 auto w
= miter_module
->addWire(cmp_name
);
234 w
->port_output
= true;
235 miter_module
->connect(w
, cmp
);
239 miter_module
->addAssert(NEW_ID
, cmp
, State::S1
);
241 trigger_signals
.append(miter_module
->Not(NEW_ID
, cmp
));
245 auto w
= miter_module
->addWire("\\trigger");
246 w
->port_output
= true;
247 miter_module
->addReduceOr(NEW_ID
, trigger_signals
, w
);
250 miter_module
->fixup_ports();
255 log("Creating miter %s from module %s.\n", log_id(miter_module
), log_id(source_module
));
256 find_miter_cells_wires();
262 struct EquivMiterPass
: public Pass
{
263 EquivMiterPass() : Pass("equiv_miter", "extract miter from equiv circuit") { }
264 void help() YS_OVERRIDE
266 // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
268 log(" equiv_miter [options] miter_module [selection]\n");
270 log("This creates a miter module for further analysis of the selected $equiv cells.\n");
273 log(" Create a trigger output\n");
276 log(" Create cmp_* outputs for individual unproven $equiv cells\n");
279 log(" Create a $assert cell for each unproven $equiv cell\n");
282 log(" Create compare logic that handles undefs correctly\n");
285 void execute(std::vector
<std::string
> args
, RTLIL::Design
*design
) YS_OVERRIDE
287 EquivMiterWorker worker
;
288 worker
.ct
.setup(design
);
289 worker
.mode_trigger
= false;
290 worker
.mode_cmp
= false;
291 worker
.mode_assert
= false;
292 worker
.mode_undef
= false;
295 for (argidx
= 1; argidx
< args
.size(); argidx
++)
297 if (args
[argidx
] == "-trigger") {
298 worker
.mode_trigger
= true;
301 if (args
[argidx
] == "-cmp") {
302 worker
.mode_cmp
= true;
305 if (args
[argidx
] == "-assert") {
306 worker
.mode_assert
= true;
309 if (args
[argidx
] == "-undef") {
310 worker
.mode_undef
= true;
316 if (argidx
>= args
.size())
317 log_cmd_error("Invalid number of arguments.\n");
319 worker
.miter_name
= RTLIL::escape_id(args
[argidx
++]);
320 extra_args(args
, argidx
, design
);
322 if (design
->module(worker
.miter_name
))
323 log_cmd_error("Miter module %s already exists.\n", log_id(worker
.miter_name
));
325 worker
.source_module
= nullptr;
326 for (auto m
: design
->selected_modules()) {
327 if (worker
.source_module
!= nullptr)
328 goto found_two_modules
;
329 worker
.source_module
= m
;
332 if (worker
.source_module
== nullptr)
334 log_cmd_error("Exactly one module must be selected for 'equiv_miter'!\n");
336 log_header(design
, "Executing EQUIV_MITER pass.\n");
338 worker
.miter_module
= design
->addModule(worker
.miter_name
);
343 PRIVATE_NAMESPACE_END