Add -undef option to equiv_opt, passed to equiv_induct

diff --git a/passes/equiv/equiv_opt.cc b/passes/equiv/equiv_opt.cc
index e5dda9c246c4cf5c5266529c3976aeaa291a77a3..3596dfd7b87d7503e8d1dc083ac04234ba0a61d9 100644 (file)
--- 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)