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"
23 PRIVATE_NAMESPACE_BEGIN
25 struct EquivStatusPass
: public Pass
{
26 EquivStatusPass() : Pass("equiv_status", "print status of equivalent checking module") { }
27 void help() YS_OVERRIDE
29 // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
31 log(" equiv_status [options] [selection]\n");
33 log("This command prints status information for all selected $equiv cells.\n");
36 log(" produce an error if any unproven $equiv cell is found\n");
39 void execute(std::vector
<std::string
> args
, Design
*design
) YS_OVERRIDE
41 bool assert_mode
= false;
42 int unproven_count
= 0;
44 log_header(design
, "Executing EQUIV_STATUS pass.\n");
47 for (argidx
= 1; argidx
< args
.size(); argidx
++) {
48 if (args
[argidx
] == "-assert") {
54 extra_args(args
, argidx
, design
);
56 for (auto module
: design
->selected_modules())
58 vector
<Cell
*> unproven_equiv_cells
;
59 int proven_equiv_cells
= 0;
61 for (auto cell
: module
->selected_cells())
62 if (cell
->type
== "$equiv") {
63 if (cell
->getPort("\\A") != cell
->getPort("\\B"))
64 unproven_equiv_cells
.push_back(cell
);
69 if (unproven_equiv_cells
.empty() && !proven_equiv_cells
) {
70 log("No $equiv cells found in %s.\n", log_id(module
));
74 log("Found %d $equiv cells in %s:\n", GetSize(unproven_equiv_cells
) + proven_equiv_cells
, log_id(module
));
75 log(" Of those cells %d are proven and %d are unproven.\n", proven_equiv_cells
, GetSize(unproven_equiv_cells
));
76 if (unproven_equiv_cells
.empty()) {
77 log(" Equivalence successfully proven!\n");
79 for (auto cell
: unproven_equiv_cells
)
80 log(" Unproven $equiv %s: %s %s\n", log_id(cell
), log_signal(cell
->getPort("\\A")), log_signal(cell
->getPort("\\B")));
83 unproven_count
+= GetSize(unproven_equiv_cells
);
86 if (unproven_count
!= 0) {
87 log("Found a total of %d unproven $equiv cells.\n", unproven_count
);
88 if (assert_mode
&& unproven_count
!= 0)
89 log_error("Found %d unproven $equiv cells in 'equiv_status -assert'.\n", unproven_count
);