2 * yosys -- Yosys Open SYnthesis Suite
4 * Copyright (C) 2012 Claire Xenia Wolf <claire@yosyshq.com>
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(stringf("$fmcombine%s", orig_type
.c_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(ID($anyseq
), ID($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 (RTLIL::builtin_ff_cell_types().count(cell
->type
)) {
118 SigSpec gold_q
= gold
->getPort(ID::Q
);
119 SigSpec gate_q
= gate
->getPort(ID::Q
);
120 SigSpec en
= module
->Initstate(NEW_ID
);
121 SigSpec eq
= module
->Eq(NEW_ID
, gold_q
, gate_q
);
122 module
->addAssume(NEW_ID
, eq
, en
);
127 import_hier_cell(cell
);
131 for (auto &conn
: original
->connections()) {
132 module
->connect(import_sig(conn
.first
, "_gold"), import_sig(conn
.second
, "_gold"));
133 module
->connect(import_sig(conn
.first
, "_gate"), import_sig(conn
.second
, "_gate"));
140 ct
.setup_internals_eval();
141 ct
.setup_stdcells_eval();
143 SigMap
sigmap(module
);
145 dict
<SigBit
, SigBit
> data_bit_to_eq_net
;
146 dict
<Cell
*, SigSpec
> cell_to_eq_nets
;
147 dict
<SigSpec
, SigSpec
> reduce_db
;
148 dict
<SigSpec
, SigSpec
> invert_db
;
150 for (auto cell
: original
->cells())
152 if (!ct
.cell_known(cell
->type
))
155 for (auto &conn
: cell
->connections())
157 if (!cell
->output(conn
.first
))
160 SigSpec A
= import_sig(conn
.second
, "_gold");
161 SigSpec B
= import_sig(conn
.second
, "_gate");
162 SigBit EQ
= module
->Eq(NEW_ID
, A
, B
);
164 for (auto bit
: sigmap({A
, B
}))
165 data_bit_to_eq_net
[bit
] = EQ
;
167 cell_to_eq_nets
[cell
].append(EQ
);
171 for (auto cell
: original
->cells())
173 if (!ct
.cell_known(cell
->type
))
176 bool skip_cell
= !cell_to_eq_nets
.count(cell
);
177 pool
<SigBit
> src_eq_bits
;
179 for (auto &conn
: cell
->connections())
184 if (cell
->output(conn
.first
))
187 SigSpec A
= import_sig(conn
.second
, "_gold");
188 SigSpec B
= import_sig(conn
.second
, "_gate");
190 for (auto bit
: sigmap({A
, B
})) {
191 if (data_bit_to_eq_net
.count(bit
))
192 src_eq_bits
.insert(data_bit_to_eq_net
.at(bit
));
199 SigSpec antecedent
= SigSpec(src_eq_bits
);
200 antecedent
.sort_and_unify();
202 if (GetSize(antecedent
) > 1) {
203 if (reduce_db
.count(antecedent
) == 0)
204 reduce_db
[antecedent
] = module
->ReduceAnd(NEW_ID
, antecedent
);
205 antecedent
= reduce_db
.at(antecedent
);
208 SigSpec consequent
= cell_to_eq_nets
.at(cell
);
209 consequent
.sort_and_unify();
211 if (GetSize(consequent
) > 1) {
212 if (reduce_db
.count(consequent
) == 0)
213 reduce_db
[consequent
] = module
->ReduceAnd(NEW_ID
, consequent
);
214 consequent
= reduce_db
.at(consequent
);
218 module
->addAssume(NEW_ID
, consequent
, antecedent
);
222 if (invert_db
.count(antecedent
) == 0)
223 invert_db
[antecedent
] = module
->Not(NEW_ID
, antecedent
);
225 if (invert_db
.count(consequent
) == 0)
226 invert_db
[consequent
] = module
->Not(NEW_ID
, consequent
);
228 module
->addAssume(NEW_ID
, invert_db
.at(antecedent
), invert_db
.at(consequent
));
235 struct FmcombinePass
: public Pass
{
236 FmcombinePass() : Pass("fmcombine", "combine two instances of a cell into one") { }
239 // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
241 log(" fmcombine [options] module_name gold_cell gate_cell\n");
242 // log(" fmcombine [options] @gold_cell @gate_cell\n");
244 log("This pass takes two cells, which are instances of the same module, and replaces\n");
245 log("them with one instance of a special 'combined' module, that effectively\n");
246 log("contains two copies of the original module, plus some formal properties.\n");
248 log("This is useful for formal test benches that check what differences in behavior\n");
249 log("a slight difference in input causes in a module.\n");
252 log(" Insert assumptions that initially all FFs in both circuits have the\n");
253 log(" same initial values.\n");
256 log(" Do not duplicate $anyseq/$anyconst cells.\n");
259 log(" Insert forward hint assumptions into the combined module.\n");
262 log(" Insert backward hint assumptions into the combined module.\n");
263 log(" (Backward hints are logically equivalend to fordward hits, but\n");
264 log(" some solvers are faster with bwd hints, or even both -bwd and -fwd.)\n");
267 log(" Don't insert hint assumptions into the combined module.\n");
268 log(" (This should not provide any speedup over the original design, but\n");
269 log(" strangely sometimes it does.)\n");
271 log("If none of -fwd, -bwd, and -nop is given, then -fwd is used as default.\n");
274 void execute(std::vector
<std::string
> args
, RTLIL::Design
*design
) override
277 Module
*module
= nullptr;
278 Cell
*gold_cell
= nullptr;
279 Cell
*gate_cell
= nullptr;
281 log_header(design
, "Executing FMCOMBINE pass.\n");
284 for (argidx
= 1; argidx
< args
.size(); argidx
++)
286 // if (args[argidx] == "-o" && argidx+1 < args.size()) {
287 // filename = args[++argidx];
290 if (args
[argidx
] == "-initeq") {
294 if (args
[argidx
] == "-anyeq") {
298 if (args
[argidx
] == "-fwd") {
302 if (args
[argidx
] == "-bwd") {
306 if (args
[argidx
] == "-nop") {
312 if (argidx
+2 == args
.size())
314 string gold_name
= args
[argidx
++];
315 string gate_name
= args
[argidx
++];
316 log_cmd_error("fmcombine @gold_cell @gate_cell call style is not implemented yet.");
318 else if (argidx
+3 == args
.size())
320 IdString module_name
= RTLIL::escape_id(args
[argidx
++]);
321 IdString gold_name
= RTLIL::escape_id(args
[argidx
++]);
322 IdString gate_name
= RTLIL::escape_id(args
[argidx
++]);
324 module
= design
->module(module_name
);
325 if (module
== nullptr)
326 log_cmd_error("Module %s not found.\n", log_id(module_name
));
328 gold_cell
= module
->cell(gold_name
);
329 if (gold_cell
== nullptr)
330 log_cmd_error("Gold cell %s not found in module %s.\n", log_id(gold_name
), log_id(module
));
332 gate_cell
= module
->cell(gate_name
);
333 if (gate_cell
== nullptr)
334 log_cmd_error("Gate cell %s not found in module %s.\n", log_id(gate_name
), log_id(module
));
338 log_cmd_error("Invalid number of arguments.\n");
340 // extra_args(args, argidx, design);
342 if (opts
.nop
&& (opts
.fwd
|| opts
.bwd
))
343 log_cmd_error("Option -nop can not be combined with -fwd and/or -bwd.\n");
345 if (!opts
.nop
&& !opts
.fwd
&& !opts
.bwd
)
348 if (gold_cell
->type
!= gate_cell
->type
)
349 log_cmd_error("Types of gold and gate cells do not match.\n");
350 if (!gold_cell
->parameters
.empty())
351 log_cmd_error("Gold cell has unresolved instance parameters.\n");
352 if (!gate_cell
->parameters
.empty())
353 log_cmd_error("Gate cell has unresolved instance parameters.\n");
355 FmcombineWorker
worker(design
, gold_cell
->type
, opts
);
357 IdString combined_cell_name
= module
->uniquify(stringf("\\%s_%s", log_id(gold_cell
), log_id(gate_cell
)));
359 Cell
*cell
= module
->addCell(combined_cell_name
, worker
.combined_type
);
360 cell
->attributes
= gold_cell
->attributes
;
361 cell
->add_strpool_attribute(ID::src
, gate_cell
->get_strpool_attribute(ID::src
));
363 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
));
365 for (auto &conn
: gold_cell
->connections())
366 cell
->setPort(conn
.first
.str() + "_gold", conn
.second
);
367 module
->remove(gold_cell
);
369 for (auto &conn
: gate_cell
->connections())
370 cell
->setPort(conn
.first
.str() + "_gate", conn
.second
);
371 module
->remove(gate_cell
);
375 PRIVATE_NAMESPACE_END