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 EquivMakeWorker
29 Module
*gold_mod
, *gate_mod
, *equiv_mod
;
30 pool
<IdString
> wire_names
, cell_names
;
34 vector
<string
> blacklists
;
35 vector
<string
> encfiles
;
37 pool
<IdString
> blacklist_names
;
38 dict
<IdString
, dict
<Const
, Const
>> encdata
;
40 pool
<SigBit
> undriven_bits
;
43 dict
<SigBit
, pool
<Cell
*>> bit2driven
; // map: bit <--> and its driven cells
49 comb_ct
.setup_internals();
50 comb_ct
.setup_stdcells();
53 void read_blacklists()
55 for (auto fn
: blacklists
)
59 log_cmd_error("Can't open blacklist file '%s'!\n", fn
.c_str());
62 while (std::getline(f
, line
)) {
64 token
= next_token(line
);
67 blacklist_names
.insert(RTLIL::escape_id(token
));
75 for (auto fn
: encfiles
)
79 log_cmd_error("Can't open encfile '%s'!\n", fn
.c_str());
81 dict
<Const
, Const
> *ed
= nullptr;
83 while (std::getline(f
, line
))
85 token
= next_token(line
);
86 if (token
.empty() || token
[0] == '#')
89 if (token
== ".fsm") {
90 IdString modname
= RTLIL::escape_id(next_token(line
));
91 IdString signame
= RTLIL::escape_id(next_token(line
));
92 if (encdata
.count(signame
))
93 log_cmd_error("Re-definition of signal '%s' in encfile '%s'!\n", signame
.c_str(), fn
.c_str());
94 encdata
[signame
] = dict
<Const
, Const
>();
95 ed
= &encdata
[signame
];
99 if (token
== ".map") {
100 Const gold_bits
= Const::from_string(next_token(line
));
101 Const gate_bits
= Const::from_string(next_token(line
));
102 (*ed
)[gold_bits
] = gate_bits
;
106 log_cmd_error("Syntax error in encfile '%s'!\n", fn
.c_str());
113 Module
*gold_clone
= gold_mod
->clone();
114 Module
*gate_clone
= gate_mod
->clone();
116 for (auto it
: gold_clone
->wires().to_vector()) {
117 if ((it
->name
[0] == '\\' || inames
) && blacklist_names
.count(it
->name
) == 0)
118 wire_names
.insert(it
->name
);
119 gold_clone
->rename(it
, it
->name
.str() + "_gold");
122 for (auto it
: gold_clone
->cells().to_vector()) {
123 if ((it
->name
[0] == '\\' || inames
) && blacklist_names
.count(it
->name
) == 0)
124 cell_names
.insert(it
->name
);
125 gold_clone
->rename(it
, it
->name
.str() + "_gold");
128 for (auto it
: gate_clone
->wires().to_vector()) {
129 if ((it
->name
[0] == '\\' || inames
) && blacklist_names
.count(it
->name
) == 0)
130 wire_names
.insert(it
->name
);
131 gate_clone
->rename(it
, it
->name
.str() + "_gate");
134 for (auto it
: gate_clone
->cells().to_vector()) {
135 if ((it
->name
[0] == '\\' || inames
) && blacklist_names
.count(it
->name
) == 0)
136 cell_names
.insert(it
->name
);
137 gate_clone
->rename(it
, it
->name
.str() + "_gate");
140 gold_clone
->cloneInto(equiv_mod
);
141 gate_clone
->cloneInto(equiv_mod
);
146 void find_same_wires()
148 SigMap
assign_map(equiv_mod
);
149 SigMap rd_signal_map
;
151 // list of cells without added $equiv cells
152 auto cells_list
= equiv_mod
->cells().to_vector();
154 for (auto id
: wire_names
)
156 IdString gold_id
= id
.str() + "_gold";
157 IdString gate_id
= id
.str() + "_gate";
159 Wire
*gold_wire
= equiv_mod
->wire(gold_id
);
160 Wire
*gate_wire
= equiv_mod
->wire(gate_id
);
162 if (encdata
.count(id
))
164 log("Creating encoder/decoder for signal %s.\n", log_id(id
));
166 Wire
*dec_wire
= equiv_mod
->addWire(id
.str() + "_decoded", gold_wire
->width
);
167 Wire
*enc_wire
= equiv_mod
->addWire(id
.str() + "_encoded", gate_wire
->width
);
169 SigSpec dec_a
, dec_b
, dec_s
;
170 SigSpec enc_a
, enc_b
, enc_s
;
172 dec_a
= SigSpec(State::Sx
, dec_wire
->width
);
173 enc_a
= SigSpec(State::Sx
, enc_wire
->width
);
175 for (auto &it
: encdata
.at(id
))
177 SigSpec dec_sig
= gate_wire
, dec_pat
= it
.second
;
178 SigSpec enc_sig
= dec_wire
, enc_pat
= it
.first
;
180 if (GetSize(dec_sig
) != GetSize(dec_pat
))
181 log_error("Invalid pattern %s for signal %s of size %d!\n",
182 log_signal(dec_pat
), log_signal(dec_sig
), GetSize(dec_sig
));
184 if (GetSize(enc_sig
) != GetSize(enc_pat
))
185 log_error("Invalid pattern %s for signal %s of size %d!\n",
186 log_signal(enc_pat
), log_signal(enc_sig
), GetSize(enc_sig
));
188 SigSpec reduced_dec_sig
, reduced_dec_pat
;
189 for (int i
= 0; i
< GetSize(dec_sig
); i
++)
190 if (dec_pat
[i
] == State::S0
|| dec_pat
[i
] == State::S1
) {
191 reduced_dec_sig
.append(dec_sig
[i
]);
192 reduced_dec_pat
.append(dec_pat
[i
]);
195 SigSpec reduced_enc_sig
, reduced_enc_pat
;
196 for (int i
= 0; i
< GetSize(enc_sig
); i
++)
197 if (enc_pat
[i
] == State::S0
|| enc_pat
[i
] == State::S1
) {
198 reduced_enc_sig
.append(enc_sig
[i
]);
199 reduced_enc_pat
.append(enc_pat
[i
]);
202 SigSpec dec_result
= it
.first
;
203 for (auto &bit
: dec_result
)
204 if (bit
!= State::S1
) bit
= State::S0
;
206 SigSpec enc_result
= it
.second
;
207 for (auto &bit
: enc_result
)
208 if (bit
!= State::S1
) bit
= State::S0
;
210 SigSpec dec_eq
= equiv_mod
->addWire(NEW_ID
);
211 SigSpec enc_eq
= equiv_mod
->addWire(NEW_ID
);
213 equiv_mod
->addEq(NEW_ID
, reduced_dec_sig
, reduced_dec_pat
, dec_eq
);
214 cells_list
.push_back(equiv_mod
->addEq(NEW_ID
, reduced_enc_sig
, reduced_enc_pat
, enc_eq
));
216 dec_s
.append(dec_eq
);
217 enc_s
.append(enc_eq
);
218 dec_b
.append(dec_result
);
219 enc_b
.append(enc_result
);
222 equiv_mod
->addPmux(NEW_ID
, dec_a
, dec_b
, dec_s
, dec_wire
);
223 equiv_mod
->addPmux(NEW_ID
, enc_a
, enc_b
, enc_s
, enc_wire
);
225 rd_signal_map
.add(assign_map(gate_wire
), enc_wire
);
226 gate_wire
= dec_wire
;
229 if (gold_wire
== nullptr || gate_wire
== nullptr || gold_wire
->width
!= gate_wire
->width
) {
230 if (gold_wire
&& gold_wire
->port_id
)
231 log_error("Can't match gold port `%s' to a gate port.\n", log_id(gold_wire
));
232 if (gate_wire
&& gate_wire
->port_id
)
233 log_error("Can't match gate port `%s' to a gold port.\n", log_id(gate_wire
));
237 log("Presumably equivalent wires: %s (%s), %s (%s) -> %s\n",
238 log_id(gold_wire
), log_signal(assign_map(gold_wire
)),
239 log_id(gate_wire
), log_signal(assign_map(gate_wire
)), log_id(id
));
241 if (gold_wire
->port_output
|| gate_wire
->port_output
)
243 Wire
*wire
= equiv_mod
->addWire(id
, gold_wire
->width
);
244 wire
->port_output
= true;
245 gold_wire
->port_input
= false;
246 gate_wire
->port_input
= false;
247 gold_wire
->port_output
= false;
248 gate_wire
->port_output
= false;
250 for (int i
= 0; i
< wire
->width
; i
++)
251 equiv_mod
->addEquiv(NEW_ID
, SigSpec(gold_wire
, i
), SigSpec(gate_wire
, i
), SigSpec(wire
, i
));
253 rd_signal_map
.add(assign_map(gold_wire
), wire
);
254 rd_signal_map
.add(assign_map(gate_wire
), wire
);
257 if (gold_wire
->port_input
|| gate_wire
->port_input
)
259 Wire
*wire
= equiv_mod
->addWire(id
, gold_wire
->width
);
260 wire
->port_input
= true;
261 gold_wire
->port_input
= false;
262 gate_wire
->port_input
= false;
263 equiv_mod
->connect(gold_wire
, wire
);
264 equiv_mod
->connect(gate_wire
, wire
);
268 Wire
*wire
= equiv_mod
->addWire(id
, gold_wire
->width
);
269 SigSpec rdmap_gold
, rdmap_gate
, rdmap_equiv
;
271 for (int i
= 0; i
< wire
->width
; i
++) {
272 if (undriven_bits
.count(assign_map(SigBit(gold_wire
, i
)))) {
273 log(" Skipping signal bit %s [%d]: undriven on gold side.\n", id2cstr(gold_wire
->name
), i
);
276 if (undriven_bits
.count(assign_map(SigBit(gate_wire
, i
)))) {
277 log(" Skipping signal bit %s [%d]: undriven on gate side.\n", id2cstr(gate_wire
->name
), i
);
280 equiv_mod
->addEquiv(NEW_ID
, SigSpec(gold_wire
, i
), SigSpec(gate_wire
, i
), SigSpec(wire
, i
));
281 rdmap_gold
.append(SigBit(gold_wire
, i
));
282 rdmap_gate
.append(SigBit(gate_wire
, i
));
283 rdmap_equiv
.append(SigBit(wire
, i
));
286 rd_signal_map
.add(rdmap_gold
, rdmap_equiv
);
287 rd_signal_map
.add(rdmap_gate
, rdmap_equiv
);
293 pool
<Cell
*> visited_cells
;
294 for (auto c
: cells_list
)
295 for (auto &conn
: c
->connections())
296 if (!ct
.cell_output(c
->type
, conn
.first
)) {
297 SigSpec old_sig
= assign_map(conn
.second
);
298 SigSpec new_sig
= rd_signal_map(old_sig
);
300 visited_cells
.clear();
301 if (old_sig
!= new_sig
) {
302 if (check_signal_in_fanout(visited_cells
, old_sig
, new_sig
))
305 log("Changing input %s of cell %s (%s): %s -> %s\n",
306 log_id(conn
.first
), log_id(c
), log_id(c
->type
),
307 log_signal(old_sig
), log_signal(new_sig
));
308 c
->setPort(conn
.first
, new_sig
);
312 equiv_mod
->fixup_ports();
315 void find_same_cells()
317 SigMap
assign_map(equiv_mod
);
319 for (auto id
: cell_names
)
321 IdString gold_id
= id
.str() + "_gold";
322 IdString gate_id
= id
.str() + "_gate";
324 Cell
*gold_cell
= equiv_mod
->cell(gold_id
);
325 Cell
*gate_cell
= equiv_mod
->cell(gate_id
);
327 if (gold_cell
== nullptr || gate_cell
== nullptr || gold_cell
->type
!= gate_cell
->type
|| !ct
.cell_known(gold_cell
->type
) ||
328 gold_cell
->parameters
!= gate_cell
->parameters
|| GetSize(gold_cell
->connections()) != GetSize(gate_cell
->connections()))
332 for (auto gold_conn
: gold_cell
->connections())
333 if (!gate_cell
->connections().count(gold_conn
.first
))
334 goto try_next_cell_name
;
336 log("Presumably equivalent cells: %s %s (%s) -> %s\n",
337 log_id(gold_cell
), log_id(gate_cell
), log_id(gold_cell
->type
), log_id(id
));
339 for (auto gold_conn
: gold_cell
->connections())
341 SigSpec gold_sig
= assign_map(gold_conn
.second
);
342 SigSpec gate_sig
= assign_map(gate_cell
->getPort(gold_conn
.first
));
344 if (ct
.cell_output(gold_cell
->type
, gold_conn
.first
)) {
345 equiv_mod
->connect(gate_sig
, gold_sig
);
349 for (int i
= 0; i
< GetSize(gold_sig
); i
++)
350 if (gold_sig
[i
] != gate_sig
[i
]) {
351 Wire
*w
= equiv_mod
->addWire(NEW_ID
);
352 equiv_mod
->addEquiv(NEW_ID
, gold_sig
[i
], gate_sig
[i
], w
);
356 gold_cell
->setPort(gold_conn
.first
, gold_sig
);
359 equiv_mod
->remove(gate_cell
);
360 equiv_mod
->rename(gold_cell
, id
);
364 void find_undriven_nets(bool mark
)
366 undriven_bits
.clear();
367 assign_map
.set(equiv_mod
);
369 for (auto wire
: equiv_mod
->wires()) {
370 for (auto bit
: assign_map(wire
))
372 undriven_bits
.insert(bit
);
375 for (auto wire
: equiv_mod
->wires()) {
376 if (wire
->port_input
)
377 for (auto bit
: assign_map(wire
))
378 undriven_bits
.erase(bit
);
381 for (auto cell
: equiv_mod
->cells()) {
382 for (auto &conn
: cell
->connections())
383 if (!ct
.cell_known(cell
->type
) || ct
.cell_output(cell
->type
, conn
.first
))
384 for (auto bit
: assign_map(conn
.second
))
385 undriven_bits
.erase(bit
);
389 SigSpec
undriven_sig(undriven_bits
);
390 undriven_sig
.sort_and_unify();
392 for (auto chunk
: undriven_sig
.chunks()) {
393 log("Setting undriven nets to undef: %s\n", log_signal(chunk
));
394 equiv_mod
->connect(chunk
, SigSpec(State::Sx
, chunk
.width
));
399 void init_bit2driven()
401 for (auto cell
: equiv_mod
->cells()) {
402 if (!ct
.cell_known(cell
->type
) && !cell
->type
.in("$dff", "$_DFF_P_", "$_DFF_N_", "$ff", "$_FF_"))
404 for (auto &conn
: cell
->connections())
406 if (yosys_celltypes
.cell_input(cell
->type
, conn
.first
))
407 for (auto bit
: assign_map(conn
.second
))
409 bit2driven
[bit
].insert(cell
);
415 bool check_signal_in_fanout(pool
<Cell
*> & visited_cells
, SigBit source_bit
, SigBit target_bit
)
417 if (source_bit
== target_bit
)
420 if (bit2driven
.count(source_bit
) == 0)
423 auto driven_cells
= bit2driven
.at(source_bit
);
424 for (auto driven_cell
: driven_cells
)
426 bool is_comb
= comb_ct
.cell_known(driven_cell
->type
);
430 if (visited_cells
.count(driven_cell
) > 0)
432 visited_cells
.insert(driven_cell
);
434 for (auto &conn
: driven_cell
->connections())
436 if (yosys_celltypes
.cell_input(driven_cell
->type
, conn
.first
))
439 for (auto bit
: conn
.second
) {
440 bool is_in_fanout
= check_signal_in_fanout(visited_cells
, bit
, target_bit
);
441 if (is_in_fanout
== true)
453 find_undriven_nets(false);
456 find_undriven_nets(true);
460 struct EquivMakePass
: public Pass
{
461 EquivMakePass() : Pass("equiv_make", "prepare a circuit for equivalence checking") { }
462 void help() YS_OVERRIDE
464 // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
466 log(" equiv_make [options] gold_module gate_module equiv_module\n");
468 log("This creates a module annotated with $equiv cells from two presumably\n");
469 log("equivalent modules. Use commands such as 'equiv_simple' and 'equiv_status'\n");
470 log("to work with the created equivalent checking module.\n");
473 log(" Also match cells and wires with $... names.\n");
475 log(" -blacklist <file>\n");
476 log(" Do not match cells or signals that match the names in the file.\n");
478 log(" -encfile <file>\n");
479 log(" Match FSM encodings using the description from the file.\n");
480 log(" See 'help fsm_recode' for details.\n");
482 log("Note: The circuit created by this command is not a miter (with something like\n");
483 log("a trigger output), but instead uses $equiv cells to encode the equivalence\n");
484 log("checking problem. Use 'miter -equiv' if you want to create a miter circuit.\n");
487 void execute(std::vector
<std::string
> args
, RTLIL::Design
*design
) YS_OVERRIDE
489 EquivMakeWorker worker
;
490 worker
.ct
.setup(design
);
491 worker
.inames
= false;
494 for (argidx
= 1; argidx
< args
.size(); argidx
++)
496 if (args
[argidx
] == "-inames") {
497 worker
.inames
= true;
500 if (args
[argidx
] == "-blacklist" && argidx
+1 < args
.size()) {
501 worker
.blacklists
.push_back(args
[++argidx
]);
504 if (args
[argidx
] == "-encfile" && argidx
+1 < args
.size()) {
505 worker
.encfiles
.push_back(args
[++argidx
]);
511 if (argidx
+3 != args
.size())
512 log_cmd_error("Invalid number of arguments.\n");
514 worker
.gold_mod
= design
->module(RTLIL::escape_id(args
[argidx
]));
515 worker
.gate_mod
= design
->module(RTLIL::escape_id(args
[argidx
+1]));
516 worker
.equiv_mod
= design
->module(RTLIL::escape_id(args
[argidx
+2]));
518 if (worker
.gold_mod
== nullptr)
519 log_cmd_error("Can't find gold module %s.\n", args
[argidx
].c_str());
521 if (worker
.gate_mod
== nullptr)
522 log_cmd_error("Can't find gate module %s.\n", args
[argidx
+1].c_str());
524 if (worker
.equiv_mod
!= nullptr)
525 log_cmd_error("Equiv module %s already exists.\n", args
[argidx
+2].c_str());
527 if (worker
.gold_mod
->has_memories() || worker
.gold_mod
->has_processes())
528 log_cmd_error("Gold module contains memories or procresses. Run 'memory' or 'proc' respectively.\n");
530 if (worker
.gate_mod
->has_memories() || worker
.gate_mod
->has_processes())
531 log_cmd_error("Gate module contains memories or procresses. Run 'memory' or 'proc' respectively.\n");
533 worker
.read_blacklists();
534 worker
.read_encfiles();
536 log_header(design
, "Executing EQUIV_MAKE pass (creating equiv checking module).\n");
538 worker
.equiv_mod
= design
->addModule(RTLIL::escape_id(args
[argidx
+2]));
543 PRIVATE_NAMESPACE_END