diff options
Diffstat (limited to 'passes/equiv/equiv_opt.cc')
| -rw-r--r-- | passes/equiv/equiv_opt.cc | 28 |
1 files changed, 26 insertions, 2 deletions
diff --git a/passes/equiv/equiv_opt.cc b/passes/equiv/equiv_opt.cc index 19d1c25ac..c7e6d71a6 100644 --- a/passes/equiv/equiv_opt.cc +++ b/passes/equiv/equiv_opt.cc @@ -32,7 +32,8 @@ struct EquivOptPass:public ScriptPass log("\n"); log(" equiv_opt [options] [command]\n"); log("\n"); - log("This command checks circuit equivalence before and after an optimization pass.\n"); + log("This command uses temporal induction to check circuit equivalence before and\n"); + log("after an optimization pass.\n"); log("\n"); log(" -run <from_label>:<to_label>\n"); log(" only run the commands between the labels (see below). an empty\n"); @@ -46,6 +47,12 @@ struct EquivOptPass:public ScriptPass log(" -assert\n"); log(" produce an error if the circuits are not equivalent.\n"); log("\n"); + log(" -multiclock\n"); + log(" run clk2fflogic before equivalence checking.\n"); + log("\n"); + log(" -async2sync\n"); + log(" run async2sync before equivalence checking.\n"); + log("\n"); log(" -undef\n"); log(" enable modelling of undef states during equiv_induct.\n"); log("\n"); @@ -55,7 +62,7 @@ struct EquivOptPass:public ScriptPass } std::string command, techmap_opts; - bool assert, undef; + bool assert, undef, multiclock, async2sync; void clear_flags() YS_OVERRIDE { @@ -63,6 +70,8 @@ struct EquivOptPass:public ScriptPass techmap_opts = ""; assert = false; undef = false; + multiclock = false; + async2sync = false; } void execute(std::vector < std::string > args, RTLIL::Design * design) YS_OVERRIDE @@ -92,6 +101,14 @@ struct EquivOptPass:public ScriptPass undef = true; continue; } + if (args[argidx] == "-multiclock") { + multiclock = true; + continue; + } + if (args[argidx] == "-async2sync") { + async2sync = true; + continue; + } break; } @@ -111,6 +128,9 @@ struct EquivOptPass:public ScriptPass if (!design->full_selection()) log_cmd_error("This command only operates on fully selected designs!\n"); + if (async2sync && multiclock) + log_cmd_error("The '-async2sync' and '-multiclock' options are mutually exclusive!\n"); + log_header(design, "Executing EQUIV_OPT pass.\n"); log_push(); @@ -146,6 +166,10 @@ struct EquivOptPass:public ScriptPass } if (check_label("prove")) { + if (multiclock || help_mode) + run("clk2fflogic", "(only with -multiclock)"); + if (async2sync || help_mode) + run("async2sync", " (only with -async2sync)"); run("equiv_make gold gate equiv"); if (help_mode) run("equiv_induct [-undef] equiv"); |