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 void read_blacklists()
42 for (auto fn
: blacklists
)
46 log_cmd_error("Can't open blacklist file '%s'!\n", fn
.c_str());
49 while (std::getline(f
, line
)) {
51 token
= next_token(line
);
54 blacklist_names
.insert(RTLIL::escape_id(token
));
62 for (auto fn
: encfiles
)
66 log_cmd_error("Can't open encfile '%s'!\n", fn
.c_str());
68 dict
<Const
, Const
> *ed
= nullptr;
70 while (std::getline(f
, line
))
72 token
= next_token(line
);
73 if (token
.empty() || token
[0] == '#')
76 if (token
== ".fsm") {
77 IdString modname
= RTLIL::escape_id(next_token(line
));
78 IdString signame
= RTLIL::escape_id(next_token(line
));
79 if (encdata
.count(signame
))
80 log_cmd_error("Re-definition of signal '%s' in encfile '%s'!\n", signame
.c_str(), fn
.c_str());
81 encdata
[signame
] = dict
<Const
, Const
>();
82 ed
= &encdata
[signame
];
86 if (token
== ".map") {
87 Const gold_bits
= Const::from_string(next_token(line
));
88 Const gate_bits
= Const::from_string(next_token(line
));
89 (*ed
)[gold_bits
] = gate_bits
;
93 log_cmd_error("Syntax error in encfile '%s'!\n", fn
.c_str());
100 Module
*gold_clone
= gold_mod
->clone();
101 Module
*gate_clone
= gate_mod
->clone();
103 for (auto it
: gold_clone
->wires().to_vector()) {
104 if ((it
->name
[0] == '\\' || inames
) && blacklist_names
.count(it
->name
) == 0)
105 wire_names
.insert(it
->name
);
106 gold_clone
->rename(it
, it
->name
.str() + "_gold");
109 for (auto it
: gold_clone
->cells().to_vector()) {
110 if ((it
->name
[0] == '\\' || inames
) && blacklist_names
.count(it
->name
) == 0)
111 cell_names
.insert(it
->name
);
112 gold_clone
->rename(it
, it
->name
.str() + "_gold");
115 for (auto it
: gate_clone
->wires().to_vector()) {
116 if ((it
->name
[0] == '\\' || inames
) && blacklist_names
.count(it
->name
) == 0)
117 wire_names
.insert(it
->name
);
118 gate_clone
->rename(it
, it
->name
.str() + "_gate");
121 for (auto it
: gate_clone
->cells().to_vector()) {
122 if ((it
->name
[0] == '\\' || inames
) && blacklist_names
.count(it
->name
) == 0)
123 cell_names
.insert(it
->name
);
124 gate_clone
->rename(it
, it
->name
.str() + "_gate");
127 gold_clone
->cloneInto(equiv_mod
);
128 gate_clone
->cloneInto(equiv_mod
);
133 void find_same_wires()
135 SigMap
assign_map(equiv_mod
);
136 SigMap rd_signal_map
;
138 // list of cells without added $equiv cells
139 auto cells_list
= equiv_mod
->cells().to_vector();
141 for (auto id
: wire_names
)
143 IdString gold_id
= id
.str() + "_gold";
144 IdString gate_id
= id
.str() + "_gate";
146 Wire
*gold_wire
= equiv_mod
->wire(gold_id
);
147 Wire
*gate_wire
= equiv_mod
->wire(gate_id
);
149 if (encdata
.count(id
))
151 log("Creating encoder/decoder for signal %s.\n", log_id(id
));
153 Wire
*dec_wire
= equiv_mod
->addWire(id
.str() + "_decoded", gold_wire
->width
);
154 Wire
*enc_wire
= equiv_mod
->addWire(id
.str() + "_encoded", gate_wire
->width
);
156 SigSpec dec_a
, dec_b
, dec_s
;
157 SigSpec enc_a
, enc_b
, enc_s
;
159 dec_a
= SigSpec(State::Sx
, dec_wire
->width
);
160 enc_a
= SigSpec(State::Sx
, enc_wire
->width
);
162 for (auto &it
: encdata
.at(id
))
164 SigSpec dec_sig
= gate_wire
, dec_pat
= it
.second
;
165 SigSpec enc_sig
= dec_wire
, enc_pat
= it
.first
;
167 if (GetSize(dec_sig
) != GetSize(dec_pat
))
168 log_error("Invalid pattern %s for signal %s of size %d!\n",
169 log_signal(dec_pat
), log_signal(dec_sig
), GetSize(dec_sig
));
171 if (GetSize(enc_sig
) != GetSize(enc_pat
))
172 log_error("Invalid pattern %s for signal %s of size %d!\n",
173 log_signal(enc_pat
), log_signal(enc_sig
), GetSize(enc_sig
));
175 SigSpec reduced_dec_sig
, reduced_dec_pat
;
176 for (int i
= 0; i
< GetSize(dec_sig
); i
++)
177 if (dec_pat
[i
] == State::S0
|| dec_pat
[i
] == State::S1
) {
178 reduced_dec_sig
.append(dec_sig
[i
]);
179 reduced_dec_pat
.append(dec_pat
[i
]);
182 SigSpec reduced_enc_sig
, reduced_enc_pat
;
183 for (int i
= 0; i
< GetSize(enc_sig
); i
++)
184 if (enc_pat
[i
] == State::S0
|| enc_pat
[i
] == State::S1
) {
185 reduced_enc_sig
.append(enc_sig
[i
]);
186 reduced_enc_pat
.append(enc_pat
[i
]);
189 SigSpec dec_result
= it
.first
;
190 for (auto &bit
: dec_result
)
191 if (bit
!= State::S1
) bit
= State::S0
;
193 SigSpec enc_result
= it
.second
;
194 for (auto &bit
: enc_result
)
195 if (bit
!= State::S1
) bit
= State::S0
;
197 SigSpec dec_eq
= equiv_mod
->addWire(NEW_ID
);
198 SigSpec enc_eq
= equiv_mod
->addWire(NEW_ID
);
200 equiv_mod
->addEq(NEW_ID
, reduced_dec_sig
, reduced_dec_pat
, dec_eq
);
201 cells_list
.push_back(equiv_mod
->addEq(NEW_ID
, reduced_enc_sig
, reduced_enc_pat
, enc_eq
));
203 dec_s
.append(dec_eq
);
204 enc_s
.append(enc_eq
);
205 dec_b
.append(dec_result
);
206 enc_b
.append(enc_result
);
209 equiv_mod
->addPmux(NEW_ID
, dec_a
, dec_b
, dec_s
, dec_wire
);
210 equiv_mod
->addPmux(NEW_ID
, enc_a
, enc_b
, enc_s
, enc_wire
);
212 rd_signal_map
.add(assign_map(gate_wire
), enc_wire
);
213 gate_wire
= dec_wire
;
216 if (gold_wire
== nullptr || gate_wire
== nullptr || gold_wire
->width
!= gate_wire
->width
) {
217 if (gold_wire
&& gold_wire
->port_id
)
218 log_error("Can't match gold port `%s' to a gate port.\n", log_id(gold_wire
));
219 if (gate_wire
&& gate_wire
->port_id
)
220 log_error("Can't match gate port `%s' to a gold port.\n", log_id(gate_wire
));
224 log("Presumably equivalent wires: %s (%s), %s (%s) -> %s\n",
225 log_id(gold_wire
), log_signal(assign_map(gold_wire
)),
226 log_id(gate_wire
), log_signal(assign_map(gate_wire
)), log_id(id
));
228 if (gold_wire
->port_output
|| gate_wire
->port_output
)
230 Wire
*wire
= equiv_mod
->addWire(id
, gold_wire
->width
);
231 wire
->port_output
= true;
232 gold_wire
->port_input
= false;
233 gate_wire
->port_input
= false;
234 gold_wire
->port_output
= false;
235 gate_wire
->port_output
= false;
237 for (int i
= 0; i
< wire
->width
; i
++)
238 equiv_mod
->addEquiv(NEW_ID
, SigSpec(gold_wire
, i
), SigSpec(gate_wire
, i
), SigSpec(wire
, i
));
240 rd_signal_map
.add(assign_map(gold_wire
), wire
);
241 rd_signal_map
.add(assign_map(gate_wire
), wire
);
244 if (gold_wire
->port_input
|| gate_wire
->port_input
)
246 Wire
*wire
= equiv_mod
->addWire(id
, gold_wire
->width
);
247 wire
->port_input
= true;
248 gold_wire
->port_input
= false;
249 gate_wire
->port_input
= false;
250 equiv_mod
->connect(gold_wire
, wire
);
251 equiv_mod
->connect(gate_wire
, wire
);
255 Wire
*wire
= equiv_mod
->addWire(id
, gold_wire
->width
);
257 for (int i
= 0; i
< wire
->width
; i
++)
258 equiv_mod
->addEquiv(NEW_ID
, SigSpec(gold_wire
, i
), SigSpec(gate_wire
, i
), SigSpec(wire
, i
));
260 rd_signal_map
.add(assign_map(gold_wire
), wire
);
261 rd_signal_map
.add(assign_map(gate_wire
), wire
);
265 for (auto c
: cells_list
)
266 for (auto &conn
: c
->connections())
267 if (ct
.cell_input(c
->type
, conn
.first
)) {
268 SigSpec old_sig
= assign_map(conn
.second
);
269 SigSpec new_sig
= rd_signal_map(old_sig
);
270 if (old_sig
!= new_sig
) {
271 log("Changing input %s of cell %s (%s): %s -> %s\n",
272 log_id(conn
.first
), log_id(c
), log_id(c
->type
),
273 log_signal(old_sig
), log_signal(new_sig
));
274 c
->setPort(conn
.first
, new_sig
);
278 equiv_mod
->fixup_ports();
281 void find_same_cells()
283 SigMap
assign_map(equiv_mod
);
285 for (auto id
: cell_names
)
287 IdString gold_id
= id
.str() + "_gold";
288 IdString gate_id
= id
.str() + "_gate";
290 Cell
*gold_cell
= equiv_mod
->cell(gold_id
);
291 Cell
*gate_cell
= equiv_mod
->cell(gate_id
);
293 if (gold_cell
== nullptr || gate_cell
== nullptr || gold_cell
->type
!= gate_cell
->type
|| !ct
.cell_known(gold_cell
->type
) ||
294 gold_cell
->parameters
!= gate_cell
->parameters
|| GetSize(gold_cell
->connections()) != GetSize(gate_cell
->connections()))
298 for (auto gold_conn
: gold_cell
->connections())
299 if (!gate_cell
->connections().count(gold_conn
.first
))
300 goto try_next_cell_name
;
302 log("Presumably equivalent cells: %s %s (%s) -> %s\n",
303 log_id(gold_cell
), log_id(gate_cell
), log_id(gold_cell
->type
), log_id(id
));
305 for (auto gold_conn
: gold_cell
->connections())
307 SigSpec gold_sig
= assign_map(gold_conn
.second
);
308 SigSpec gate_sig
= assign_map(gate_cell
->getPort(gold_conn
.first
));
310 if (ct
.cell_output(gold_cell
->type
, gold_conn
.first
)) {
311 equiv_mod
->connect(gate_sig
, gold_sig
);
315 for (int i
= 0; i
< GetSize(gold_sig
); i
++)
316 if (gold_sig
[i
] != gate_sig
[i
]) {
317 Wire
*w
= equiv_mod
->addWire(NEW_ID
);
318 equiv_mod
->addEquiv(NEW_ID
, gold_sig
[i
], gate_sig
[i
], w
);
322 gold_cell
->setPort(gold_conn
.first
, gold_sig
);
325 equiv_mod
->remove(gate_cell
);
326 equiv_mod
->rename(gold_cell
, id
);
330 void find_undriven_nets()
332 pool
<SigBit
> undriven_bits
;
333 SigMap
assign_map(equiv_mod
);
335 for (auto wire
: equiv_mod
->wires()) {
336 for (auto bit
: assign_map(wire
))
338 undriven_bits
.insert(bit
);
341 for (auto wire
: equiv_mod
->wires()) {
342 if (wire
->port_input
)
343 for (auto bit
: assign_map(wire
))
344 undriven_bits
.erase(bit
);
347 for (auto cell
: equiv_mod
->cells()) {
348 for (auto &conn
: cell
->connections())
349 if (!ct
.cell_known(cell
->type
) || ct
.cell_output(cell
->type
, conn
.first
))
350 for (auto bit
: assign_map(conn
.second
))
351 undriven_bits
.erase(bit
);
354 SigSpec
undriven_sig(undriven_bits
);
355 undriven_sig
.sort_and_unify();
357 for (auto chunk
: undriven_sig
.chunks()) {
358 log("Setting undriven nets to undef: %s\n", log_signal(chunk
));
359 equiv_mod
->connect(chunk
, SigSpec(State::Sx
, chunk
.width
));
368 find_undriven_nets();
372 struct EquivMakePass
: public Pass
{
373 EquivMakePass() : Pass("equiv_make", "prepare a circuit for equivalence checking") { }
376 // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
378 log(" equiv_make [options] gold_module gate_module equiv_module\n");
380 log("This creates a module annotated with $equiv cells from two presumably\n");
381 log("equivalent modules. Use commands such as 'equiv_simple' and 'equiv_status'\n");
382 log("to work with the created equivalent checking module.\n");
385 log(" Also match cells and wires with $... names.\n");
387 log(" -blacklist <file>\n");
388 log(" Do not match cells or signals that match the names in the file.\n");
390 log(" -encfile <file>\n");
391 log(" Match FSM encodings using the desiption from the file.\n");
392 log(" See 'help fsm_recode' for details.\n");
394 log("Note: The circuit created by this command is not a miter (with something like\n");
395 log("a trigger output), but instead uses $equiv cells to encode the equivalence\n");
396 log("checking problem. Use 'miter -equiv' if you want to create a miter circuit.\n");
399 virtual void execute(std::vector
<std::string
> args
, RTLIL::Design
*design
)
401 EquivMakeWorker worker
;
402 worker
.ct
.setup(design
);
403 worker
.inames
= false;
406 for (argidx
= 1; argidx
< args
.size(); argidx
++)
408 if (args
[argidx
] == "-inames") {
409 worker
.inames
= true;
412 if (args
[argidx
] == "-blacklist" && argidx
+1 < args
.size()) {
413 worker
.blacklists
.push_back(args
[++argidx
]);
416 if (args
[argidx
] == "-encfile" && argidx
+1 < args
.size()) {
417 worker
.encfiles
.push_back(args
[++argidx
]);
423 if (argidx
+3 != args
.size())
424 log_cmd_error("Invalid number of arguments.\n");
426 worker
.gold_mod
= design
->module(RTLIL::escape_id(args
[argidx
]));
427 worker
.gate_mod
= design
->module(RTLIL::escape_id(args
[argidx
+1]));
428 worker
.equiv_mod
= design
->module(RTLIL::escape_id(args
[argidx
+2]));
430 if (worker
.gold_mod
== nullptr)
431 log_cmd_error("Can't find gold module %s.\n", args
[argidx
].c_str());
433 if (worker
.gate_mod
== nullptr)
434 log_cmd_error("Can't find gate module %s.\n", args
[argidx
+1].c_str());
436 if (worker
.equiv_mod
!= nullptr)
437 log_cmd_error("Equiv module %s already exists.\n", args
[argidx
+2].c_str());
439 if (worker
.gold_mod
->has_memories() || worker
.gold_mod
->has_processes())
440 log_cmd_error("Gold module contains memories or procresses. Run 'memory' or 'proc' respectively.\n");
442 if (worker
.gate_mod
->has_memories() || worker
.gate_mod
->has_processes())
443 log_cmd_error("Gate module contains memories or procresses. Run 'memory' or 'proc' respectively.\n");
445 worker
.read_blacklists();
446 worker
.read_encfiles();
448 log_header("Executing EQUIV_MAKE pass (creating equiv checking module).\n");
450 worker
.equiv_mod
= design
->addModule(RTLIL::escape_id(args
[argidx
+2]));
455 PRIVATE_NAMESPACE_END