Extend `add` command to allow adding cells for verification like $assert, $assume...

diff --git a/passes/cmds/add.cc b/passes/cmds/add.cc
index dd05ac81f3125ff2a0c5c6ffa3c1140d79e6bc2b..459b29f358e7969c297b74e6210872721b929e44 100644 (file)
--- a/passes/cmds/add.cc
+++ b/passes/cmds/add.cc
@@ -22,6 +22,42 @@
 USING_YOSYS_NAMESPACE
 PRIVATE_NAMESPACE_BEGIN
 
+static bool is_formal_celltype(const std::string &celltype)
+{
+       if(celltype == "assert" || celltype == "assume" || celltype == "live" || celltype == "fair" || celltype == "cover")
+               return true;
+       else
+               return false;
+}
+
+static void add_formal(RTLIL::Module *module, const std::string &celltype, const std::string &name, const std::string &enable_name)
+{
+       std::string escaped_name = RTLIL::escape_id(name);
+       std::string escaped_enable_name = (enable_name != "") ? RTLIL::escape_id(enable_name) : "";
+       RTLIL::Wire *wire = module->wire(escaped_name);
+       log_assert(is_formal_celltype(celltype));
+
+       if (wire == nullptr) {
+               log_error("Could not find wire with name \"%s\".\n", name.c_str());
+       }
+       else {
+               RTLIL::Cell *formal_cell = module->addCell(NEW_ID, "$" + celltype);
+               formal_cell->setPort(ID(A), wire);
+               if(enable_name == "") {
+                       formal_cell->setPort(ID(EN), State::S1);
+                       log("Added $%s cell for wire \"%s.%s\"\n", celltype.c_str(), module->name.str().c_str(), name.c_str());
+               }
+               else {
+                       RTLIL::Wire *enable_wire = module->wire(escaped_enable_name);
+                       if(enable_wire == nullptr)
+                               log_error("Could not find enable wire with name \"%s\".\n", enable_name.c_str());
+
+                       formal_cell->setPort(ID(EN), enable_wire);
+                       log("Added $%s cell for wire \"%s.%s\" enabled by wire \"%s.%s\".\n", celltype.c_str(), module->name.str().c_str(), name.c_str(), module->name.str().c_str(), enable_name.c_str());
+               }
+       }
+}
+
 static void add_wire(RTLIL::Design *design, RTLIL::Module *module, std::string name, int width, bool flag_input, bool flag_output, bool flag_global)
 {
        RTLIL::Wire *wire = NULL;
@@ -106,6 +142,12 @@ struct AddPass : public Pass {
                log("selected modules.\n");
                log("\n");
                log("\n");
+               log("    add {-assert|-assume|-live|-fair|-cover} <name1> [-if <name2>]\n");
+               log("\n");
+               log("Add an $assert, $assume, etc. cell connected to a wire named name1, with its\n");
+               log("enable signal optionally connected to a wire named name2 (default: 1'b1).\n");
+               log("\n");
+               log("\n");
                log("    add -mod <name[s]>\n");
                log("\n");
                log("Add module[s] with the specified name[s].\n");
@@ -115,6 +157,7 @@ struct AddPass : public Pass {
        {
                std::string command;
                std::string arg_name;
+               std::string enable_name = "";
                bool arg_flag_input = false;
                bool arg_flag_output = false;
                bool arg_flag_global = false;
@@ -144,6 +187,17 @@ struct AddPass : public Pass {
                                argidx++;
                                break;
                        }
+                       if (arg.length() > 0 && arg[0] == '-' && is_formal_celltype(arg.substr(1))) {
+                               if (argidx + 1 >= args.size())
+                                       break;
+                               command = arg.substr(1);
+                               arg_name = args[++argidx];
+                               if (argidx + 2 < args.size() && args[argidx + 1] == "-if") {
+                                       enable_name = args[argidx + 2];
+                                       argidx += 2;
+                               }
+                               continue;
+                       }
                        break;
                }
 
@@ -163,7 +217,9 @@ struct AddPass : public Pass {
                        if (module->get_bool_attribute("\\blackbox"))
                                continue;
 
-                       if (command == "wire")
+                       if (is_formal_celltype(command))
+                               add_formal(module, command, arg_name, enable_name);
+                       else if (command == "wire")
                                add_wire(design, module, arg_name, arg_width, arg_flag_input, arg_flag_output, arg_flag_global);
                }
        }