5 files changed, 318 insertions, 31 deletions
diff --git a/frontends/ast/simplify.cc b/frontends/ast/simplify.cc
index 63212a9ed..57237f4b3 100644
--- a/frontends/ast/simplify.cc
+++ b/frontends/ast/simplify.cc
@@ -3696,6 +3696,8 @@ skip_dynamic_range_lvalue_expansion:;
 				goto apply_newNode;
 			}
 
+			if (current_scope.count(str) == 0)
+				str = try_pop_module_prefix();
 			if (current_scope.count(str) == 0 || current_scope[str]->type != AST_FUNCTION)
 				log_file_error(filename, location.first_line, "Can't resolve function name `%s'.\n", str.c_str());
 		}
@@ -3767,6 +3769,8 @@ skip_dynamic_range_lvalue_expansion:;
 				goto apply_newNode;
 			}
 
+			if (current_scope.count(str) == 0)
+				str = try_pop_module_prefix();
 			if (current_scope.count(str) == 0 || current_scope[str]->type != AST_TASK)
 				log_file_error(filename, location.first_line, "Can't resolve task name `%s'.\n", str.c_str());
 		}
diff --git a/frontends/blif/blifparse.cc b/frontends/blif/blifparse.cc
index 73d1f0ea7..ebbe082a2 100644
--- a/frontends/blif/blifparse.cc
+++ b/frontends/blif/blifparse.cc
@@ -21,6 +21,8 @@
 
 YOSYS_NAMESPACE_BEGIN
 
+const int lut_input_plane_limit = 12;
+
 static bool read_next_line(char *&buffer, size_t &buffer_size, int &line_count, std::istream &f)
 {
 	string strbuf;
@@ -513,6 +515,11 @@ void parse_blif(RTLIL::Design *design, std::istream &f, IdString dff_name, bool
 					sopmode = -1;
 					lastcell = sopcell;
 				}
+				else if (input_sig.size() > lut_input_plane_limit)
+				{
+					err_reason = stringf("names' input plane must have fewer than %d signals.", lut_input_plane_limit + 1);
+					goto error_with_reason;
+				}
 				else
 				{
 					RTLIL::Cell *cell = module->addCell(NEW_ID, ID($lut));
@@ -576,7 +583,7 @@ void parse_blif(RTLIL::Design *design, std::istream &f, IdString dff_name, bool
 
 		if (lutptr)
 		{
-			if (input_len > 12)
+			if (input_len > lut_input_plane_limit)
 				goto error;
 
 			for (int i = 0; i < (1 << input_len); i++) {
diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index 5eb4857c5..1e61b3a31 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -47,12 +47,22 @@ USING_YOSYS_NAMESPACE
 #include "VeriModule.h"
 #include "VeriWrite.h"
 #include "VeriLibrary.h"
+#include "VeriExpression.h"
 
 #ifdef VERIFIC_VHDL_SUPPORT
 #include "vhdl_file.h"
 #include "VhdlUnits.h"
 #endif
 
+#ifdef VERIFIC_EDIF_SUPPORT
+#include "edif_file.h"
+#endif
+
+#ifdef VERIFIC_LIBERTY_SUPPORT
+#include "synlib_file.h"
+#include "SynlibGroup.h"
+#endif
+
 #include "VerificStream.h"
 #include "FileSystem.h"
 
@@ -190,6 +200,36 @@ RTLIL::IdString VerificImporter::new_verific_id(Verific::DesignObj *obj)
 	return s;
 }
 
+static bool isNumber(const string& str)
+{
+	for (auto &c : str) {
+		if (std::isdigit(c) == 0) return false;
+	}
+	return true;
+}
+
+// When used as attributes or parameter values Verific constants come already processed.
+// - Real string values are already under quotes
+// - Numeric values with specified width are always converted to binary
+// - Rest of user defined values are handled as 32bit integers
+// - There could be some internal values that are strings without quotes
+//   so we check if value is all digits or not
+//
+static const RTLIL::Const verific_const(const char *value)
+{
+	std::string val = std::string(value);
+	if (val.size()>1 && val[0]=='\"' && val.back()=='\"')
+		return RTLIL::Const(val.substr(1,val.size()-2));
+	else
+		if (val.find("'b") != std::string::npos)
+			return RTLIL::Const::from_string(val.substr(val.find("'b") + 2));
+		else
+			if (isNumber(val))
+				return RTLIL::Const(std::stoi(val),32);
+			else
+				return RTLIL::Const(val);
+}
+
 void VerificImporter::import_attributes(dict<RTLIL::IdString, RTLIL::Const> &attributes, DesignObj *obj, Netlist *nl)
 {
 	MapIter mi;
@@ -198,14 +238,10 @@ void VerificImporter::import_attributes(dict<RTLIL::IdString, RTLIL::Const> &att
 	if (obj->Linefile())
 		attributes[ID::src] = stringf("%s:%d", LineFile::GetFileName(obj->Linefile()), LineFile::GetLineNo(obj->Linefile()));
 
-	// FIXME: Parse numeric attributes
 	FOREACH_ATTRIBUTE(obj, mi, attr) {
 		if (attr->Key()[0] == ' ' || attr->Value() == nullptr)
 			continue;
-		std::string val = std::string(attr->Value());
-		if (val.size()>1 && val[0]=='\"' && val.back()=='\"')
-			val = val.substr(1,val.size()-2);
-		attributes[RTLIL::escape_id(attr->Key())] = RTLIL::Const(val);
+		attributes[RTLIL::escape_id(attr->Key())] = verific_const(attr->Value());
 	}
 
 	if (nl) {
@@ -1176,6 +1212,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::ma
 			memory->name = RTLIL::escape_id(net->Name());
 			log_assert(module->count_id(memory->name) == 0);
 			module->memories[memory->name] = memory;
+			import_attributes(memory->attributes, net, nl);
 
 			int number_of_bits = net->Size();
 			int bits_in_word = number_of_bits;
@@ -2231,7 +2268,7 @@ struct VerificExtNets
 	}
 };
 
-void verific_import(Design *design, const std::map<std::string,std::string> &parameters, std::string top)
+std::string verific_import(Design *design, const std::map<std::string,std::string> &parameters, std::string top)
 {
 	verific_sva_fsm_limit = 16;
 
@@ -2264,6 +2301,18 @@ void verific_import(Design *design, const std::map<std::string,std::string> &par
 			VeriModule *veri_module = veri_lib->GetModule(top.c_str(), 1);
 			if (veri_module) {
 				veri_modules.InsertLast(veri_module);
+				if (veri_module->IsConfiguration()) {
+					VeriConfiguration *cfg = (VeriConfiguration*)veri_module;
+					VeriName *module_name = (VeriName*)cfg->GetTopModuleNames()->GetLast();
+					VeriLibrary *lib = veri_module->GetLibrary() ;
+					if (module_name && module_name->IsHierName()) {
+						VeriName *prefix = module_name->GetPrefix() ;
+						const char *lib_name = (prefix) ? prefix->GetName() : 0 ;
+						if (!Strings::compare("work", lib_name)) lib = veri_file::GetLibrary(lib_name, 1) ;
+					}
+					veri_module = (lib && module_name) ? lib->GetModule(module_name->GetName(), 1) : 0;
+					top = veri_module->GetName();
+				}
 			}
 
 			// Also elaborate all root modules since they may contain bind statements
@@ -2325,6 +2374,12 @@ void verific_import(Design *design, const std::map<std::string,std::string> &par
 #ifdef VERIFIC_VHDL_SUPPORT
 	vhdl_file::Reset();
 #endif
+#ifdef VERIFIC_EDIF_SUPPORT
+	edif_file::Reset();
+#endif
+#ifdef VERIFIC_LIBERTY_SUPPORT
+	synlib_file::Reset();
+#endif
 	Libset::Reset();
 	Message::Reset();
 	RuntimeFlags::DeleteAllFlags();
@@ -2336,6 +2391,7 @@ void verific_import(Design *design, const std::map<std::string,std::string> &par
 
 	if (!verific_error_msg.empty())
 		log_error("%s\n", verific_error_msg.c_str());
+	return top;
 }
 
 YOSYS_NAMESPACE_END
@@ -2386,6 +2442,25 @@ struct VerificPass : public Pass {
 		log("\n");
 		log("\n");
 #endif
+#ifdef VERIFIC_EDIF_SUPPORT
+		log("    verific {-edif} <edif-file>..\n");
+		log("\n");
+		log("Load the specified EDIF files into Verific.\n");
+		log("\n");
+		log("\n");
+#endif
+#ifdef VERIFIC_LIBERTY_SUPPORT
+		log("    verific {-liberty} <liberty-file>..\n");
+		log("\n");
+		log("Load the specified Liberty files into Verific.\n");
+		log("Default library when -work is not present is one specified in liberty file.\n");
+		log("To use from SystemVerilog or VHDL use -L to specify liberty library.");
+		log("\n");
+		log("    -lib\n");
+		log("        only create empty blackbox modules\n");
+		log("\n");
+		log("\n");
+#endif
 		log("    verific {-f|-F} [-vlog95|-vlog2k|-sv2005|-sv2009|\n");
 		log("                     -sv2012|-sv|-formal] <command-file>\n");
 		log("\n");
@@ -2466,10 +2541,10 @@ struct VerificPass : public Pass {
 		log("is printed, such as VERI-1209.\n");
 		log("\n");
 		log("\n");
-		log("    verific -import [options] <top-module>..\n");
+		log("    verific -import [options] <top>..\n");
 		log("\n");
-		log("Elaborate the design for the specified top modules, import to Yosys and\n");
-		log("reset the internal state of Verific.\n");
+		log("Elaborate the design for the specified top modules or configurations, import to\n");
+		log("Yosys and reset the internal state of Verific.\n");
 		log("\n");
 		log("Import options:\n");
 		log("\n");
@@ -2492,6 +2567,10 @@ struct VerificPass : public Pass {
 		log("  -fullinit\n");
 		log("    Keep all register initializations, even those for non-FF registers.\n");
 		log("\n");
+		log("  -cells\n");
+		log("    Import all cell definitions from Verific loaded libraries even if they are\n");
+		log("    unused in design. Useful with \"-edif\" and \"-liberty\" option.\n");
+		log("\n");
 		log("  -chparam name value \n");
 		log("    Elaborate the specified top modules (all modules when -all given) using\n");
 		log("    this parameter value. Modules on which this parameter does not exist will\n");
@@ -2561,6 +2640,45 @@ struct VerificPass : public Pass {
 		log("\n");
 	}
 #ifdef YOSYS_ENABLE_VERIFIC
+	std::string frontent_rewrite(std::vector<std::string> &args, int &argidx, std::vector<std::string> &tmp_files)
+	{
+		std::string filename = args[argidx++];
+		//Accommodate heredocs with EOT marker spaced out from "<<", e.g. "<< EOT" vs. "<<EOT"
+		if (filename == "<<" && (argidx < GetSize(args))) {
+			filename += args[argidx++];
+		}
+		if (filename.compare(0, 2, "<<") == 0) {
+			if (filename.size() <= 2)
+				log_error("Missing EOT marker in here document!\n");
+			std::string eot_marker = filename.substr(2);
+			if (Frontend::current_script_file == nullptr)
+				filename = "<stdin>";
+			std::string last_here_document;
+			while (1) {
+				std::string buffer;
+				char block[4096];
+				while (1) {
+					if (fgets(block, 4096, Frontend::current_script_file == nullptr? stdin : Frontend::current_script_file) == nullptr)
+						log_error("Unexpected end of file in here document '%s'!\n", filename.c_str());
+					buffer += block;
+					if (buffer.size() > 0 && (buffer[buffer.size() - 1] == '\n' || buffer[buffer.size() - 1] == '\r'))
+						break;
+				}
+				size_t indent = buffer.find_first_not_of(" \t\r\n");
+				if (indent != std::string::npos && buffer.compare(indent, eot_marker.size(), eot_marker) == 0)
+					break;
+				last_here_document += buffer;
+			}
+			filename = make_temp_file();
+			tmp_files.push_back(filename);
+			std::ofstream file(filename);
+			file << last_here_document;
+		} else {
+			rewrite_filename(filename);
+		}
+		return filename;
+	}
+
 	void execute(std::vector<std::string> args, RTLIL::Design *design) override
 	{
 		static bool set_verific_global_flags = true;
@@ -2633,6 +2751,7 @@ struct VerificPass : public Pass {
 		const char *release_str = Message::ReleaseString();
 		time_t release_time = Message::ReleaseDate();
 		char *release_tmstr = ctime(&release_time);
+		std::vector<std::string> tmp_files;
 
 		if (release_str == nullptr)
 			release_str = "(no release string)";
@@ -2644,6 +2763,7 @@ struct VerificPass : public Pass {
 
 		int argidx = 1;
 		std::string work = "work";
+		bool is_work_set = false;
 		veri_file::RegisterCallBackVerificStream(&verific_read_cb);
 
 		if (GetSize(args) > argidx && (args[argidx] == "-set-error" || args[argidx] == "-set-warning" ||
@@ -2710,10 +2830,25 @@ struct VerificPass : public Pass {
 		}
 
 		veri_file::RemoveAllLOptions();
+		veri_file::AddLOption("work");
+		for (int i = argidx; i < GetSize(args); i++)
+		{
+			if (args[i] == "-work" && i+1 < GetSize(args)) {
+				++i;
+				continue;
+			}
+			if (args[i] == "-L" && i+1 < GetSize(args)) {
+				if (args[++i] == "work")
+					veri_file::RemoveAllLOptions();
+				continue;
+			}
+			break;
+		}
 		for (; argidx < GetSize(args); argidx++)
 		{
 			if (args[argidx] == "-work" && argidx+1 < GetSize(args)) {
 				work = args[++argidx];
+				is_work_set = true;
 				continue;
 			}
 			if (args[argidx] == "-L" && argidx+1 < GetSize(args)) {
@@ -2830,8 +2965,7 @@ struct VerificPass : public Pass {
 				veri_file::AddLibExt(ext.c_str());
 
 			while (argidx < GetSize(args)) {
-				std::string filename(args[argidx++]);
-				rewrite_filename(filename);
+				std::string filename = frontent_rewrite(args, argidx, tmp_files);
 				file_names.Insert(strdup(filename.c_str()));
 			}
 			if (!veri_file::AnalyzeMultipleFiles(&file_names, verilog_mode, work.c_str(), veri_file::MFCU)) {
@@ -2846,9 +2980,9 @@ struct VerificPass : public Pass {
 #ifdef VERIFIC_VHDL_SUPPORT
 		if (GetSize(args) > argidx && args[argidx] == "-vhdl87") {
 			vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_1987").c_str());
-			for (argidx++; argidx < GetSize(args); argidx++) {
-				std::string filename(args[argidx]);
-				rewrite_filename(filename);
+			argidx++;
+			while (argidx < GetSize(args)) {
+				std::string filename = frontent_rewrite(args, argidx, tmp_files);
 				if (!vhdl_file::Analyze(filename.c_str(), work.c_str(), vhdl_file::VHDL_87))
 					log_cmd_error("Reading `%s' in VHDL_87 mode failed.\n", filename.c_str());
 			}
@@ -2858,9 +2992,9 @@ struct VerificPass : public Pass {
 
 		if (GetSize(args) > argidx && args[argidx] == "-vhdl93") {
 			vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_1993").c_str());
-			for (argidx++; argidx < GetSize(args); argidx++) {
-				std::string filename(args[argidx]);
-				rewrite_filename(filename);
+			argidx++;
+			while (argidx < GetSize(args)) {
+				std::string filename = frontent_rewrite(args, argidx, tmp_files);
 				if (!vhdl_file::Analyze(filename.c_str(), work.c_str(), vhdl_file::VHDL_93))
 					log_cmd_error("Reading `%s' in VHDL_93 mode failed.\n", filename.c_str());
 			}
@@ -2870,9 +3004,9 @@ struct VerificPass : public Pass {
 
 		if (GetSize(args) > argidx && args[argidx] == "-vhdl2k") {
 			vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_1993").c_str());
-			for (argidx++; argidx < GetSize(args); argidx++) {
-				std::string filename(args[argidx]);
-				rewrite_filename(filename);
+			argidx++;
+			while (argidx < GetSize(args)) {
+				std::string filename = frontent_rewrite(args, argidx, tmp_files);
 				if (!vhdl_file::Analyze(filename.c_str(), work.c_str(), vhdl_file::VHDL_2K))
 					log_cmd_error("Reading `%s' in VHDL_2K mode failed.\n", filename.c_str());
 			}
@@ -2882,9 +3016,9 @@ struct VerificPass : public Pass {
 
 		if (GetSize(args) > argidx && (args[argidx] == "-vhdl2008" || args[argidx] == "-vhdl")) {
 			vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_2008").c_str());
-			for (argidx++; argidx < GetSize(args); argidx++) {
-				std::string filename(args[argidx]);
-				rewrite_filename(filename);
+			argidx++;
+			while (argidx < GetSize(args)) {
+				std::string filename = frontent_rewrite(args, argidx, tmp_files);
 				if (!vhdl_file::Analyze(filename.c_str(), work.c_str(), vhdl_file::VHDL_2008))
 					log_cmd_error("Reading `%s' in VHDL_2008 mode failed.\n", filename.c_str());
 			}
@@ -2892,7 +3026,54 @@ struct VerificPass : public Pass {
 			goto check_error;
 		}
 #endif
+#ifdef VERIFIC_EDIF_SUPPORT
+		if (GetSize(args) > argidx && args[argidx] == "-edif") {
+			edif_file edif;
+			argidx++;
+			while (argidx < GetSize(args)) {
+				std::string filename = frontent_rewrite(args, argidx, tmp_files);
+				if (!edif.Read(filename.c_str()))
+					log_cmd_error("Reading `%s' in EDIF mode failed.\n", filename.c_str());
+			}
+			goto check_error;
+		}
+#endif
+#ifdef VERIFIC_LIBERTY_SUPPORT
+		if (GetSize(args) > argidx && args[argidx] == "-liberty") {
+			bool flag_lib = false;
+			for (argidx++; argidx < GetSize(args); argidx++) {
+				if (args[argidx] == "-lib") {
+					flag_lib = true;
+					continue;
+				}
+				if (args[argidx].compare(0, 1, "-") == 0) {
+					cmd_error(args, argidx, "unknown option");
+					goto check_error;
+				}
+				break;
+			}
 
+			while (argidx < GetSize(args)) {
+				std::string filename = frontent_rewrite(args, argidx, tmp_files);
+				if (!synlib_file::Read(filename.c_str(), is_work_set ? work.c_str() : nullptr))
+					log_cmd_error("Reading `%s' in LIBERTY mode failed.\n", filename.c_str());
+				SynlibLibrary *lib = synlib_file::GetLastLibraryAnalyzed();
+				if (lib && flag_lib) {
+					MapIter mi ;
+					Verific::Cell *c ;
+					FOREACH_CELL_OF_LIBRARY(lib->GetLibrary(),mi,c) {
+						MapIter ni ;
+						Netlist *nl;
+						FOREACH_NETLIST_OF_CELL(c, ni, nl) {
+							if (nl)
+								nl->MakeBlackBox();
+						}
+					}
+				}
+			}
+			goto check_error;
+		}
+#endif
 		if (argidx < GetSize(args) && args[argidx] == "-pp")
 		{
 			const char* filename = nullptr;
@@ -2947,7 +3128,7 @@ struct VerificPass : public Pass {
 			bool mode_all = false, mode_gates = false, mode_keep = false;
 			bool mode_nosva = false, mode_names = false, mode_verific = false;
 			bool mode_autocover = false, mode_fullinit = false;
-			bool flatten = false, extnets = false;
+			bool flatten = false, extnets = false, mode_cells = false;
 			string dumpfile;
 			string ppfile;
 			Map parameters(STRING_HASH);
@@ -2993,6 +3174,10 @@ struct VerificPass : public Pass {
 					mode_fullinit = true;
 					continue;
 				}
+				if (args[argidx] == "-cells") {
+					mode_cells = true;
+					continue;
+				}
 				if (args[argidx] == "-chparam"  && argidx+2 < GetSize(args)) {
 					const std::string &key = args[++argidx];
 					const std::string &value = args[++argidx];
@@ -3075,8 +3260,29 @@ struct VerificPass : public Pass {
 
 					VeriModule *veri_module = veri_lib ? veri_lib->GetModule(name, 1) : nullptr;
 					if (veri_module) {
-						log("Adding Verilog module '%s' to elaboration queue.\n", name);
-						veri_modules.InsertLast(veri_module);
+						if (veri_module->IsConfiguration()) {
+							log("Adding Verilog configuration '%s' to elaboration queue.\n", name);	
+							veri_modules.InsertLast(veri_module);
+
+							top_mod_names.erase(name);
+
+							VeriConfiguration *cfg = (VeriConfiguration*)veri_module;
+							VeriName *module_name;
+							int i;
+							FOREACH_ARRAY_ITEM(cfg->GetTopModuleNames(), i, module_name) {
+								VeriLibrary *lib = veri_module->GetLibrary() ;
+								if (module_name && module_name->IsHierName()) {
+									VeriName *prefix = module_name->GetPrefix() ;
+									const char *lib_name = (prefix) ? prefix->GetName() : 0 ;
+									if (!Strings::compare("work", lib_name)) lib = veri_file::GetLibrary(lib_name, 1) ;
+								}
+								veri_module = (lib && module_name) ? lib->GetModule(module_name->GetName(), 1) : 0;
+								top_mod_names.insert(veri_module->GetName());
+							}
+						} else {
+							log("Adding Verilog module '%s' to elaboration queue.\n", name);
+							veri_modules.InsertLast(veri_module);
+						}
 						continue;
 					}
 #ifdef VERIFIC_VHDL_SUPPORT
@@ -3113,6 +3319,28 @@ struct VerificPass : public Pass {
 				}
 				delete netlists;
 			}
+			if (mode_cells) {
+				log("Importing all cells.\n");
+				Libset *gls = Libset::Global() ;
+				MapIter it ;
+				Library *l ;
+				FOREACH_LIBRARY_OF_LIBSET(gls,it,l) {
+					MapIter mi ;
+					Verific::Cell *c ;
+					FOREACH_CELL_OF_LIBRARY(l,mi,c) {
+						if (!mode_verific && (l == Library::Primitives() || l == Library::Operators())) continue;
+						MapIter ni ;
+						if (c->NumOfNetlists() == 1) {
+							c->GetFirstNetlist()->SetName("");
+						}
+						Netlist *nl;
+						FOREACH_NETLIST_OF_CELL(c, ni, nl) {
+							if (nl)
+								nl_todo.emplace(nl->CellBaseName(), nl);
+						}
+					}
+				}
+			}
 
 			if (!verific_error_msg.empty())
 				goto check_error;
@@ -3156,6 +3384,12 @@ struct VerificPass : public Pass {
 #ifdef VERIFIC_VHDL_SUPPORT
 			vhdl_file::Reset();
 #endif
+#ifdef VERIFIC_EDIF_SUPPORT
+			edif_file::Reset();
+#endif
+#ifdef VERIFIC_LIBERTY_SUPPORT
+			synlib_file::Reset();
+#endif
 			Libset::Reset();
 			Message::Reset();
 			RuntimeFlags::DeleteAllFlags();
@@ -3236,6 +3470,13 @@ struct VerificPass : public Pass {
 		cmd_error(args, argidx, "Missing or unsupported mode parameter.\n");
 
 	check_error:
+		if (tmp_files.size()) {
+			log("Removing temp files.\n");
+			for(auto &fn : tmp_files) {
+				remove(fn.c_str());
+			}
+		}
+
 		if (!verific_error_msg.empty())
 			log_error("%s\n", verific_error_msg.c_str());
 
@@ -3275,6 +3516,21 @@ struct ReadPass : public Pass {
 		log("\n");
 		log("\n");
 #endif
+#ifdef VERIFIC_EDIF_SUPPORT
+		log("    read {-edif} <edif-file>..\n");
+		log("\n");
+		log("Load the specified EDIF files. (Requires Verific.)\n");
+		log("\n");
+		log("\n");
+#endif
+		log("    read {-liberty} <liberty-file>..\n");
+		log("\n");
+		log("Load the specified Liberty files.\n");
+		log("\n");
+		log("    -lib\n");
+		log("        only create empty blackbox modules\n");
+		log("\n");
+		log("\n");
 		log("    read {-f|-F} <command-file>\n");
 		log("\n");
 		log("Load and execute the specified command file. (Requires Verific.)\n");
@@ -3368,6 +3624,26 @@ struct ReadPass : public Pass {
 			return;
 		}
 #endif
+#ifdef VERIFIC_EDIF_SUPPORT
+		if (args[1] == "-edif") {
+			if (use_verific) {
+				args[0] = "verific";
+				Pass::call(design, args);
+			} else {
+				cmd_error(args, 1, "This version of Yosys is built without Verific support.\n");
+			}
+			return;
+		}
+#endif
+		if (args[1] == "-liberty") {
+			if (use_verific) {
+				args[0] = "verific";
+			} else {
+				args[0] = "read_liberty";
+			}
+			Pass::call(design, args);
+			return;
+		}
 		if (args[1] == "-f" || args[1] == "-F") {
 			if (use_verific) {
 				args[0] = "verific";
diff --git a/frontends/verific/verific.h b/frontends/verific/verific.h
index 695c04f3b..d9f0077db 100644
--- a/frontends/verific/verific.h
+++ b/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, const std::map<std::string,std::string> &parameters, std::string top = std::string());
+extern std::string verific_import(Design *design, const std::map<std::string,std::string> &parameters, std::string top = std::string());
 
 extern pool<int> verific_sva_prims;
 
diff --git a/frontends/verilog/verilog_parser.y b/frontends/verilog/verilog_parser.y
index c533b0c40..70ee47561 100644
--- a/frontends/verilog/verilog_parser.y
+++ b/frontends/verilog/verilog_parser.y
@@ -229,9 +229,9 @@ static AstNode *checkRange(AstNode *type_node, AstNode *range_node)
 static void rewriteRange(AstNode *rangeNode)
 {
 	if (rangeNode->type == AST_RANGE && rangeNode->children.size() == 1) {
-		// SV array size [n], rewrite as [n-1:0]
-		rangeNode->children[0] = new AstNode(AST_SUB, rangeNode->children[0], AstNode::mkconst_int(1, true));
-		rangeNode->children.push_back(AstNode::mkconst_int(0, false));
+		// SV array size [n], rewrite as [0:n-1]
+		rangeNode->children.push_back(new AstNode(AST_SUB, rangeNode->children[0], AstNode::mkconst_int(1, true)));
+		rangeNode->children[0] = AstNode::mkconst_int(0, false);
 	}
 }