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

1 files changed, 57 insertions, 1 deletions

diff --git a/passes/cmds/add.cc b/passes/cmds/add.cc
index dd05ac81f..459b29f35 100644
--- 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);
 		}
 	}