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
36 struct FmcombineWorker
40 Module
*original
= nullptr;
41 Module
*module
= nullptr;
42 IdString orig_type
, combined_type
;
44 FmcombineWorker(Design
*design
, IdString orig_type
, const opts_t
&opts
) :
45 opts(opts
), design(design
), original(design
->module(orig_type
)),
46 orig_type(orig_type
), combined_type("$fmcombine" + orig_type
.str())
50 SigSpec
import_sig(SigSpec sig
, const string
&suffix
)
53 for (auto chunk
: sig
.chunks()) {
54 if (chunk
.wire
!= nullptr)
55 chunk
.wire
= module
->wire(chunk
.wire
->name
.str() + suffix
);
61 Cell
*import_prim_cell(Cell
*cell
, const string
&suffix
)
63 Cell
*c
= module
->addCell(cell
->name
.str() + suffix
, cell
->type
);
64 c
->parameters
= cell
->parameters
;
65 c
->attributes
= cell
->attributes
;
67 for (auto &conn
: cell
->connections())
68 c
->setPort(conn
.first
, import_sig(conn
.second
, suffix
));
73 void import_hier_cell(Cell
*cell
)
75 if (!cell
->parameters
.empty())
76 log_cmd_error("Cell %s.%s has unresolved instance parameters.\n", log_id(original
), log_id(cell
));
78 FmcombineWorker
sub_worker(design
, cell
->type
, opts
);
79 sub_worker
.generate();
81 Cell
*c
= module
->addCell(cell
->name
.str() + "_combined", sub_worker
.combined_type
);
82 // c->parameters = cell->parameters;
83 c
->attributes
= cell
->attributes
;
85 for (auto &conn
: cell
->connections()) {
86 c
->setPort(conn
.first
.str() + "_gold", import_sig(conn
.second
, "_gold"));
87 c
->setPort(conn
.first
.str() + "_gate", import_sig(conn
.second
, "_gate"));
93 if (design
->module(combined_type
)) {
94 // log("Combined module %s already exists.\n", log_id(combined_type));
98 log("Generating combined module %s from module %s.\n", log_id(combined_type
), log_id(orig_type
));
99 module
= design
->addModule(combined_type
);
101 for (auto wire
: original
->wires()) {
102 module
->addWire(wire
->name
.str() + "_gold", wire
);
103 module
->addWire(wire
->name
.str() + "_gate", wire
);
105 module
->fixup_ports();
107 for (auto cell
: original
->cells()) {
108 if (design
->module(cell
->type
) == nullptr) {
109 if (opts
.anyeq
&& cell
->type
.in("$anyseq", "$anyconst")) {
110 Cell
*gold
= import_prim_cell(cell
, "_gold");
111 for (auto &conn
: cell
->connections())
112 module
->connect(import_sig(conn
.second
, "_gate"), gold
->getPort(conn
.first
));
114 Cell
*gold
= import_prim_cell(cell
, "_gold");
115 Cell
*gate
= import_prim_cell(cell
, "_gate");
117 if (cell
->type
.in("$ff", "$dff", "$dffe",
118 "$dffsr", "$adff", "$dlatch", "$dlatchsr")) {
119 SigSpec gold_q
= gold
->getPort("\\Q");
120 SigSpec gate_q
= gate
->getPort("\\Q");
121 SigSpec en
= module
->Initstate(NEW_ID
);
122 SigSpec eq
= module
->Eq(NEW_ID
, gold_q
, gate_q
);
123 module
->addAssume(NEW_ID
, eq
, en
);
128 import_hier_cell(cell
);
132 for (auto &conn
: original
->connections()) {
133 module
->connect(import_sig(conn
.first
, "_gold"), import_sig(conn
.second
, "_gold"));
134 module
->connect(import_sig(conn
.first
, "_gate"), import_sig(conn
.second
, "_gate"));
141 ct
.setup_internals_eval();
142 ct
.setup_stdcells_eval();
144 SigMap
sigmap(module
);
146 dict
<SigBit
, SigBit
> data_bit_to_eq_net
;
147 dict
<Cell
*, SigSpec
> cell_to_eq_nets
;
148 dict
<SigSpec
, SigSpec
> reduce_db
;
149 dict
<SigSpec
, SigSpec
> invert_db
;
151 for (auto cell
: original
->cells())
153 if (!ct
.cell_known(cell
->type
))
156 for (auto &conn
: cell
->connections())
158 if (!cell
->output(conn
.first
))
161 SigSpec A
= import_sig(conn
.second
, "_gold");
162 SigSpec B
= import_sig(conn
.second
, "_gate");
163 SigBit EQ
= module
->Eq(NEW_ID
, A
, B
);
165 for (auto bit
: sigmap({A
, B
}))
166 data_bit_to_eq_net
[bit
] = EQ
;
168 cell_to_eq_nets
[cell
].append(EQ
);
172 for (auto cell
: original
->cells())
174 if (!ct
.cell_known(cell
->type
))
177 bool skip_cell
= !cell_to_eq_nets
.count(cell
);
178 pool
<SigBit
> src_eq_bits
;
180 for (auto &conn
: cell
->connections())
185 if (cell
->output(conn
.first
))
188 SigSpec A
= import_sig(conn
.second
, "_gold");
189 SigSpec B
= import_sig(conn
.second
, "_gate");
191 for (auto bit
: sigmap({A
, B
})) {
192 if (data_bit_to_eq_net
.count(bit
))
193 src_eq_bits
.insert(data_bit_to_eq_net
.at(bit
));
200 SigSpec antecedent
= SigSpec(src_eq_bits
);
201 antecedent
.sort_and_unify();
203 if (GetSize(antecedent
) > 1) {
204 if (reduce_db
.count(antecedent
) == 0)
205 reduce_db
[antecedent
] = module
->ReduceAnd(NEW_ID
, antecedent
);
206 antecedent
= reduce_db
.at(antecedent
);
209 SigSpec consequent
= cell_to_eq_nets
.at(cell
);
210 consequent
.sort_and_unify();
212 if (GetSize(consequent
) > 1) {
213 if (reduce_db
.count(consequent
) == 0)
214 reduce_db
[consequent
] = module
->ReduceAnd(NEW_ID
, consequent
);
215 consequent
= reduce_db
.at(consequent
);
219 module
->addAssume(NEW_ID
, consequent
, antecedent
);
223 if (invert_db
.count(antecedent
) == 0)
224 invert_db
[antecedent
] = module
->Not(NEW_ID
, antecedent
);
226 if (invert_db
.count(consequent
) == 0)
227 invert_db
[consequent
] = module
->Not(NEW_ID
, consequent
);
229 module
->addAssume(NEW_ID
, invert_db
.at(antecedent
), invert_db
.at(consequent
));
236 struct FmcombinePass
: public Pass
{
237 FmcombinePass() : Pass("fmcombine", "combine two instances of a cell into one") { }
238 void help() YS_OVERRIDE
240 // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
242 log(" fmcombine [options] module_name gold_cell gate_cell\n");
243 // log(" fmcombine [options] @gold_cell @gate_cell\n");
245 log("This pass takes two cells, which are instances of the same module, and replaces\n");
246 log("them with one instance of a special 'combined' module, that effectively\n");
247 log("contains two copies of the original module, plus some formal properties.\n");
249 log("This is useful for formal test benches that check what differences in behavior\n");
250 log("a slight difference in input causes in a module.\n");
253 log(" Insert assumptions that initially all FFs in both circuits have the\n");
254 log(" same initial values.\n");
257 log(" Do not duplicate $anyseq/$anyconst cells.\n");
260 log(" Insert forward hint assumptions into the combined module.\n");
263 log(" Insert backward hint assumptions into the combined module.\n");
264 log(" (Backward hints are logically equivalend to fordward hits, but\n");
265 log(" some solvers are faster with bwd hints, or even both -bwd and -fwd.)\n");
268 log(" Don't insert hint assumptions into the combined module.\n");
269 log(" (This should not provide any speedup over the original design, but\n");
270 log(" strangely sometimes it does.)\n");
272 log("If none of -fwd, -bwd, and -nop is given, then -fwd is used as default.\n");
275 void execute(std::vector
<std::string
> args
, RTLIL::Design
*design
) YS_OVERRIDE
278 Module
*module
= nullptr;
279 Cell
*gold_cell
= nullptr;
280 Cell
*gate_cell
= nullptr;
282 log_header(design
, "Executing FMCOMBINE pass.\n");
285 for (argidx
= 1; argidx
< args
.size(); argidx
++)
287 // if (args[argidx] == "-o" && argidx+1 < args.size()) {
288 // filename = args[++argidx];
291 if (args
[argidx
] == "-initeq") {
295 if (args
[argidx
] == "-anyeq") {
299 if (args
[argidx
] == "-fwd") {
303 if (args
[argidx
] == "-bwd") {
307 if (args
[argidx
] == "-nop") {
313 if (argidx
+2 == args
.size())
315 string gold_name
= args
[argidx
++];
316 string gate_name
= args
[argidx
++];
317 log_cmd_error("fmcombine @gold_cell @gate_cell call style is not implemented yet.");
319 else if (argidx
+3 == args
.size())
321 IdString module_name
= RTLIL::escape_id(args
[argidx
++]);
322 IdString gold_name
= RTLIL::escape_id(args
[argidx
++]);
323 IdString gate_name
= RTLIL::escape_id(args
[argidx
++]);
325 module
= design
->module(module_name
);
326 if (module
== nullptr)
327 log_cmd_error("Module %s not found.\n", log_id(module_name
));
329 gold_cell
= module
->cell(gold_name
);
330 if (gold_cell
== nullptr)
331 log_cmd_error("Gold cell %s not found in module %s.\n", log_id(gold_name
), log_id(module
));
333 gate_cell
= module
->cell(gate_name
);
334 if (gate_cell
== nullptr)
335 log_cmd_error("Gate cell %s not found in module %s.\n", log_id(gate_name
), log_id(module
));
339 log_cmd_error("Invalid number of arguments.\n");
341 // extra_args(args, argidx, design);
343 if (opts
.nop
&& (opts
.fwd
|| opts
.bwd
))
344 log_cmd_error("Option -nop can not be combined with -fwd and/or -bwd.\n");
346 if (!opts
.nop
&& !opts
.fwd
&& !opts
.bwd
)
349 if (gold_cell
->type
!= gate_cell
->type
)
350 log_cmd_error("Types of gold and gate cells do not match.\n");
351 if (!gold_cell
->parameters
.empty())
352 log_cmd_error("Gold cell has unresolved instance parameters.\n");
353 if (!gate_cell
->parameters
.empty())
354 log_cmd_error("Gate cell has unresolved instance parameters.\n");
356 FmcombineWorker
worker(design
, gold_cell
->type
, opts
);
358 IdString combined_cell_name
= module
->uniquify(stringf("\\%s_%s", log_id(gold_cell
), log_id(gate_cell
)));
360 Cell
*cell
= module
->addCell(combined_cell_name
, worker
.combined_type
);
361 cell
->attributes
= gold_cell
->attributes
;
362 cell
->add_strpool_attribute("\\src", gate_cell
->get_strpool_attribute("\\src"));
364 log("Combining cells %s and %s in module %s into new cell %s.\n", log_id(gold_cell
), log_id(gate_cell
), log_id(module
), log_id(cell
));
366 for (auto &conn
: gold_cell
->connections())
367 cell
->setPort(conn
.first
.str() + "_gold", conn
.second
);
368 module
->remove(gold_cell
);
370 for (auto &conn
: gate_cell
->connections())
371 cell
->setPort(conn
.first
.str() + "_gate", conn
.second
);
372 module
->remove(gate_cell
);
376 PRIVATE_NAMESPACE_END