diff options
author | Eddie Hung <eddie@fpgeh.com> | 2019-04-26 11:14:33 -0700 |
---|---|---|
committer | Eddie Hung <eddie@fpgeh.com> | 2019-04-26 11:16:48 -0700 |
commit | 159e7cc2983e3d026fa8c5187252bb890a04b96f (patch) | |
tree | aab15aaba82a7fcfa54aefb1b5de2154d9333749 | |
parent | 408161ea3af78c747b9d45cd6482f2e4d9170085 (diff) | |
download | yosys-159e7cc2983e3d026fa8c5187252bb890a04b96f.tar.gz yosys-159e7cc2983e3d026fa8c5187252bb890a04b96f.tar.bz2 yosys-159e7cc2983e3d026fa8c5187252bb890a04b96f.zip |
Add -undef option to equiv_opt, passed to equiv_induct
-rw-r--r-- | passes/equiv/equiv_opt.cc | 19 |
1 files changed, 16 insertions, 3 deletions
diff --git a/passes/equiv/equiv_opt.cc b/passes/equiv/equiv_opt.cc index e5dda9c24..3596dfd7b 100644 --- a/passes/equiv/equiv_opt.cc +++ b/passes/equiv/equiv_opt.cc @@ -44,7 +44,10 @@ struct EquivOptPass:public ScriptPass log(" useful for handling architecture-specific primitives.\n"); log("\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("The following commands are executed by this verification command:\n"); help_script(); @@ -52,13 +55,14 @@ struct EquivOptPass:public ScriptPass } std::string command, techmap_opts; - bool assert; + bool assert, undef; void clear_flags() YS_OVERRIDE { command = ""; techmap_opts = ""; assert = false; + undef = false; } void execute(std::vector < std::string > args, RTLIL::Design * design) YS_OVERRIDE @@ -84,6 +88,10 @@ struct EquivOptPass:public ScriptPass assert = true; continue; } + if (args[argidx] == "-undef") { + undef = true; + continue; + } break; } @@ -139,7 +147,12 @@ struct EquivOptPass:public ScriptPass if (check_label("prove")) { 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) run("equiv_status [-assert] equiv"); else if (assert) |