riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Merge pull request #960 from YosysHQ/eddie/equiv_opt_undef 

Add -undef option to equiv_opt, passed to equiv_induct
This commit is contained in:
Clifford Wolf 2019-04-29 13:54:26 +02:00 committed by GitHub
parent 8fde245ea2 159e7cc298
commit 314ff1e4ca
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 16 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

19
passes/equiv/equiv_opt.cc
View File

@ -44,7 +44,10 @@ struct EquivOptPass:public ScriptPass
log(" useful for handling architecture-specific primitives.\n"); log(" useful for handling architecture-specific primitives.\n");
log("\n"); log("\n");
log(" -assert\n"); log(" -assert\n");
log(" produce an error if the circuits are not equivalent\n"); log(" produce an error if the circuits are not equivalent.\n");
log("\n");
log(" -undef\n");
log(" enable modelling of undef states during equiv_induct.\n");
log("\n"); log("\n");
log("The following commands are executed by this verification command:\n"); log("The following commands are executed by this verification command:\n");
help_script(); help_script();
@ -52,13 +55,14 @@ struct EquivOptPass:public ScriptPass
} }
std::string command, techmap_opts; std::string command, techmap_opts;
bool assert; bool assert, undef;
void clear_flags() YS_OVERRIDE void clear_flags() YS_OVERRIDE
{ {
command = ""; command = "";
techmap_opts = ""; techmap_opts = "";
assert = false; assert = false;
undef = false;
} }
void execute(std::vector < std::string > args, RTLIL::Design * design) YS_OVERRIDE void execute(std::vector < std::string > args, RTLIL::Design * design) YS_OVERRIDE
@ -84,6 +88,10 @@ struct EquivOptPass:public ScriptPass
assert = true; assert = true;
continue; continue;
} }
if (args[argidx] == "-undef") {
undef = true;
continue;
}
break; break;
} }
@ -139,7 +147,12 @@ struct EquivOptPass:public ScriptPass
if (check_label("prove")) { if (check_label("prove")) {
run("equiv_make gold gate equiv"); run("equiv_make gold gate equiv");
run("equiv_induct equiv"); if (help_mode)
run("equiv_induct [-undef] equiv");
else if (undef)
run("equiv_induct -undef equiv");
else
run("equiv_induct equiv");
if (help_mode) if (help_mode)
run("equiv_status [-assert] equiv"); run("equiv_status [-assert] equiv");
else if (assert) else if (assert)