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

This option allows you to process a design that includes unsupported
SVA. Unsupported SVA gets imported as formal cells using 'x inputs and
with the `unsupported_sva` attribute set. This allows you to get a
complete list of defined properties or to check only a supported subset
of properties. To ensure no properties are unintentionally skipped for
actual verification, even in cases where `-sva-continue-on-error` is
used by default to read and inspect a design, `hierarchy -simcheck` and
`hierarchy -smtcheck` (run by SBY) now ensure that no `unsupported_sva`
property cells remain in the design.

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

@@ -1023,7 +1023,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();
@@ -1709,8 +1709,6 @@ struct VerificSvaImporter
 	}
 
 	void import()
-	{
-		try
 	{
 		module = importer->module;
 		netlist = root->Owner();
@@ -1734,6 +1732,8 @@ struct VerificSvaImporter
 
 		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 +1836,21 @@ struct VerificSvaImporter
 		}
 		catch (ParserErrorException)
 		{
+			if (importer->mode_sva_continue) {
+
+				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 `delete */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_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