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 void read_blacklists()
45 for (auto fn
: blacklists
)
49 log_cmd_error("Can't open blacklist file '%s'!\n", fn
.c_str());
52 while (std::getline(f
, line
)) {
54 token
= next_token(line
);
57 blacklist_names
.insert(RTLIL::escape_id(token
));
65 for (auto fn
: encfiles
)
69 log_cmd_error("Can't open encfile '%s'!\n", fn
.c_str());
71 dict
<Const
, Const
> *ed
= nullptr;
73 while (std::getline(f
, line
))
75 token
= next_token(line
);
76 if (token
.empty() || token
[0] == '#')
79 if (token
== ".fsm") {
80 IdString modname
= RTLIL::escape_id(next_token(line
));
81 IdString signame
= RTLIL::escape_id(next_token(line
));
82 if (encdata
.count(signame
))
83 log_cmd_error("Re-definition of signal '%s' in encfile '%s'!\n", signame
.c_str(), fn
.c_str());
84 encdata
[signame
] = dict
<Const
, Const
>();
85 ed
= &encdata
[signame
];
89 if (token
== ".map") {
90 Const gold_bits
= Const::from_string(next_token(line
));
91 Const gate_bits
= Const::from_string(next_token(line
));
92 (*ed
)[gold_bits
] = gate_bits
;
96 log_cmd_error("Syntax error in encfile '%s'!\n", fn
.c_str());
103 Module
*gold_clone
= gold_mod
->clone();
104 Module
*gate_clone
= gate_mod
->clone();
106 for (auto it
: gold_clone
->wires().to_vector()) {
107 if ((it
->name
[0] == '\\' || inames
) && blacklist_names
.count(it
->name
) == 0)
108 wire_names
.insert(it
->name
);
109 gold_clone
->rename(it
, it
->name
.str() + "_gold");
112 for (auto it
: gold_clone
->cells().to_vector()) {
113 if ((it
->name
[0] == '\\' || inames
) && blacklist_names
.count(it
->name
) == 0)
114 cell_names
.insert(it
->name
);
115 gold_clone
->rename(it
, it
->name
.str() + "_gold");
118 for (auto it
: gate_clone
->wires().to_vector()) {
119 if ((it
->name
[0] == '\\' || inames
) && blacklist_names
.count(it
->name
) == 0)
120 wire_names
.insert(it
->name
);
121 gate_clone
->rename(it
, it
->name
.str() + "_gate");
124 for (auto it
: gate_clone
->cells().to_vector()) {
125 if ((it
->name
[0] == '\\' || inames
) && blacklist_names
.count(it
->name
) == 0)
126 cell_names
.insert(it
->name
);
127 gate_clone
->rename(it
, it
->name
.str() + "_gate");
130 gold_clone
->cloneInto(equiv_mod
);
131 gate_clone
->cloneInto(equiv_mod
);
136 void find_same_wires()
138 SigMap
assign_map(equiv_mod
);
139 SigMap rd_signal_map
;
141 // list of cells without added $equiv cells
142 auto cells_list
= equiv_mod
->cells().to_vector();
144 for (auto id
: wire_names
)
146 IdString gold_id
= id
.str() + "_gold";
147 IdString gate_id
= id
.str() + "_gate";
149 Wire
*gold_wire
= equiv_mod
->wire(gold_id
);
150 Wire
*gate_wire
= equiv_mod
->wire(gate_id
);
152 if (encdata
.count(id
))
154 log("Creating encoder/decoder for signal %s.\n", log_id(id
));
156 Wire
*dec_wire
= equiv_mod
->addWire(id
.str() + "_decoded", gold_wire
->width
);
157 Wire
*enc_wire
= equiv_mod
->addWire(id
.str() + "_encoded", gate_wire
->width
);
159 SigSpec dec_a
, dec_b
, dec_s
;
160 SigSpec enc_a
, enc_b
, enc_s
;
162 dec_a
= SigSpec(State::Sx
, dec_wire
->width
);
163 enc_a
= SigSpec(State::Sx
, enc_wire
->width
);
165 for (auto &it
: encdata
.at(id
))
167 SigSpec dec_sig
= gate_wire
, dec_pat
= it
.second
;
168 SigSpec enc_sig
= dec_wire
, enc_pat
= it
.first
;
170 if (GetSize(dec_sig
) != GetSize(dec_pat
))
171 log_error("Invalid pattern %s for signal %s of size %d!\n",
172 log_signal(dec_pat
), log_signal(dec_sig
), GetSize(dec_sig
));
174 if (GetSize(enc_sig
) != GetSize(enc_pat
))
175 log_error("Invalid pattern %s for signal %s of size %d!\n",
176 log_signal(enc_pat
), log_signal(enc_sig
), GetSize(enc_sig
));
178 SigSpec reduced_dec_sig
, reduced_dec_pat
;
179 for (int i
= 0; i
< GetSize(dec_sig
); i
++)
180 if (dec_pat
[i
] == State::S0
|| dec_pat
[i
] == State::S1
) {
181 reduced_dec_sig
.append(dec_sig
[i
]);
182 reduced_dec_pat
.append(dec_pat
[i
]);
185 SigSpec reduced_enc_sig
, reduced_enc_pat
;
186 for (int i
= 0; i
< GetSize(enc_sig
); i
++)
187 if (enc_pat
[i
] == State::S0
|| enc_pat
[i
] == State::S1
) {
188 reduced_enc_sig
.append(enc_sig
[i
]);
189 reduced_enc_pat
.append(enc_pat
[i
]);
192 SigSpec dec_result
= it
.first
;
193 for (auto &bit
: dec_result
)
194 if (bit
!= State::S1
) bit
= State::S0
;
196 SigSpec enc_result
= it
.second
;
197 for (auto &bit
: enc_result
)
198 if (bit
!= State::S1
) bit
= State::S0
;
200 SigSpec dec_eq
= equiv_mod
->addWire(NEW_ID
);
201 SigSpec enc_eq
= equiv_mod
->addWire(NEW_ID
);
203 equiv_mod
->addEq(NEW_ID
, reduced_dec_sig
, reduced_dec_pat
, dec_eq
);
204 cells_list
.push_back(equiv_mod
->addEq(NEW_ID
, reduced_enc_sig
, reduced_enc_pat
, enc_eq
));
206 dec_s
.append(dec_eq
);
207 enc_s
.append(enc_eq
);
208 dec_b
.append(dec_result
);
209 enc_b
.append(enc_result
);
212 equiv_mod
->addPmux(NEW_ID
, dec_a
, dec_b
, dec_s
, dec_wire
);
213 equiv_mod
->addPmux(NEW_ID
, enc_a
, enc_b
, enc_s
, enc_wire
);
215 rd_signal_map
.add(assign_map(gate_wire
), enc_wire
);
216 gate_wire
= dec_wire
;
219 if (gold_wire
== nullptr || gate_wire
== nullptr || gold_wire
->width
!= gate_wire
->width
) {
220 if (gold_wire
&& gold_wire
->port_id
)
221 log_error("Can't match gold port `%s' to a gate port.\n", log_id(gold_wire
));
222 if (gate_wire
&& gate_wire
->port_id
)
223 log_error("Can't match gate port `%s' to a gold port.\n", log_id(gate_wire
));
227 log("Presumably equivalent wires: %s (%s), %s (%s) -> %s\n",
228 log_id(gold_wire
), log_signal(assign_map(gold_wire
)),
229 log_id(gate_wire
), log_signal(assign_map(gate_wire
)), log_id(id
));
231 if (gold_wire
->port_output
|| gate_wire
->port_output
)
233 Wire
*wire
= equiv_mod
->addWire(id
, gold_wire
->width
);
234 wire
->port_output
= true;
235 gold_wire
->port_input
= false;
236 gate_wire
->port_input
= false;
237 gold_wire
->port_output
= false;
238 gate_wire
->port_output
= false;
240 for (int i
= 0; i
< wire
->width
; i
++)
241 equiv_mod
->addEquiv(NEW_ID
, SigSpec(gold_wire
, i
), SigSpec(gate_wire
, i
), SigSpec(wire
, i
));
243 rd_signal_map
.add(assign_map(gold_wire
), wire
);
244 rd_signal_map
.add(assign_map(gate_wire
), wire
);
247 if (gold_wire
->port_input
|| gate_wire
->port_input
)
249 Wire
*wire
= equiv_mod
->addWire(id
, gold_wire
->width
);
250 wire
->port_input
= true;
251 gold_wire
->port_input
= false;
252 gate_wire
->port_input
= false;
253 equiv_mod
->connect(gold_wire
, wire
);
254 equiv_mod
->connect(gate_wire
, wire
);
258 Wire
*wire
= equiv_mod
->addWire(id
, gold_wire
->width
);
259 SigSpec rdmap_gold
, rdmap_gate
, rdmap_equiv
;
261 for (int i
= 0; i
< wire
->width
; i
++) {
262 if (undriven_bits
.count(assign_map(SigBit(gold_wire
, i
)))) {
263 log(" Skipping signal bit %s [%d]: undriven on gold side.\n", id2cstr(gold_wire
->name
), i
);
266 if (undriven_bits
.count(assign_map(SigBit(gate_wire
, i
)))) {
267 log(" Skipping signal bit %s [%d]: undriven on gate side.\n", id2cstr(gate_wire
->name
), i
);
270 equiv_mod
->addEquiv(NEW_ID
, SigSpec(gold_wire
, i
), SigSpec(gate_wire
, i
), SigSpec(wire
, i
));
271 rdmap_gold
.append(SigBit(gold_wire
, i
));
272 rdmap_gate
.append(SigBit(gate_wire
, i
));
273 rdmap_equiv
.append(SigBit(wire
, i
));
276 rd_signal_map
.add(rdmap_gold
, rdmap_equiv
);
277 rd_signal_map
.add(rdmap_gate
, rdmap_equiv
);
281 for (auto c
: cells_list
)
282 for (auto &conn
: c
->connections())
283 if (!ct
.cell_output(c
->type
, conn
.first
)) {
284 SigSpec old_sig
= assign_map(conn
.second
);
285 SigSpec new_sig
= rd_signal_map(old_sig
);
286 if (old_sig
!= new_sig
) {
287 log("Changing input %s of cell %s (%s): %s -> %s\n",
288 log_id(conn
.first
), log_id(c
), log_id(c
->type
),
289 log_signal(old_sig
), log_signal(new_sig
));
290 c
->setPort(conn
.first
, new_sig
);
294 equiv_mod
->fixup_ports();
297 void find_same_cells()
299 SigMap
assign_map(equiv_mod
);
301 for (auto id
: cell_names
)
303 IdString gold_id
= id
.str() + "_gold";
304 IdString gate_id
= id
.str() + "_gate";
306 Cell
*gold_cell
= equiv_mod
->cell(gold_id
);
307 Cell
*gate_cell
= equiv_mod
->cell(gate_id
);
309 if (gold_cell
== nullptr || gate_cell
== nullptr || gold_cell
->type
!= gate_cell
->type
|| !ct
.cell_known(gold_cell
->type
) ||
310 gold_cell
->parameters
!= gate_cell
->parameters
|| GetSize(gold_cell
->connections()) != GetSize(gate_cell
->connections()))
314 for (auto gold_conn
: gold_cell
->connections())
315 if (!gate_cell
->connections().count(gold_conn
.first
))
316 goto try_next_cell_name
;
318 log("Presumably equivalent cells: %s %s (%s) -> %s\n",
319 log_id(gold_cell
), log_id(gate_cell
), log_id(gold_cell
->type
), log_id(id
));
321 for (auto gold_conn
: gold_cell
->connections())
323 SigSpec gold_sig
= assign_map(gold_conn
.second
);
324 SigSpec gate_sig
= assign_map(gate_cell
->getPort(gold_conn
.first
));
326 if (ct
.cell_output(gold_cell
->type
, gold_conn
.first
)) {
327 equiv_mod
->connect(gate_sig
, gold_sig
);
331 for (int i
= 0; i
< GetSize(gold_sig
); i
++)
332 if (gold_sig
[i
] != gate_sig
[i
]) {
333 Wire
*w
= equiv_mod
->addWire(NEW_ID
);
334 equiv_mod
->addEquiv(NEW_ID
, gold_sig
[i
], gate_sig
[i
], w
);
338 gold_cell
->setPort(gold_conn
.first
, gold_sig
);
341 equiv_mod
->remove(gate_cell
);
342 equiv_mod
->rename(gold_cell
, id
);
346 void find_undriven_nets(bool mark
)
348 undriven_bits
.clear();
349 assign_map
.set(equiv_mod
);
351 for (auto wire
: equiv_mod
->wires()) {
352 for (auto bit
: assign_map(wire
))
354 undriven_bits
.insert(bit
);
357 for (auto wire
: equiv_mod
->wires()) {
358 if (wire
->port_input
)
359 for (auto bit
: assign_map(wire
))
360 undriven_bits
.erase(bit
);
363 for (auto cell
: equiv_mod
->cells()) {
364 for (auto &conn
: cell
->connections())
365 if (!ct
.cell_known(cell
->type
) || ct
.cell_output(cell
->type
, conn
.first
))
366 for (auto bit
: assign_map(conn
.second
))
367 undriven_bits
.erase(bit
);
371 SigSpec
undriven_sig(undriven_bits
);
372 undriven_sig
.sort_and_unify();
374 for (auto chunk
: undriven_sig
.chunks()) {
375 log("Setting undriven nets to undef: %s\n", log_signal(chunk
));
376 equiv_mod
->connect(chunk
, SigSpec(State::Sx
, chunk
.width
));
384 find_undriven_nets(false);
387 find_undriven_nets(true);
391 struct EquivMakePass
: public Pass
{
392 EquivMakePass() : Pass("equiv_make", "prepare a circuit for equivalence checking") { }
393 void help() YS_OVERRIDE
395 // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
397 log(" equiv_make [options] gold_module gate_module equiv_module\n");
399 log("This creates a module annotated with $equiv cells from two presumably\n");
400 log("equivalent modules. Use commands such as 'equiv_simple' and 'equiv_status'\n");
401 log("to work with the created equivalent checking module.\n");
404 log(" Also match cells and wires with $... names.\n");
406 log(" -blacklist <file>\n");
407 log(" Do not match cells or signals that match the names in the file.\n");
409 log(" -encfile <file>\n");
410 log(" Match FSM encodings using the description from the file.\n");
411 log(" See 'help fsm_recode' for details.\n");
413 log("Note: The circuit created by this command is not a miter (with something like\n");
414 log("a trigger output), but instead uses $equiv cells to encode the equivalence\n");
415 log("checking problem. Use 'miter -equiv' if you want to create a miter circuit.\n");
418 void execute(std::vector
<std::string
> args
, RTLIL::Design
*design
) YS_OVERRIDE
420 EquivMakeWorker worker
;
421 worker
.ct
.setup(design
);
422 worker
.inames
= false;
425 for (argidx
= 1; argidx
< args
.size(); argidx
++)
427 if (args
[argidx
] == "-inames") {
428 worker
.inames
= true;
431 if (args
[argidx
] == "-blacklist" && argidx
+1 < args
.size()) {
432 worker
.blacklists
.push_back(args
[++argidx
]);
435 if (args
[argidx
] == "-encfile" && argidx
+1 < args
.size()) {
436 worker
.encfiles
.push_back(args
[++argidx
]);
442 if (argidx
+3 != args
.size())
443 log_cmd_error("Invalid number of arguments.\n");
445 worker
.gold_mod
= design
->module(RTLIL::escape_id(args
[argidx
]));
446 worker
.gate_mod
= design
->module(RTLIL::escape_id(args
[argidx
+1]));
447 worker
.equiv_mod
= design
->module(RTLIL::escape_id(args
[argidx
+2]));
449 if (worker
.gold_mod
== nullptr)
450 log_cmd_error("Can't find gold module %s.\n", args
[argidx
].c_str());
452 if (worker
.gate_mod
== nullptr)
453 log_cmd_error("Can't find gate module %s.\n", args
[argidx
+1].c_str());
455 if (worker
.equiv_mod
!= nullptr)
456 log_cmd_error("Equiv module %s already exists.\n", args
[argidx
+2].c_str());
458 if (worker
.gold_mod
->has_memories() || worker
.gold_mod
->has_processes())
459 log_cmd_error("Gold module contains memories or procresses. Run 'memory' or 'proc' respectively.\n");
461 if (worker
.gate_mod
->has_memories() || worker
.gate_mod
->has_processes())
462 log_cmd_error("Gate module contains memories or procresses. Run 'memory' or 'proc' respectively.\n");
464 worker
.read_blacklists();
465 worker
.read_encfiles();
467 log_header(design
, "Executing EQUIV_MAKE pass (creating equiv checking module).\n");
469 worker
.equiv_mod
= design
->addModule(RTLIL::escape_id(args
[argidx
+2]));
474 PRIVATE_NAMESPACE_END