summaryrefslogtreecommitdiff
path: root/passes/equiv
diff options
context:
space:
mode:
authorRuben Undheim <ruben.undheim@gmail.com>2019-10-18 19:56:51 +0000
committerRuben Undheim <ruben.undheim@gmail.com>2019-10-18 19:56:51 +0000
commit1f6bb85359149a016811e7e7fef980c3d45211e7 (patch)
tree749672f9a104cbfb25bb02acad6cb731724b9d56 /passes/equiv
parentff5734b20220e6fb4a3913cf5279ed94bb5156ea (diff)
New upstream version 0.9
Diffstat (limited to 'passes/equiv')
-rw-r--r--passes/equiv/equiv_opt.cc21
1 files changed, 17 insertions, 4 deletions
diff --git a/passes/equiv/equiv_opt.cc b/passes/equiv/equiv_opt.cc
index 86550a69..3596dfd7 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;
}
@@ -134,12 +142,17 @@ struct EquivOptPass:public ScriptPass
opts = " -map <filename> ...";
else
opts = techmap_opts;
- run("techmap -D EQUIV -autoproc" + opts);
+ run("techmap -wb -D EQUIV -autoproc" + opts);
}
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)