Add "chformal -assert2assume" and friends

diff --git a/passes/cmds/chformal.cc b/passes/cmds/chformal.cc
index 4200a5583ffe88ef86f9595f76b0a52f17fe3552..daed803547a26bff62cc1aca25181e6720306b33 100644 (file)
--- a/passes/cmds/chformal.cc
+++ b/passes/cmds/chformal.cc
@@ -55,9 +55,20 @@ struct ChformalPass : public Pass {
                log("    -skip <N>\n");
                log("        ignore activation of the constraint in the first <N> clock cycles\n");
                log("\n");
+               log("    -assert2assume\n");
+               log("    -assume2assert\n");
+               log("    -live2fair\n");
+               log("    -fair2live\n");
+               log("        change the roles of cells as indicated. this options can be combined\n");
+               log("\n");
        }
        virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
        {
+               bool assert2assume = false;
+               bool assume2assert = false;
+               bool live2fair = false;
+               bool fair2live = false;
+
                pool<IdString> constr_types;
                char mode = 0;
                int mode_arg;
@@ -103,6 +114,26 @@ struct ChformalPass : public Pass {
                                mode_arg = atoi(args[++argidx].c_str());
                                continue;
                        }
+                       if ((mode == 0 || mode == 'c') && args[argidx] == "-assert2assume") {
+                               assert2assume = true;
+                               mode = 'c';
+                               continue;
+                       }
+                       if ((mode == 0 || mode == 'c') && args[argidx] == "-assume2assert") {
+                               assume2assert = true;
+                               mode = 'c';
+                               continue;
+                       }
+                       if ((mode == 0 || mode == 'c') && args[argidx] == "-live2fair") {
+                               live2fair = true;
+                               mode = 'c';
+                               continue;
+                       }
+                       if ((mode == 0 || mode == 'c') && args[argidx] == "-fair2live") {
+                               fair2live = true;
+                               mode = 'c';
+                               continue;
+                       }
                        break;
                }
                extra_args(args, argidx, design);
@@ -231,6 +262,19 @@ struct ChformalPass : public Pass {
                                for (auto cell : constr_cells)
                                        cell->setPort("\\EN", module->LogicAnd(NEW_ID, en, cell->getPort("\\EN")));
                        }
+                       else
+                       if (mode == 'c')
+                       {
+                               for (auto cell : constr_cells)
+                                       if (assert2assume && cell->type == "$assert")
+                                               cell->type = "$assume";
+                                       else if (assume2assert && cell->type == "$assume")
+                                               cell->type = "$assert";
+                                       else if (live2fair && cell->type == "$live")
+                                               cell->type = "$fair";
+                                       else if (fair2live && cell->type == "$fair")
+                                               cell->type = "$live";
+                       }
                }
        }
 } ChformalPass;