diff options
| author | Clifford Wolf <clifford@clifford.at> | 2019-04-30 17:00:34 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-04-30 17:00:34 +0200 |
| commit | d9d50b0b0c4da21c9bf2b0f1499297368b808491 (patch) | |
| tree | 6a926310738ae81a1b98f74066e79f423310b33b /passes | |
| parent | 727eec04c53c6863b18883a5afd7cee1cb52a157 (diff) | |
| parent | 58e991a0eb36f0a5a23170e6818338efa7445a44 (diff) | |
| download | yosys-d9d50b0b0c4da21c9bf2b0f1499297368b808491.tar.gz yosys-d9d50b0b0c4da21c9bf2b0f1499297368b808491.tar.bz2 yosys-d9d50b0b0c4da21c9bf2b0f1499297368b808491.zip | |
Merge branch 'master' into eddie/refactor_synth_xilinx
Diffstat (limited to 'passes')
| -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) |