Merge pull request #5389 from jix/sva_continue

verific: New `-sva-continue-on-error` import option

frontends/verific/verific.cc

@@ -200,8 +200,8 @@ YosysStreamCallBackHandler verific_read_cb;
 
 // ==================================================================
 
-VerificImporter::VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_names, bool mode_verific, bool mode_autocover, bool mode_fullinit) :
+VerificImporter::VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_sva_continue, bool mode_names, bool mode_verific, bool mode_autocover, bool mode_fullinit) :
-		mode_gates(mode_gates), mode_keep(mode_keep), mode_nosva(mode_nosva),
+		mode_gates(mode_gates), mode_keep(mode_keep), mode_nosva(mode_nosva), mode_sva_continue(mode_sva_continue),
 		mode_names(mode_names), mode_verific(mode_verific), mode_autocover(mode_autocover),
 		mode_fullinit(mode_fullinit)
 {
@@ -2316,6 +2316,12 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::ma
 				wire->attributes.erase(ID::init);
 		}
 	}
+
+	if (num_sva_continue) {
+		log_warning("Encountered %d items containing unsupported SVA!\n", num_sva_continue);
+		log_warning("Unsupported SVA imported as 'x and marked using the `unsupported_sva' attribute due to -sva-continue-on-err.\n");
+	}
+	num_sva_continue = 0;
 }
 
 // ==================================================================
@@ -3051,7 +3057,7 @@ std::string verific_import(Design *design, const std::map<std::string,std::strin
 		auto it = nl_todo.begin();
 		Netlist *nl = it->second;
 		if (nl_done.count(it->first) == 0) {
-			VerificImporter importer(false, false, false, false, false, false, false);
+			VerificImporter importer(false, false, false, false, false, false, false, false);
 			nl_done[it->first] = it->second;
 			importer.import_netlist(design, nl, nl_todo, top_mod_names.count(nl->CellBaseName()));
 		}
@@ -3288,6 +3294,11 @@ struct VerificPass : public Pass {
 		log("  -nosva\n");
 		log("    Ignore SVA properties, do not infer checker logic.\n");
 		log("\n");
+		log("  -sva-continue-on-err\n");
+		log("    Turns unsupported SVA from an error into a warning. Properties are imported\n");
+		log("    with their trigger condition replaced with 'x and with an `unsupported_sva'\n");
+		log("    attribute to produce a later error in SBY if they remain in the design.\n");
+		log("\n");
 		log("  -L <int>\n");
 		log("    Maximum number of ctrl bits for SVA checker FSMs (default=16).\n");
 		log("\n");
@@ -4033,7 +4044,8 @@ struct VerificPass : public Pass {
 		{
 			std::map<std::string,Netlist*> nl_todo, nl_done;
 			bool mode_all = false, mode_gates = false, mode_keep = false;
-			bool mode_nosva = false, mode_names = false, mode_verific = false;
+			bool mode_nosva = false, mode_sva_continue = false;
+			bool mode_names = false, mode_verific = false;
 			bool mode_autocover = false, mode_fullinit = false;
 			bool flatten = false, extnets = false, mode_cells = false;
 			bool split_complex_ports = true;
@@ -4071,6 +4083,10 @@ struct VerificPass : public Pass {
 					mode_nosva = true;
 					continue;
 				}
+				if (args[argidx] == "-sva-continue-on-err") {
+					mode_sva_continue = true;
+					continue;
+				}
 				if (args[argidx] == "-L" && argidx+1 < GetSize(args)) {
 					verific_sva_fsm_limit = atoi(args[++argidx].c_str());
 					continue;
@@ -4201,7 +4217,7 @@ struct VerificPass : public Pass {
 				auto it = nl_todo.begin();
 				Netlist *nl = it->second;
 				if (nl_done.count(it->first) == 0) {
-					VerificImporter importer(mode_gates, mode_keep, mode_nosva,
+					VerificImporter importer(mode_gates, mode_keep, mode_nosva, mode_sva_continue,
 							mode_names, mode_verific, mode_autocover, mode_fullinit);
 					nl_done[it->first] = it->second;
 					importer.import_netlist(design, nl, nl_todo, top_mod_names.count(nl->CellBaseName()));

frontends/verific/verific.h

@@ -73,10 +73,12 @@ struct VerificImporter
 	std::map<Verific::Net*, Verific::Net*> sva_posedge_map;
 	pool<Verific::Net*> any_all_nets;
 
-	bool mode_gates, mode_keep, mode_nosva, mode_names, mode_verific;
+	bool mode_gates, mode_keep, mode_nosva, mode_sva_continue, mode_names, mode_verific;
 	bool mode_autocover, mode_fullinit;
 
-	VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_names, bool mode_verific, bool mode_autocover, bool mode_fullinit);
+	int num_sva_continue = 0;
+
+	VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_sva_continue, bool mode_names, bool mode_verific, bool mode_autocover, bool mode_fullinit);
 
 	RTLIL::SigBit net_map_at(Verific::Net *net);
 

frontends/verific/verificsva.cc

@@ -124,6 +124,7 @@ struct SvaFsm
 {
 	Module *module;
 	VerificClocking clocking;
+	std::function<void (std::string)> parser_error;
 
 	SigBit trigger_sig = State::S1, disable_sig;
 	SigBit throughout_sig = State::S1;
@@ -148,6 +149,7 @@ struct SvaFsm
 		module = clking.module;
 		clocking = clking;
 		trigger_sig = trig;
+		parser_error = [](std::string msg){ log_error("%s", msg); };
 
 		startNode = createNode();
 		acceptNode = createNode();
@@ -475,8 +477,8 @@ struct SvaFsm
 				dump();
 				log("      ctrl signal: %s\n", log_signal(dnode.ctrl));
 			}
-			log_error("SVA DFSM state ctrl signal has %d (>%d) bits. Stopping to prevent exponential design size explosion.\n",
+			parser_error(stringf("SVA DFSM state ctrl signal has %d (>%d) bits. Stopping to prevent exponential design size explosion.\n",
-					GetSize(dnode.ctrl), verific_sva_fsm_limit);
+					GetSize(dnode.ctrl), verific_sva_fsm_limit));
 		}
 
 		for (unsigned long long i = 0; i < (1ull << GetSize(dnode.ctrl)); i++)
@@ -1023,7 +1025,7 @@ struct VerificSvaImporter
 
 	[[noreturn]] void parser_error(std::string errmsg)
 	{
-		if (!importer->mode_keep)
+		if (!importer->mode_keep && !importer->mode_sva_continue)
 			log_error("%s", errmsg);
 		log_warning("%s", errmsg);
 		throw ParserErrorException();
@@ -1260,6 +1262,7 @@ struct VerificSvaImporter
 		if (inst->Type() == PRIM_SVA_FIRST_MATCH)
 		{
 			SvaFsm match_fsm(clocking);
+			match_fsm.parser_error = [&](std::string msg) { this->parser_error(msg); };
 			match_fsm.createLink(parse_sequence(match_fsm, match_fsm.createStartNode(), inst->GetInput()), match_fsm.acceptNode);
 
 			int node = fsm.createNode();
@@ -1426,12 +1429,15 @@ struct VerificSvaImporter
 		if (inst->Type() == PRIM_SVA_SEQ_AND || inst->Type() == PRIM_SVA_AND)
 		{
 			SvaFsm fsm1(clocking);
+			fsm1.parser_error = [&](std::string msg) { this->parser_error(msg); };
 			fsm1.createLink(parse_sequence(fsm1, fsm1.createStartNode(), inst->GetInput1()), fsm1.acceptNode);
 
 			SvaFsm fsm2(clocking);
+			fsm2.parser_error = [&](std::string msg) { this->parser_error(msg); };
 			fsm2.createLink(parse_sequence(fsm2, fsm2.createStartNode(), inst->GetInput2()), fsm2.acceptNode);
 
 			SvaFsm combined_fsm(clocking);
+			combined_fsm.parser_error = [&](std::string msg) { this->parser_error(msg); };
 			fsm1.getDFsm(combined_fsm, combined_fsm.createStartNode(), -1, combined_fsm.acceptNode);
 			fsm2.getDFsm(combined_fsm, combined_fsm.createStartNode(), -1, combined_fsm.acceptNode);
 
@@ -1456,6 +1462,7 @@ struct VerificSvaImporter
 		if (inst->Type() == PRIM_SVA_INTERSECT || inst->Type() == PRIM_SVA_WITHIN)
 		{
 			SvaFsm intersect_fsm(clocking);
+			intersect_fsm.parser_error = [&](std::string msg) { this->parser_error(msg); };
 
 			if (inst->Type() == PRIM_SVA_INTERSECT)
 			{
@@ -1562,6 +1569,7 @@ struct VerificSvaImporter
 			int node;
 
 			SvaFsm antecedent_fsm(clocking, trig);
+			antecedent_fsm.parser_error = [&](std::string msg) { this->parser_error(msg); };
 			node = parse_sequence(antecedent_fsm, antecedent_fsm.createStartNode(), antecedent_net);
 			if (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION) {
 				int next_node = antecedent_fsm.createNode();
@@ -1623,6 +1631,7 @@ struct VerificSvaImporter
 			int node;
 
 			SvaFsm antecedent_fsm(clocking, trig);
+			antecedent_fsm.parser_error = [&](std::string msg) { this->parser_error(msg); };
 			node = parse_sequence(antecedent_fsm, antecedent_fsm.createStartNode(), antecedent_net);
 			if (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION || inst->Type() == PRIM_SVA_NON_OVERLAPPED_FOLLOWED_BY) {
 				int next_node = antecedent_fsm.createNode();
@@ -1677,6 +1686,7 @@ struct VerificSvaImporter
 			}
 
 			SvaFsm consequent_fsm(clocking, antecedent_match);
+			consequent_fsm.parser_error = [&](std::string msg) { this->parser_error(msg); };
 			node = parse_sequence(consequent_fsm, consequent_fsm.createStartNode(), consequent_net);
 			consequent_fsm.createLink(node, consequent_fsm.acceptNode);
 
@@ -1696,6 +1706,7 @@ struct VerificSvaImporter
 			}
 
 			SvaFsm fsm(clocking, trig);
+			fsm.parser_error = [&](std::string msg) { this->parser_error(msg); };
 			int node = parse_sequence(fsm, fsm.createStartNode(), net);
 			fsm.createLink(node, fsm.acceptNode);
 
@@ -1710,30 +1721,34 @@ struct VerificSvaImporter
 
 	void import()
 	{
-		try
+		module = importer->module;
-		{
+		netlist = root->Owner();
-			module = importer->module;
-			netlist = root->Owner();
 
-			if (verific_verbose)
+		int initial_cell_count = GetSize(module->cells_);
-				log("  importing SVA property at root cell %s (%s) at %s:%d.\n", root->Name(), root->View()->Owner()->Name(),
+		int initial_wire_count = GetSize(module->wires_);
-						LineFile::GetFileName(root->Linefile()), LineFile::GetLineNo(root->Linefile()));
+		int initial_connection_count = GetSize(module->connections_);
 
-			bool is_user_declared = root->IsUserDeclared();
+		if (verific_verbose)
+			log("  importing SVA property at root cell %s (%s) at %s:%d.\n", root->Name(), root->View()->Owner()->Name(),
+					LineFile::GetFileName(root->Linefile()), LineFile::GetLineNo(root->Linefile()));
 
-			// FIXME
+		bool is_user_declared = root->IsUserDeclared();
-			if (!is_user_declared) {
+
-				const char *name = root->Name();
+		// FIXME
-				for (int i = 0; name[i]; i++) {
+		if (!is_user_declared) {
-					if (i ? (name[i] < '0' || name[i] > '9') : (name[i] != 'i')) {
+			const char *name = root->Name();
-						is_user_declared = true;
+			for (int i = 0; name[i]; i++) {
-						break;
+				if (i ? (name[i] < '0' || name[i] > '9') : (name[i] != 'i')) {
-					}
+					is_user_declared = true;
+					break;
 				}
 			}
+		}
 
-			RTLIL::IdString root_name = module->uniquify(importer->mode_names || is_user_declared ? RTLIL::escape_id(root->Name()) : NEW_ID);
+		RTLIL::IdString root_name = module->uniquify(importer->mode_names || is_user_declared ? RTLIL::escape_id(root->Name()) : NEW_ID);
 
+		try
+		{
 			// parse SVA sequence into trigger signal
 
 			clocking = VerificClocking(importer, root->GetInput(), true);
@@ -1836,6 +1851,36 @@ struct VerificSvaImporter
 		}
 		catch (ParserErrorException)
 		{
+			if (importer->mode_sva_continue) {
+
+				std::vector<Cell *> remove_cells;
+				pool<Wire *> remove_wires;
+
+				for (int i = 0, end = GetSize(module->cells_) - initial_cell_count; i != end; ++i)
+					remove_cells.push_back(module->cells_.element(i)->second);
+
+				for (int i = 0, end = GetSize(module->wires_) - initial_wire_count; i != end; ++i)
+					remove_wires.emplace(module->wires_.element(i)->second);
+
+				for (auto cell : remove_cells)
+					module->remove(cell);
+				module->remove(remove_wires);
+
+				module->connections_.resize(initial_connection_count);
+
+				RTLIL::Cell *c = nullptr;
+
+				if (mode_assert) c = module->addAssert(root_name, State::Sx, State::Sx);
+				if (mode_assume) c = module->addAssume(root_name, State::Sx, State::Sx);
+				if (mode_cover) c = module->addCover(root_name, State::Sx, State::Sx);
+
+				if (c) {
+					importer->import_attributes(c->attributes, root);
+					c->set_bool_attribute(ID(unsupported_sva));
+				}
+
+				importer->num_sva_continue++;
+			}
 		}
 	}
 };

passes/hierarchy/hierarchy.cc

@@ -1149,6 +1149,25 @@ struct HierarchyPass : public Pass {
 				}
 		}
 
+		if (flag_simcheck || flag_smtcheck) {
+			for (auto mod : design->modules()) {
+				for (auto cell : mod->cells()) {
+					if (!cell->type.in(ID($check), ID($assert), ID($assume), ID($live), ID($fair), ID($cover)))
+						continue;
+					if (!cell->has_attribute(ID(unsupported_sva)))
+						continue;
+
+					auto src = cell->get_src_attribute();
+
+					if (!src.empty())
+						src += ": ";
+
+					log_error("%sProperty `%s' in module `%s' uses unsupported SVA constructs. See frontend warnings for details, run `chformal -remove a:unsupported_sva' to ignore.\n",
+						src, log_id(cell->name), log_id(mod->name));
+				}
+			}
+		}
+
 		if (!keep_positionals)
 		{
 			std::set<RTLIL::Module*> pos_mods;

tests/verific/sva_continue_on_err.ys

@@ -0,0 +1,38 @@
+verific -sv <<EOF
+module top(input clk, input a, input b);
+
+    prop_supported: assert property (@(posedge clk) a ##1 b |=> b);
+    prop_unsupported1: assert property (@(posedge clk) a ##1 b #=# b);
+    prop_unsupported2: assert property (@(posedge clk) a ##1 @(posedge b) ##1 a);
+
+    sequence local_var_seq;
+        logic v;
+        (1, v = a) ##1 b ##1 (v == a);
+    endsequence
+
+    prop_unsupported3: assert property (@(posedge clk) local_var_seq);
+
+endmodule
+EOF
+
+logger -expect warning "Mixed clocking is currently not supported" 1
+logger -expect warning "Verific SVA primitive sva_non_overlapped_followed_by .* is currently unsupported in this context" 1
+logger -expect warning "SVA sequences with local variable assignments are currently not supported" 1
+logger -expect warning "Encountered 3 items containing unsupported SVA" 1
+verific -import -sva-continue-on-err top
+logger -check-expected
+
+select -assert-count 4 top/t:$assert
+select -assert-count 4 top/a:unsupported_sva top/prop_supported %% top/t:$assert %i
+
+select -assert-count 3 top/a:unsupported_sva
+select -assert-count 3 top/a:unsupported_sva top/prop_unsupported* %i
+select -assert-count 1 top/a:unsupported_sva top/prop_unsupported1 %i
+select -assert-count 1 top/a:unsupported_sva top/prop_unsupported2 %i
+select -assert-count 1 top/a:unsupported_sva top/prop_unsupported3 %i
+select -assert-count 0 top/a:unsupported_sva top/prop_supported %i
+select -assert-count 1 top/prop_supported
+
+logger -expect error "uses unsupported SVA constructs." 1
+hierarchy -smtcheck -top top
+logger -check-expected

tests/verific/sva_continue_on_err_explosion.ys

@@ -0,0 +1,31 @@
+verific -sv <<EOF
+module top(input clk, input a, input b);
+
+    prop_supported1: assert property (@(posedge clk) a ##1 b |=> b);
+
+    prop_exploding: assert property (@(posedge clk)
+        ((a [*7] ##1 b)  [*11]) and
+        ((a [*11] ##1 b) [*7]) and
+        ((a [*13] ##1 b) [*5]) and
+        ((a [*5] ##1 b) [*13])
+    );
+
+    prop_supported2: assert property (@(posedge clk) a [*5] ##1 b |=> b);
+
+endmodule
+EOF
+
+logger -expect warning "Stopping to prevent exponential design size explosion." 1
+verific -import -sva-continue-on-err top
+logger -check-expected
+
+select -assert-count 3 top/t:$assert
+select -assert-count 1 top/a:unsupported_sva top/prop_exploding %% top/t:$assert %i
+
+select -assert-count 0 top/a:unsupported_sva top/prop_supported1 %i
+select -assert-count 0 top/a:unsupported_sva top/prop_supported2 %i
+select -assert-count 2 top/prop_supported*
+
+logger -expect error "uses unsupported SVA constructs." 1
+hierarchy -smtcheck -top top
+logger -check-expected

tests/verific/sva_no_continue_on_err.ys

@@ -0,0 +1,9 @@
+
+verific -sv <<EOF
+module top(input clk, input a, input b);
+    prop_unsupported: assert property (@(posedge clk) a ##1 @(posedge b) ##1 a);
+endmodule;
+EOF
+
+logger -expect error "Mixed clocking is currently not supported" 1
+verific -import top