From: Miodrag Milanovic <mmicko@gmail.com>
Date: Wed, 26 Aug 2020 08:39:57 +0000 (+0200)
Subject: Add formal apps and template generators
X-Git-Tag: working-ls180~301^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=fe8226a22d6f4030a525a6792a6188817571718b;p=yosys.git

Add formal apps and template generators
---

diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index 632dc51fd..52047ae2b 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -54,7 +54,7 @@ USING_YOSYS_NAMESPACE
 #  error "Only Symbiotic EDA flavored Verific is supported. Please contact office@symbioticeda.com for commercial support for Yosys+Verific."
 #endif
 
-#if SYMBIOTIC_VERIFIC_API_VERSION < 202006
+#if SYMBIOTIC_VERIFIC_API_VERSION < 20200702
 #  error "Please update your version of Symbiotic EDA flavored Verific."
 #endif
 
@@ -2158,6 +2158,70 @@ struct VerificPass : public Pass {
 		log("    Dump the Verific netlist as a verilog file.\n");
 		log("\n");
 		log("\n");
+		log("    verific [-work <libname>] -pp [options] <filename> [<module>]..\n");
+		log("\n");
+		log("Pretty print design (or just module) to the specified file from the\n");
+		log("specified library. (default library when -work is not present: \"work\")\n");
+		log("\n");
+		log("Pretty print options:\n");
+		log("\n");
+		log("  -verilog\n");
+		log("    Save output for Verilog/SystemVerilog design modules (default).\n");
+		log("\n");
+		log("  -vhdl\n");
+		log("    Save output for VHDL design units.\n");
+		log("\n");
+		log("\n");
+		log("    verific -app <application>..\n");
+		log("\n");
+		log("Execute SEDA formal application on loaded Verilog files.\n");
+		log("\n");
+		log("Application options:\n");
+		log("\n");
+		log("    -blacklist <filename[:lineno]>\n");
+		log("        Do not run application on modules from files that match the filename\n");
+		log("        or filename and line number if provided in such format.\n");
+		log("        Parameter can also contain comma separated list of file locations.\n");
+		log("\n");
+		log("    -blfile <file>\n");
+		log("        Do not run application on locations specified in file, they can represent filename\n");
+		log("        or filename and location in file.\n");
+		log("\n");
+		log("Applications:\n");
+		log("\n");
+#ifdef YOSYS_ENABLE_VERIFIC
+		VerificFormalApplications vfa;
+		log("%s\n",vfa.GetHelp().c_str());
+#else
+		log("  WARNING: Applications only available in commercial build.\n");
+
+#endif
+		log("\n");
+		log("\n");
+		log("    verific -template <name> <top_module>..\n");
+		log("\n");
+		log("Generate template for specified top module of loaded design.\n");
+		log("\n");
+		log("Template options:\n");
+		log("\n");
+		log("  -out\n");
+		log("    Specifies output file for generated template, by default output is stdout\n");
+		log("\n");
+		log("  -chparam name value \n");
+		log("    Generate template using this parameter value. Otherwise default parameter\n");
+		log("    values will be used for templat generate functionality. This option\n");
+		log("    can be specified multiple times to override multiple parameters.\n");
+		log("    String values must be passed in double quotes (\").\n");
+		log("\n");
+		log("Templates:\n");
+		log("\n");
+#ifdef YOSYS_ENABLE_VERIFIC
+		VerificTemplateGenerator vfg;
+		log("%s\n",vfg.GetHelp().c_str());
+#else
+		log("  WARNING: Templates only available in commercial build.\n");
+		log("\n");
+#endif
 		log("Use Symbiotic EDA Suite if you need Yosys+Verifc.\n");
 		log("https://www.symbioticeda.com/seda-suite\n");
 		log("\n");
@@ -2202,6 +2266,9 @@ struct VerificPass : public Pass {
 			RuntimeFlags::SetVar("veri_preserve_assignments", 1);
 			RuntimeFlags::SetVar("vhdl_preserve_assignments", 1);
 
+			RuntimeFlags::SetVar("veri_preserve_comments",1);
+			//RuntimeFlags::SetVar("vhdl_preserve_comments",1);
+
 			// Workaround for VIPER #13851
 			RuntimeFlags::SetVar("veri_create_name_for_unnamed_gen_block", 1);
 
@@ -2399,6 +2466,161 @@ struct VerificPass : public Pass {
 			goto check_error;
 		}
 
+		if (args[argidx] == "-app" && argidx+1 < GetSize(args))
+		{
+			VerificFormalApplications vfa;
+			auto apps = vfa.GetApps();
+			std::string app = args[++argidx];
+			std::vector<std::string> blacklists;
+			if (apps.find(app) == apps.end())
+				log_cmd_error("Application '%s' does not exist.\n", app.c_str());
+
+			for (argidx++; argidx < GetSize(args); argidx++) {
+				if (args[argidx] == "-blacklist" && argidx+1 < GetSize(args)) {
+					std::string line = args[++argidx];
+					std::string p;
+					while (!(p = next_token(line, ",\t\r\n ")).empty())
+						blacklists.push_back(p);
+					continue;
+				}
+				if (args[argidx] == "-blfile" && argidx+1 < GetSize(args)) {
+					std::string fn = args[++argidx];
+					std::ifstream f(fn);
+					if (f.fail())
+						log_cmd_error("Can't open blacklist file '%s'!\n", fn.c_str());
+
+					std::string line,p;
+					while (std::getline(f, line)) {
+						while (!(p = next_token(line, ",\t\r\n ")).empty())
+							blacklists.push_back(p);
+					}
+					continue;
+				}
+				break;
+			}
+			if (argidx < GetSize(args))
+				cmd_error(args, argidx, "unknown option/parameter");
+			MapIter mi;
+			VeriModule *module ;
+			VeriLibrary *veri_lib = veri_file::GetLibrary(work.c_str(), 1);
+			log("Running formal application '%s'.\n", app.c_str());
+			FOREACH_VERILOG_MODULE_IN_LIBRARY(veri_lib, mi, module) {
+				vfa.Run(module,apps[app],blacklists);
+			}
+			goto check_error;
+		}
+
+		if (args[argidx] == "-pp" && argidx < GetSize(args))
+		{
+			const char* filename = nullptr;
+			const char* module = nullptr;
+			bool mode_vhdl = false;
+			for (argidx++; argidx < GetSize(args); argidx++) {
+				if (args[argidx] == "-vhdl") {
+					mode_vhdl = true;
+					continue;
+				}
+				if (args[argidx] == "-verilog") {
+					mode_vhdl = false;
+					continue;
+				}
+
+				if (args[argidx].compare(0, 1, "-") == 0) {
+					cmd_error(args, argidx, "unknown option");
+					goto check_error;
+				}
+
+				if (!filename) {
+					filename = args[argidx].c_str();
+					continue;
+				}
+				if (module)
+					log_cmd_error("Only one module can be specified.\n");
+				module = args[argidx].c_str();
+			}
+
+			if (argidx < GetSize(args))
+				cmd_error(args, argidx, "unknown option/parameter");
+
+			if (!filename)
+				log_cmd_error("Filname must be specified.\n");
+
+			if (mode_vhdl)
+				vhdl_file::PrettyPrint(filename, module, work.c_str());
+			else
+				veri_file::PrettyPrint(filename, module, work.c_str());
+			goto check_error;
+		}
+
+		if (args[argidx] == "-template" && argidx < GetSize(args))
+		{
+			if (!(argidx < GetSize(args)))
+				cmd_error(args, argidx, "No template type specified.\n");
+
+			VerificTemplateGenerator vfg;
+			auto gens = vfg.GetGenerators();
+			std::string app = args[++argidx];
+			if (gens.find(app) == gens.end())
+				log_cmd_error("Template generator '%s' does not exist.\n", app.c_str());
+			TemplateGenerator *generator = gens[app];
+			if (!(argidx < GetSize(args)))
+				cmd_error(args, argidx, "No top module specified.\n");
+			
+			std::string module = args[++argidx];
+			VeriLibrary* veri_lib = veri_file::GetLibrary(work.c_str(), 1);
+			VeriModule *veri_module = veri_lib ? veri_lib->GetModule(module.c_str(), 1) : nullptr;
+			if (!veri_module) {
+				log_error("Can't find module/unit '%s'.\n", module.c_str());
+			}
+
+			log("Template '%s' is running for module '%s'.\n", app.c_str(),module.c_str());
+
+			Map parameters(STRING_HASH);
+			const char *out_filename = nullptr;
+
+			for (argidx++; argidx < GetSize(args); argidx++) {
+				if (generator->checkParams(args, argidx))
+					continue;
+				if (args[argidx] == "-chparam"  && argidx+2 < GetSize(args)) {
+					const std::string &key = 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)
+						log_warning_noprefix("-chparam %s already specified: overwriting.\n", key.c_str());
+					continue;
+				}
+
+				if (args[argidx] == "-out" && argidx+1 < GetSize(args)) {
+					out_filename = args[++argidx].c_str();
+					continue;
+				}
+
+				break;
+			}
+			if (argidx < GetSize(args))
+				cmd_error(args, argidx, "unknown option/parameter");
+
+			const char *err = generator->validate();
+			if (err)
+				cmd_error(args, argidx, err);
+
+			std::string val = generator->generate(veri_module, &parameters);
+
+			FILE *of = stdout;
+			if (out_filename) {
+				of = fopen(out_filename, "w");
+				if (of == nullptr)
+					log_error("Can't open '%s' for writing: %s\n", out_filename, strerror(errno));
+				log("Writing output to '%s'\n",out_filename);
+			}
+			fprintf(of, "%s\n",val.c_str());
+			fflush(of);
+			if (of!=stdout)
+				fclose(of);
+			goto check_error;
+		}
+
 		if (GetSize(args) > argidx && args[argidx] == "-import")
 		{
 			std::set<Netlist*> nl_todo, nl_done;