mirror of https://github.com/YosysHQ/yosys.git
Add -nocells flag to equiv_make and equiv_opt
The -nocells flag skips cell equivalence checking and only checks wire equivalence. This is useful when optimizations preserve functionality but rename or restructure cells, avoiding false negatives in equivalence checking.
This commit is contained in:
parent
967b47d984
commit
6bf9fc1817
|
|
@ -34,6 +34,7 @@ struct EquivMakeWorker
|
|||
vector<string> blacklists;
|
||||
vector<string> encfiles;
|
||||
bool make_assert;
|
||||
bool nocells;
|
||||
|
||||
pool<IdString> blacklist_names;
|
||||
dict<IdString, dict<Const, Const>> encdata;
|
||||
|
|
@ -419,7 +420,8 @@ struct EquivMakeWorker
|
|||
copy_to_equiv();
|
||||
find_undriven_nets(false);
|
||||
find_same_wires();
|
||||
find_same_cells();
|
||||
if (!nocells)
|
||||
find_same_cells();
|
||||
find_undriven_nets(true);
|
||||
}
|
||||
};
|
||||
|
|
@ -450,6 +452,9 @@ struct EquivMakePass : public Pass {
|
|||
log(" Check equivalence with $assert cells instead of $equiv.\n");
|
||||
log(" $eqx (===) is used to compare signals.");
|
||||
log("\n");
|
||||
log(" -nocells\n");
|
||||
log(" Do not check for equivalent cells, just wires.\n");
|
||||
log("\n");
|
||||
log("Note: The circuit created by this command is not a miter (with something like\n");
|
||||
log("a trigger output), but instead uses $equiv cells to encode the equivalence\n");
|
||||
log("checking problem. Use 'miter -equiv' if you want to create a miter circuit.\n");
|
||||
|
|
@ -461,6 +466,7 @@ struct EquivMakePass : public Pass {
|
|||
worker.ct.setup(design);
|
||||
worker.inames = false;
|
||||
worker.make_assert = false;
|
||||
worker.nocells = false;
|
||||
|
||||
size_t argidx;
|
||||
for (argidx = 1; argidx < args.size(); argidx++)
|
||||
|
|
@ -481,6 +487,10 @@ struct EquivMakePass : public Pass {
|
|||
worker.make_assert = true;
|
||||
continue;
|
||||
}
|
||||
if (args[argidx] == "-nocells") {
|
||||
worker.nocells = true;
|
||||
continue;
|
||||
}
|
||||
break;
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -60,6 +60,9 @@ struct EquivOptPass:public ScriptPass
|
|||
log(" -undef\n");
|
||||
log(" enable modelling of undef states during equiv_induct.\n");
|
||||
log("\n");
|
||||
log(" -nocells\n");
|
||||
log(" Do not check for equivalent cells, just wires.\n");
|
||||
log("\n");
|
||||
log(" -nocheck\n");
|
||||
log(" disable running check before and after the command under test.\n");
|
||||
log("\n");
|
||||
|
|
@ -126,6 +129,10 @@ struct EquivOptPass:public ScriptPass
|
|||
async2sync = true;
|
||||
continue;
|
||||
}
|
||||
if (args[argidx] == "-nocells") {
|
||||
make_opts += " -nocells";
|
||||
continue;
|
||||
}
|
||||
break;
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -0,0 +1,13 @@
|
|||
read_verilog <<EOT
|
||||
module gold(input a, input b, output y);
|
||||
assign y = a & b;
|
||||
endmodule
|
||||
|
||||
module gate(input a, input b, output y);
|
||||
assign y = a & b;
|
||||
endmodule
|
||||
EOT
|
||||
|
||||
equiv_make -nocells gold gate equiv
|
||||
equiv_simple equiv
|
||||
equiv_status -assert equiv
|
||||
Loading…
Reference in New Issue