Add proper SVA seq.triggered support

Signed-off-by: Clifford Wolf <clifford@clifford.at>

frontends/verific/verific.cc

@@ -1001,6 +1001,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
 	pool<Instance*, hash_ptr_ops> sva_asserts;
 	pool<Instance*, hash_ptr_ops> sva_assumes;
 	pool<Instance*, hash_ptr_ops> sva_covers;
+	pool<Instance*, hash_ptr_ops> sva_triggers;
 
 	pool<RTLIL::Cell*> past_ffs;
 
@@ -1106,6 +1107,9 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
 		if (inst->Type() == PRIM_SVA_COVER || inst->Type() == PRIM_SVA_IMMEDIATE_COVER)
 			sva_covers.insert(inst);
 
+		if (inst->Type() == PRIM_SVA_TRIGGERED)
+			sva_triggers.insert(inst);
+
 		if (inst->Type() == OPER_SVA_STABLE)
 		{
 			VerificClocking clocking(this, inst->GetInput2Bit(0));
@@ -1264,6 +1268,9 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
 		for (auto inst : sva_covers)
 			import_sva_cover(this, inst);
 
+		for (auto inst : sva_triggers)
+			import_sva_trigger(this, inst);
+
 		merge_past_ffs(past_ffs);
 	}
 }

frontends/verific/verific.h

@@ -45,6 +45,16 @@ struct VerificClocking {
 	RTLIL::Cell *addDff(IdString name, SigSpec sig_d, SigSpec sig_q, Const init_value = Const());
 	RTLIL::Cell *addAdff(IdString name, RTLIL::SigSpec sig_arst, SigSpec sig_d, SigSpec sig_q, Const arst_value);
 	RTLIL::Cell *addDffsr(IdString name, RTLIL::SigSpec sig_set, RTLIL::SigSpec sig_clr, SigSpec sig_d, SigSpec sig_q);
+
+	bool property_matches_sequence(const VerificClocking &seq) const {
+		if (clock_net != seq.clock_net)
+			return false;
+		if (enable_net != seq.enable_net)
+			return false;
+		if (posedge != seq.posedge)
+			return false;
+		return true;
+	}
 };
 
 struct VerificImporter
@@ -78,10 +88,10 @@ struct VerificImporter
 	void import_netlist(RTLIL::Design *design, Verific::Netlist *nl, std::set<Verific::Netlist*> &nl_todo);
 };
 
-
 void import_sva_assert(VerificImporter *importer, Verific::Instance *inst);
 void import_sva_assume(VerificImporter *importer, Verific::Instance *inst);
 void import_sva_cover(VerificImporter *importer, Verific::Instance *inst);
+void import_sva_trigger(VerificImporter *importer, Verific::Instance *inst);
 
 YOSYS_NAMESPACE_END
 

frontends/verific/verificsva.cc

@@ -24,9 +24,7 @@
 //   seq |-> seq
 //   seq |-> not seq
 //   seq |-> seq until expr
-//   seq |-> seq until seq.triggered
 //   seq |-> not seq until expr
-//   seq |-> not seq until seq.triggered
 //
 // Currently supported sequence operators:
 //   seq ##[N:M] seq
@@ -42,6 +40,9 @@
 //   [*N:M] includes [*N], [*], [+]
 //   [=N:M], [->N:M] includes [=N], [->N]
 //
+// Expressions can be any boolean expression, including expressions
+// that use $past, $rose, $fell, $stable, and sequence.triggered.
+//
 // -------------------------------------------------------
 //
 // SVA Properties Simplified Syntax (essentially a todo-list):
@@ -772,6 +773,7 @@ struct VerificSvaImporter
 	bool mode_assert = false;
 	bool mode_assume = false;
 	bool mode_cover = false;
+	bool mode_trigger = false;
 	bool eventually = false;
 
 	Instance *net_to_ast_driver(Net *n)
@@ -791,7 +793,8 @@ struct VerificSvaImporter
 			return nullptr;
 
 		if (inst->Type() == PRIM_SVA_ROSE || inst->Type() == PRIM_SVA_FELL ||
-				inst->Type() == PRIM_SVA_STABLE || inst->Type() == OPER_SVA_STABLE || inst->Type() == PRIM_SVA_PAST)
+				inst->Type() == PRIM_SVA_STABLE || inst->Type() == OPER_SVA_STABLE ||
+				inst->Type() == PRIM_SVA_PAST || inst->Type() == PRIM_SVA_TRIGGERED)
 			return nullptr;
 
 		return inst;
@@ -819,10 +822,12 @@ struct VerificSvaImporter
 
 	[[noreturn]] void parser_error(std::string errmsg, linefile_type loc)
 	{
-		if (!importer->mode_keep)
+		parser_error(stringf("%s at %s:%d.\n", errmsg.c_str(), LineFile::GetFileName(loc), LineFile::GetLineNo(loc)));
-			log_error("%s at %s:%d.\n", errmsg.c_str(), LineFile::GetFileName(loc), LineFile::GetLineNo(loc));
+	}
-		log_warning("%s at %s:%d.\n", errmsg.c_str(), LineFile::GetFileName(loc), LineFile::GetLineNo(loc));
+
-		throw ParserErrorException();
+	[[noreturn]] void parser_error(std::string errmsg, Instance *inst)
+	{
+		parser_error(stringf("%s at %s (%s)", errmsg.c_str(), inst->View()->Owner()->Name(), inst->Name()), inst->Linefile());
 	}
 
 	[[noreturn]] void parser_error(Instance *inst)
@@ -841,6 +846,14 @@ struct VerificSvaImporter
 			return node;
 		}
 
+		if (inst->Type() == PRIM_SVA_AT)
+		{
+			VerificClocking new_clocking(importer, net);
+			if (!clocking.property_matches_sequence(new_clocking))
+				parser_error("Mixed clocking is currently not supported", inst);
+			return parse_sequence(fsm, start_node, new_clocking.body_net);
+		}
+
 		if (inst->Type() == PRIM_SVA_SEQ_CONCAT)
 		{
 			const char *sva_low_s = inst->GetAttValue("sva:low");
@@ -1003,11 +1016,8 @@ struct VerificSvaImporter
 				consequent_net = consequent_inst->GetInput1();
 				consequent_inst = net_to_ast_driver(consequent_net);
 
-				if (until_inst != nullptr) {
+				if (until_inst != nullptr)
-					if (until_inst->Type() != PRIM_SVA_TRIGGERED)
+					parser_error("Currently only expressions are allowed in SVA_UNTIL condition", until_inst);
-						parser_error("Currently only boolean expressions or sequence.triggered is allowed in SVA_UNTIL condition", until_inst->Linefile());
-					until_net = until_inst->GetInput();
-				}
 
 				SvaFsm until_fsm(clocking);
 				node = parse_sequence(until_fsm, until_fsm.startNode, until_net);
@@ -1043,7 +1053,7 @@ struct VerificSvaImporter
 			consequent_fsm.createLink(node, consequent_fsm.acceptNode);
 
 			SigBit prop_okay;
-			if (mode_cover) {
+			if (mode_cover || mode_trigger) {
 				prop_okay = consequent_not ? consequent_fsm.getReject() : consequent_fsm.getAccept();
 			} else {
 				SigBit consequent_match = consequent_not ? consequent_fsm.getAccept() : consequent_fsm.getReject();
@@ -1058,13 +1068,19 @@ struct VerificSvaImporter
 			return prop_okay;
 		}
 		else
-		if (inst->Type() == PRIM_SVA_NOT || mode_cover)
+		if (inst->Type() == PRIM_SVA_NOT)
 		{
 			SvaFsm fsm(clocking);
-			int node = parse_sequence(fsm, fsm.startNode, mode_cover ? net : inst->GetInput());
+			int node = parse_sequence(fsm, fsm.startNode, inst->GetInput());
 			fsm.createLink(node, fsm.acceptNode);
-			SigBit accept = fsm.getAccept();
+
-			SigBit prop_okay = module->Not(NEW_ID, accept);
+			SigBit prop_okay;
+			if (mode_cover || mode_trigger) {
+				prop_okay = fsm.getReject();
+			} else {
+				SigBit accept = fsm.getAccept();
+				prop_okay = module->Not(NEW_ID, accept);
+			}
 
 			if (verific_verbose) {
 				log("    Sequence FSM:\n");
@@ -1075,8 +1091,24 @@ struct VerificSvaImporter
 		}
 		else
 		{
-			// Handle unsupported primitives
+			SvaFsm fsm(clocking);
-			parser_error(inst);
+			int node = parse_sequence(fsm, fsm.startNode, net);
+			fsm.createLink(node, fsm.acceptNode);
+
+			SigBit prop_okay;
+			if (mode_cover || mode_trigger) {
+				prop_okay = fsm.getAccept();
+			} else {
+				SigBit accept = fsm.getReject();
+				prop_okay = module->Not(NEW_ID, accept);
+			}
+
+			if (verific_verbose) {
+				log("    Sequence FSM:\n");
+				fsm.dump();
+			}
+
+			return prop_okay;
 		}
 	}
 
@@ -1096,34 +1128,41 @@ struct VerificSvaImporter
 			clocking = VerificClocking(importer, root->GetInput());
 
 			if (clocking.body_net == nullptr)
-				parser_error(stringf("Failed to parse SVA clocking at %s (%s) at %s:%d.", root->Name(), root->View()->Owner()->Name(),
+				parser_error(stringf("Failed to parse SVA clocking"), root);
-						LineFile::GetFileName(root->Linefile()), LineFile::GetLineNo(root->Linefile())));
 
 			// parse SVA sequence into trigger signal
 
 			Net *net = clocking.body_net;
 			SigBit prop_okay = parse_property(net);
 
-			// add final FF stage
+			if (mode_trigger)
-
+			{
-			SigBit prop_okay_q = module->addWire(NEW_ID);
+				module->connect(importer->net_map_at(root->GetOutput()), prop_okay);
-			clocking.addDff(NEW_ID, prop_okay, prop_okay_q, Const(mode_cover ? 0 : 1, 1));
-
-			// generate assert/assume/cover cell
-
-			RTLIL::Cell *c = nullptr;
-
-			if (eventually) {
-				parser_error("No support for eventually in Verific SVA bindings yet.\n");
-				// if (mode_assert) c = module->addLive(root_name, prop_okay_q, prop_start_q);
-				// if (mode_assume) c = module->addFair(root_name, prop_okay_q, prop_start_q);
-			} else {
-				if (mode_assert) c = module->addAssert(root_name, prop_okay_q, State::S1);
-				if (mode_assume) c = module->addAssume(root_name, prop_okay_q, State::S1);
-				if (mode_cover) c = module->addCover(root_name, prop_okay_q, State::S1);
 			}
+			else
+			{
+				// add final FF stage
 
-			importer->import_attributes(c->attributes, root);
+				SigBit prop_okay_q = module->addWire(NEW_ID);
+				clocking.addDff(NEW_ID, prop_okay, prop_okay_q, Const(mode_cover ? 0 : 1, 1));
+
+				// generate assert/assume/cover cell
+
+				RTLIL::Cell *c = nullptr;
+
+				if (eventually) {
+					parser_error("No support for eventually in Verific SVA bindings yet", root);
+					// if (mode_assert) c = module->addLive(root_name, prop_okay_q, prop_start_q);
+					// if (mode_assume) c = module->addFair(root_name, prop_okay_q, prop_start_q);
+				} else {
+					if (mode_assert) c = module->addAssert(root_name, prop_okay_q, State::S1);
+					if (mode_assume) c = module->addAssume(root_name, prop_okay_q, State::S1);
+					if (mode_cover) c = module->addCover(root_name, prop_okay_q, State::S1);
+				}
+
+				if (c != nullptr)
+					importer->import_attributes(c->attributes, root);
+			}
 		}
 		catch (ParserErrorException)
 		{
@@ -1158,4 +1197,13 @@ void import_sva_cover(VerificImporter *importer, Instance *inst)
 	worker.import();
 }
 
+void import_sva_trigger(VerificImporter *importer, Instance *inst)
+{
+	VerificSvaImporter worker;
+	worker.importer = importer;
+	worker.root = inst;
+	worker.mode_trigger = true;
+	worker.import();
+}
+
 YOSYS_NAMESPACE_END