Merge branch 'eddie/clkpart' into xaig_dff

3 files changed, 48 insertions, 13 deletions

diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index a5c4aa26a..843e7b9b4 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -130,7 +130,7 @@ RTLIL::SigBit VerificImporter::net_map_at(Net *net)
 
 bool is_blackbox(Netlist *nl)
 {
-	if (nl->IsBlackBox())
+	if (nl->IsBlackBox() || nl->IsEmptyBox())
 		return true;
 
 	const char *attr = nl->GetAttValue("blackbox");
@@ -784,15 +784,15 @@ void VerificImporter::merge_past_ffs(pool<RTLIL::Cell*> &candidates)
 		merge_past_ffs_clock(it.second, it.first.first, it.first.second);
 }
 
-void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::set<Netlist*> &nl_todo)
+void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::set<Netlist*> &nl_todo, bool norename)
 {
 	std::string netlist_name = nl->GetAtt(" \\top") ? nl->CellBaseName() : nl->Owner()->Name();
 	std::string module_name = netlist_name;
 
-	if (nl->IsOperator()) {
+	if (nl->IsOperator() || nl->IsPrimitive()) {
 		module_name = "$verific$" + module_name;
 	} else {
-		if (*nl->Name()) {
+		if (!norename && *nl->Name()) {
 			module_name += "(";
 			module_name += nl->Name();
 			module_name += ")";
@@ -1409,7 +1409,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
 
 		std::string inst_type = inst->View()->Owner()->Name();
 
-		if (inst->View()->IsOperator()) {
+		if (inst->View()->IsOperator() || inst->View()->IsPrimitive()) {
 			inst_type = "$verific$" + inst_type;
 		} else {
 			if (*inst->View()->Name()) {
@@ -1899,7 +1899,7 @@ void verific_import(Design *design, const std::map<std::string,std::string> &par
 		Netlist *nl = *nl_todo.begin();
 		if (nl_done.count(nl) == 0) {
 			VerificImporter importer(false, false, false, false, false, false, false);
-			importer.import_netlist(design, nl, nl_todo);
+			importer.import_netlist(design, nl, nl_todo, nl->Owner()->Name() == top);
 		}
 		nl_todo.erase(nl);
 		nl_done.insert(nl);
@@ -2373,6 +2373,8 @@ struct VerificPass : public Pass {
 			if (argidx > GetSize(args) && args[argidx].compare(0, 1, "-") == 0)
 				cmd_error(args, argidx, "unknown option");
 
+			std::set<std::string> top_mod_names;
+
 			if (mode_all)
 			{
 				log("Running hier_tree::ElaborateAll().\n");
@@ -2401,6 +2403,7 @@ struct VerificPass : public Pass {
 				for (; argidx < GetSize(args); argidx++)
 				{
 					const char *name = args[argidx].c_str();
+					top_mod_names.insert(name);
 					VeriLibrary* veri_lib = veri_file::GetLibrary(work.c_str(), 1);
 
 					if (veri_lib) {
@@ -2466,7 +2469,7 @@ struct VerificPass : public Pass {
 				if (nl_done.count(nl) == 0) {
 					VerificImporter importer(mode_gates, mode_keep, mode_nosva,
 							mode_names, mode_verific, mode_autocover, mode_fullinit);
-					importer.import_netlist(design, nl, nl_todo);
+					importer.import_netlist(design, nl, nl_todo, top_mod_names.count(nl->Owner()->Name()));
 				}
 				nl_todo.erase(nl);
 				nl_done.insert(nl);
diff --git a/frontends/verific/verific.h b/frontends/verific/verific.h
index 5cbd78f7b..2ccfcd42c 100644
--- a/frontends/verific/verific.h
+++ b/frontends/verific/verific.h
@@ -93,7 +93,7 @@ struct VerificImporter
 	void merge_past_ffs_clock(pool<RTLIL::Cell*> &candidates, SigBit clock, bool clock_pol);
 	void merge_past_ffs(pool<RTLIL::Cell*> &candidates);
 
-	void import_netlist(RTLIL::Design *design, Verific::Netlist *nl, std::set<Verific::Netlist*> &nl_todo);
+	void import_netlist(RTLIL::Design *design, Verific::Netlist *nl, std::set<Verific::Netlist*> &nl_todo, bool norename = false);
 };
 
 void verific_import_sva_assert(VerificImporter *importer, Verific::Instance *inst);
diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc
index 909e9b4f1..49c0c40ac 100644
--- a/frontends/verific/verificsva.cc
+++ b/frontends/verific/verificsva.cc
@@ -36,6 +36,8 @@
 // basic_property:
 //   sequence
 //   not basic_property
+//   nexttime basic_property
+//   nexttime[N] basic_property
 //   sequence #-# basic_property
 //   sequence #=# basic_property
 //   basic_property or basic_property           (cover only)
@@ -1264,6 +1266,26 @@ struct VerificSvaImporter
 			return node;
 		}
 
+		if (inst->Type() == PRIM_SVA_NEXTTIME || inst->Type() == PRIM_SVA_S_NEXTTIME)
+		{
+			const char *sva_low_s = inst->GetAttValue("sva:low");
+			const char *sva_high_s = inst->GetAttValue("sva:high");
+
+			int sva_low = atoi(sva_low_s);
+			int sva_high = atoi(sva_high_s);
+			log_assert(sva_low == sva_high);
+
+			int node = start_node;
+
+			for (int i = 0; i < sva_low; i++) {
+				int next_node = fsm.createNode();
+				fsm.createEdge(node, next_node);
+				node = next_node;
+			}
+
+			return parse_sequence(fsm, node, inst->GetInput());
+		}
+
 		if (inst->Type() == PRIM_SVA_SEQ_CONCAT)
 		{
 			const char *sva_low_s = inst->GetAttValue("sva:low");
@@ -1590,15 +1612,25 @@ struct VerificSvaImporter
 			Instance *consequent_inst = net_to_ast_driver(consequent_net);
 
 			if (consequent_inst && (consequent_inst->Type() == PRIM_SVA_UNTIL || consequent_inst->Type() == PRIM_SVA_S_UNTIL ||
-					consequent_inst->Type() == PRIM_SVA_UNTIL_WITH || consequent_inst->Type() == PRIM_SVA_S_UNTIL_WITH))
+					consequent_inst->Type() == PRIM_SVA_UNTIL_WITH || consequent_inst->Type() == PRIM_SVA_S_UNTIL_WITH ||
+					consequent_inst->Type() == PRIM_SVA_ALWAYS || consequent_inst->Type() == PRIM_SVA_S_ALWAYS))
 			{
 				bool until_with = consequent_inst->Type() == PRIM_SVA_UNTIL_WITH || consequent_inst->Type() == PRIM_SVA_S_UNTIL_WITH;
 
-				Net *until_net = consequent_inst->GetInput2();
-				consequent_net = consequent_inst->GetInput1();
-				consequent_inst = net_to_ast_driver(consequent_net);
+				Net *until_net = nullptr;
+				if (consequent_inst->Type() == PRIM_SVA_ALWAYS || consequent_inst->Type() == PRIM_SVA_S_ALWAYS)
+				{
+					consequent_net = consequent_inst->GetInput();
+					consequent_inst = net_to_ast_driver(consequent_net);
+				}
+				else
+				{
+					until_net = consequent_inst->GetInput2();
+					consequent_net = consequent_inst->GetInput1();
+					consequent_inst = net_to_ast_driver(consequent_net);
+				}
 
-				SigBit until_sig = parse_expression(until_net);
+				SigBit until_sig = until_net ? parse_expression(until_net) : RTLIL::S0;
 				SigBit not_until_sig = module->Not(NEW_ID, until_sig);
 				antecedent_fsm.createEdge(node, node, not_until_sig);