Merge pull request #871 from YosysHQ/verific_import

Improve verific -chparam and add hierarchy -chparam

frontends/verific/verific.cc

@@ -46,7 +46,7 @@ USING_YOSYS_NAMESPACE
 #include "VeriModule.h"
 #include "VeriWrite.h"
 #include "VhdlUnits.h"
-#include "Message.h"
+#include "VeriLibrary.h"
 
 #ifdef __clang__
 #pragma clang diagnostic pop
@@ -776,13 +776,14 @@ void VerificImporter::merge_past_ffs(pool<RTLIL::Cell*> &candidates)
 
 void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::set<Netlist*> &nl_todo)
 {
-	std::string module_name = nl->IsOperator() ? std::string("$verific$") + nl->Owner()->Name() : RTLIL::escape_id(nl->Owner()->Name());
+	std::string netlist_name = nl->GetAtt(" \\top") ? nl->CellBaseName() : nl->Owner()->Name();
+	std::string module_name = nl->IsOperator() ? "$verific$" + netlist_name : RTLIL::escape_id(netlist_name);
 
 	netlist = nl;
 
 	if (design->has(module_name)) {
 		if (!nl->IsOperator() && !is_blackbox(nl))
-			log_cmd_error("Re-definition of module `%s'.\n", nl->Owner()->Name());
+			log_cmd_error("Re-definition of module `%s'.\n", netlist_name.c_str());
 		return;
 	}
 
@@ -1752,32 +1753,64 @@ struct VerificExtNets
 	}
 };
 
-void verific_import(Design *design, std::string top)
+void verific_import(Design *design, const std::map<std::string,std::string> &parameters, std::string top)
 {
 	verific_sva_fsm_limit = 16;
 
 	std::set<Netlist*> nl_todo, nl_done;
 
-	{
+	VhdlLibrary *vhdl_lib = vhdl_file::GetLibrary("work", 1);
-		VhdlLibrary *vhdl_lib = vhdl_file::GetLibrary("work", 1);
+	VeriLibrary *veri_lib = veri_file::GetLibrary("work", 1);
-		VeriLibrary *veri_lib = veri_file::GetLibrary("work", 1);
+	Array *netlists = NULL;
+	Array veri_libs, vhdl_libs;
+	if (vhdl_lib) vhdl_libs.InsertLast(vhdl_lib);
+	if (veri_lib) veri_libs.InsertLast(veri_lib);
 
-		Array veri_libs, vhdl_libs;
+	Map verific_params(STRING_HASH);
-		if (vhdl_lib) vhdl_libs.InsertLast(vhdl_lib);
+	for (const auto &i : parameters)
-		if (veri_lib) veri_libs.InsertLast(veri_lib);
+		verific_params.Insert(i.first.c_str(), i.second.c_str());
 
-		Array *netlists = hier_tree::ElaborateAll(&veri_libs, &vhdl_libs);
+	if (top.empty()) {
-		Netlist *nl;
+		netlists = hier_tree::ElaborateAll(&veri_libs, &vhdl_libs, &verific_params);
-		int i;
+	}
+	else {
+		Array veri_modules, vhdl_units;
 
-		FOREACH_ARRAY_ITEM(netlists, i, nl) {
+		if (veri_lib) {
-			if (top.empty() || nl->Owner()->Name() == top)
+			VeriModule *veri_module = veri_lib->GetModule(top.c_str(), 1);
-				nl_todo.insert(nl);
+			if (veri_module) {
+				veri_modules.InsertLast(veri_module);
+			}
+
+			// Also elaborate all root modules since they may contain bind statements
+			MapIter mi;
+			FOREACH_VERILOG_MODULE_IN_LIBRARY(veri_lib, mi, veri_module) {
+				if (!veri_module->IsRootModule()) continue;
+				veri_modules.InsertLast(veri_module);
+			}
 		}
 
-		delete netlists;
+		if (vhdl_lib) {
+			VhdlDesignUnit *vhdl_unit = vhdl_lib->GetPrimUnit(top.c_str());
+			if (vhdl_unit)
+				vhdl_units.InsertLast(vhdl_unit);
+		}
+
+		netlists = hier_tree::Elaborate(&veri_modules, &vhdl_units, &verific_params);
 	}
 
+	Netlist *nl;
+	int i;
+
+	FOREACH_ARRAY_ITEM(netlists, i, nl) {
+		if (top.empty() && nl->CellBaseName() != top)
+			continue;
+		nl->AddAtt(new Att(" \\top", NULL));
+		nl_todo.insert(nl);
+	}
+
+	delete netlists;
+
 	if (!verific_error_msg.empty())
 		log_error("%s\n", verific_error_msg.c_str());
 
@@ -2212,8 +2245,8 @@ struct VerificPass : public Pass {
 					continue;
 				}
 				if (args[argidx] == "-chparam"  && argidx+2 < GetSize(args)) {
-                                        const std::string &key = args[++argidx];
+					const std::string &key = args[++argidx];
-                                        const std::string &value = args[++argidx];
+					const std::string &value = args[++argidx];
 					unsigned new_insertion = parameters.Insert(key.c_str(), value.c_str(),
 									           1 /* force_overwrite */);
 					if (!new_insertion)
@@ -2270,12 +2303,22 @@ struct VerificPass : public Pass {
 				for (; argidx < GetSize(args); argidx++)
 				{
 					const char *name = args[argidx].c_str();
+					VeriLibrary* veri_lib = veri_file::GetLibrary(work.c_str(), 1);
 
-					VeriModule *veri_module = veri_file::GetModule(name);
+					if (veri_lib) {
-					if (veri_module) {
+						VeriModule *veri_module = veri_lib->GetModule(name, 1);
-						log("Adding Verilog module '%s' to elaboration queue.\n", name);
+						if (veri_module) {
-						veri_modules.InsertLast(veri_module);
+							log("Adding Verilog module '%s' to elaboration queue.\n", name);
-						continue;
+							veri_modules.InsertLast(veri_module);
+							continue;
+						}
+
+						// Also elaborate all root modules since they may contain bind statements
+						MapIter mi;
+						FOREACH_VERILOG_MODULE_IN_LIBRARY(veri_lib, mi, veri_module) {
+							if (!veri_module->IsRootModule()) continue;
+							veri_modules.InsertLast(veri_module);
+						}
 					}
 
 					VhdlLibrary *vhdl_lib = vhdl_file::GetLibrary(work.c_str(), 1);
@@ -2294,8 +2337,10 @@ struct VerificPass : public Pass {
 				Netlist *nl;
 				int i;
 
-				FOREACH_ARRAY_ITEM(netlists, i, nl)
+				FOREACH_ARRAY_ITEM(netlists, i, nl) {
+					nl->AddAtt(new Att(" \\top", NULL));
 					nl_todo.insert(nl);
+				}
 				delete netlists;
 			}
 

frontends/verific/verific.h

@@ -26,7 +26,7 @@ YOSYS_NAMESPACE_BEGIN
 extern int verific_verbose;
 
 extern bool verific_import_pending;
-extern void verific_import(Design *design, std::string top = std::string());
+extern void verific_import(Design *design, const std::map<std::string,std::string> &parameters, std::string top = std::string());
 
 extern pool<int> verific_sva_prims;
 

passes/hierarchy/hierarchy.cc

@@ -570,7 +570,7 @@ struct HierarchyPass : public Pass {
 		log("\n");
 		log("    -simcheck\n");
 		log("        like -check, but also throw an error if blackbox modules are\n");
-		log("        instantiated, and throw an error if the design has no top module\n");
+		log("        instantiated, and throw an error if the design has no top module.\n");
 		log("\n");
 		log("    -purge_lib\n");
 		log("        by default the hierarchy command will not remove library (blackbox)\n");
@@ -583,20 +583,20 @@ struct HierarchyPass : public Pass {
 		log("\n");
 		log("    -keep_positionals\n");
 		log("        per default this pass also converts positional arguments in cells\n");
-		log("        to arguments using port names. this option disables this behavior.\n");
+		log("        to arguments using port names. This option disables this behavior.\n");
 		log("\n");
 		log("    -keep_portwidths\n");
 		log("        per default this pass adjusts the port width on cells that are\n");
-		log("        module instances when the width does not match the module port. this\n");
+		log("        module instances when the width does not match the module port. This\n");
 		log("        option disables this behavior.\n");
 		log("\n");
 		log("    -nokeep_asserts\n");
 		log("        per default this pass sets the \"keep\" attribute on all modules\n");
-		log("        that directly or indirectly contain one or more $assert cells. this\n");
+		log("        that directly or indirectly contain one or more formal properties.\n");
-		log("        option disables this behavior.\n");
+		log("        This option disables this behavior.\n");
 		log("\n");
 		log("    -top <module>\n");
-		log("        use the specified top module to built a design hierarchy. modules\n");
+		log("        use the specified top module to build the design hierarchy. Modules\n");
 		log("        outside this tree (unused modules) are removed.\n");
 		log("\n");
 		log("        when the -top option is used, the 'top' attribute will be set on the\n");
@@ -606,6 +606,12 @@ struct HierarchyPass : public Pass {
 		log("    -auto-top\n");
 		log("        automatically determine the top of the design hierarchy and mark it.\n");
 		log("\n");
+		log("    -chparam name value \n");
+		log("       elaborate the top module using this parameter value. Modules on which\n");
+		log("       this parameter does not exist may cause a warning message to be output.\n");
+		log("       This option can be specified multiple times to override multiple\n");
+		log("       parameters. String values must be passed in double quotes (\").\n");
+		log("\n");
 		log("In -generate mode this pass generates blackbox modules for the given cell\n");
 		log("types (wildcards supported). For this the design is searched for cells that\n");
 		log("match the given types and then the given port declarations are used to\n");
@@ -641,6 +647,7 @@ struct HierarchyPass : public Pass {
 		bool nokeep_asserts = false;
 		std::vector<std::string> generate_cells;
 		std::vector<generate_port_decl_t> generate_ports;
+		std::map<std::string, std::string> parameters;
 
 		size_t argidx;
 		for (argidx = 1; argidx < args.size(); argidx++)
@@ -715,28 +722,61 @@ struct HierarchyPass : public Pass {
 			if (args[argidx] == "-top") {
 				if (++argidx >= args.size())
 					log_cmd_error("Option -top requires an additional argument!\n");
-				top_mod = design->modules_.count(RTLIL::escape_id(args[argidx])) ? design->modules_.at(RTLIL::escape_id(args[argidx])) : NULL;
+				load_top_mod = args[argidx];
-				if (top_mod == NULL && design->modules_.count("$abstract" + RTLIL::escape_id(args[argidx]))) {
-					dict<RTLIL::IdString, RTLIL::Const> empty_parameters;
-					design->modules_.at("$abstract" + RTLIL::escape_id(args[argidx]))->derive(design, empty_parameters);
-					top_mod = design->modules_.count(RTLIL::escape_id(args[argidx])) ? design->modules_.at(RTLIL::escape_id(args[argidx])) : NULL;
-				}
-				if (top_mod == NULL)
-					load_top_mod = args[argidx];
 				continue;
 			}
 			if (args[argidx] == "-auto-top") {
 				auto_top_mode = true;
 				continue;
 			}
+			if (args[argidx] == "-chparam"  && argidx+2 < args.size()) {
+				const std::string &key = args[++argidx];
+				const std::string &value = args[++argidx];
+				auto r = parameters.emplace(key, value);
+				if (!r.second) {
+					log_warning("-chparam %s already specified: overwriting.\n", key.c_str());
+					r.first->second = value;
+				}
+				continue;
+			}
 			break;
 		}
 		extra_args(args, argidx, design, false);
 
-		if (!load_top_mod.empty()) {
+		if (!load_top_mod.empty())
+		{
+			IdString top_name = RTLIL::escape_id(load_top_mod);
+			IdString abstract_id = "$abstract" + RTLIL::escape_id(load_top_mod);
+			top_mod = design->module(top_name);
+
+			dict<RTLIL::IdString, RTLIL::Const> top_parameters;
+			for (auto &para : parameters) {
+				SigSpec sig_value;
+				if (!RTLIL::SigSpec::parse(sig_value, NULL, para.second))
+					log_cmd_error("Can't decode value '%s'!\n", para.second.c_str());
+				top_parameters[RTLIL::escape_id(para.first)] = sig_value.as_const();
+			}
+
+			if (top_mod == nullptr && design->module(abstract_id))
+				top_mod = design->module(design->module(abstract_id)->derive(design, top_parameters));
+			else if (top_mod != nullptr && !top_parameters.empty())
+				top_mod = design->module(top_mod->derive(design, top_parameters));
+
+			if (top_mod != nullptr && top_mod->name != top_name) {
+				Module *m = top_mod->clone();
+				m->name = top_name;
+				Module *old_mod = design->module(top_name);
+				if (old_mod)
+					design->remove(old_mod);
+				design->add(m);
+				top_mod = m;
+			}
+		}
+
+		if (top_mod == nullptr && !load_top_mod.empty()) {
 #ifdef YOSYS_ENABLE_VERIFIC
 			if (verific_import_pending) {
-				verific_import(design, load_top_mod);
+				verific_import(design, parameters, load_top_mod);
 				top_mod = design->module(RTLIL::escape_id(load_top_mod));
 			}
 #endif
@@ -745,7 +785,7 @@ struct HierarchyPass : public Pass {
 		} else {
 #ifdef YOSYS_ENABLE_VERIFIC
 			if (verific_import_pending)
-				verific_import(design);
+				verific_import(design, parameters);
 #endif
 		}
 
@@ -846,7 +886,7 @@ struct HierarchyPass : public Pass {
 			std::map<RTLIL::Module*, bool> cache;
 			for (auto mod : design->modules())
 				if (set_keep_assert(cache, mod)) {
-					log("Module %s directly or indirectly contains $assert cells -> setting \"keep\" attribute.\n", log_id(mod));
+					log("Module %s directly or indirectly contains formal properties -> setting \"keep\" attribute.\n", log_id(mod));
 					mod->set_bool_attribute("\\keep");
 				}
 		}

tests/various/chparam.sh

@@ -0,0 +1,52 @@
+#!/bin/bash
+
+trap 'echo "ERROR in chparam.sh" >&2; exit 1' ERR
+
+cat > chparam1.sv << "EOT"
+module top #(
+        parameter [31:0] X = 0
+) (
+        input [31:0] din,
+        output [31:0] dout
+);
+        assign dout = X-din;
+endmodule
+
+module top_props #(
+        parameter [31:0] X = 0
+) (
+        input [31:0] dout
+);
+        always @* assert (dout != X);
+endmodule
+
+bind top top_props #(.X(123456789)) props (.*);
+EOT
+
+cat > chparam2.sv << "EOT"
+module top #(
+	parameter [31:0] X = 0
+) (
+	input [31:0] din,
+	output [31:0] dout
+);
+	assign dout = X-din;
+	always @* assert (dout != 123456789);
+endmodule
+EOT
+
+if ../../yosys -q -p 'verific -sv chparam1.sv'; then
+	../../yosys -q -p 'verific -sv chparam1.sv; hierarchy -chparam X 123123123 -top top; prep -flatten' \
+			-p 'sat -verify -prove-asserts -show-ports -set din[0] 1' \
+			-p 'sat -falsify -prove-asserts -show-ports -set din[0] 0'
+
+	../../yosys -q -p 'verific -sv chparam2.sv; hierarchy -chparam X 123123123 -top top; prep -flatten' \
+			-p 'sat -verify -prove-asserts -show-ports -set din[0] 1' \
+			-p 'sat -falsify -prove-asserts -show-ports -set din[0] 0'
+fi
+../../yosys -q -p 'read_verilog -sv chparam2.sv; hierarchy -chparam X 123123123 -top top; prep -flatten' \
+		-p 'sat -verify -prove-asserts -show-ports -set din[0] 1' \
+		-p 'sat -falsify -prove-asserts -show-ports -set din[0] 0'
+
+rm chparam1.sv
+rm chparam2.sv