Merge branch 'verificsva-ng'

3 files changed, 751 insertions, 402 deletions

diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index e85e6cf71..fc0f72be8 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -60,6 +60,7 @@ using namespace Verific;
 #ifdef YOSYS_ENABLE_VERIFIC
 YOSYS_NAMESPACE_BEGIN
 
+bool verific_verbose;
 string verific_error_msg;
 
 void msg_func(msg_type_t msg_type, const char *message_id, linefile_type linefile, const char *msg, va_list args)
@@ -97,9 +98,9 @@ string get_full_netlist_name(Netlist *nl)
 
 // ==================================================================
 
-VerificImporter::VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_nosvapp, bool mode_names, bool verbose) :
+VerificImporter::VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_names) :
 		mode_gates(mode_gates), mode_keep(mode_keep), mode_nosva(mode_nosva),
-		mode_nosvapp(mode_nosvapp), mode_names(mode_names), verbose(verbose)
+		mode_names(mode_names)
 {
 }
 
@@ -642,13 +643,13 @@ void VerificImporter::merge_past_ffs_clock(pool<RTLIL::Cell*> &candidates, SigBi
 			SigSpec sig_q = module->addWire(NEW_ID, GetSize(sig_d));
 			RTLIL::Cell *new_ff = module->addDff(NEW_ID, clock, sig_d, sig_q, clock_pol);
 
-			if (verbose)
+			if (verific_verbose)
 				log("  merging single-bit past_ffs into new %d-bit ff %s.\n", GetSize(sig_d), log_id(new_ff));
 
 			for (int i = 0; i < GetSize(sig_d); i++)
 				for (auto old_ff : dbits_db[sig_d[i]])
 				{
-					if (verbose)
+					if (verific_verbose)
 						log("    replacing old ff %s on bit %d.\n", log_id(old_ff), i);
 
 					SigBit old_q = old_ff->getPort("\\Q");
@@ -711,38 +712,12 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
 	Instance *inst;
 	PortRef *pr;
 
-	if (!mode_nosvapp)
-	{
-		vector<Instance*> asserts, assumes, covers;
-
-		FOREACH_INSTANCE_OF_NETLIST(nl, mi, inst)
-		{
-			if (inst->Type() == PRIM_SVA_ASSERT || inst->Type() == PRIM_SVA_IMMEDIATE_ASSERT)
-				asserts.push_back(inst);
-
-			if (inst->Type() == PRIM_SVA_ASSUME || inst->Type() == PRIM_SVA_IMMEDIATE_ASSUME)
-				assumes.push_back(inst);
-
-			if (inst->Type() == PRIM_SVA_COVER || inst->Type() == PRIM_SVA_IMMEDIATE_COVER)
-				covers.push_back(inst);
-		}
-
-		for (auto inst : asserts)
-			svapp_assert(inst);
-
-		for (auto inst : assumes)
-			svapp_assume(inst);
-
-		for (auto inst : covers)
-			svapp_cover(inst);
-	}
-
 	FOREACH_PORT_OF_NETLIST(nl, mi, port)
 	{
 		if (port->Bus())
 			continue;
 
-		if (verbose)
+		if (verific_verbose)
 			log("  importing port %s.\n", port->Name());
 
 		RTLIL::Wire *wire = module->addWire(RTLIL::escape_id(port->Name()));
@@ -768,7 +743,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
 
 	FOREACH_PORTBUS_OF_NETLIST(nl, mi, portbus)
 	{
-		if (verbose)
+		if (verific_verbose)
 			log("  importing portbus %s.\n", portbus->Name());
 
 		RTLIL::Wire *wire = module->addWire(RTLIL::escape_id(portbus->Name()), portbus->Size());
@@ -882,7 +857,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
 			anyseq_nets.insert(net);
 
 		if (net_map.count(net)) {
-			if (verbose)
+			if (verific_verbose)
 				log("  skipping net %s.\n", net->Name());
 			continue;
 		}
@@ -892,7 +867,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
 
 		RTLIL::IdString wire_name = module->uniquify(mode_names || net->IsUserDeclared() ? RTLIL::escape_id(net->Name()) : NEW_ID);
 
-		if (verbose)
+		if (verific_verbose)
 			log("  importing net %s as %s.\n", net->Name(), log_id(wire_name));
 
 		RTLIL::Wire *wire = module->addWire(wire_name);
@@ -916,7 +891,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
 		{
 			RTLIL::IdString wire_name = module->uniquify(mode_names || netbus->IsUserDeclared() ? RTLIL::escape_id(netbus->Name()) : NEW_ID);
 
-			if (verbose)
+			if (verific_verbose)
 				log("  importing netbus %s as %s.\n", netbus->Name(), log_id(wire_name));
 
 			RTLIL::Wire *wire = module->addWire(wire_name, netbus->Size());
@@ -958,7 +933,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
 		}
 		else
 		{
-			if (verbose)
+			if (verific_verbose)
 				log("  skipping netbus %s.\n", netbus->Name());
 		}
 
@@ -1022,7 +997,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
 	{
 		RTLIL::IdString inst_name = module->uniquify(mode_names || inst->IsUserDeclared() ? RTLIL::escape_id(inst->Name()) : NEW_ID);
 
-		if (verbose)
+		if (verific_verbose)
 			log("  importing cell %s (%s) as %s.\n", inst->Name(), inst->View()->Owner()->Name(), log_id(inst_name));
 
 		if (inst->Type() == PRIM_PWR) {
@@ -1134,7 +1109,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
 				sig_o.append(net_map_at(inst->GetOutputBit(i)));
 			}
 
-			if (verbose) {
+			if (verific_verbose) {
 				log("    %sedge FF with D=%s, Q=%s, C=%s.\n", clock_edge.posedge ? "pos" : "neg",
 						log_signal(sig_d), log_signal(sig_q), log_signal(clock_edge.clock_sig));
 				log("    XNOR with A=%s, B=%s, Y=%s.\n",
@@ -1156,7 +1131,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
 			SigSpec sig_o = net_map_at(inst->GetOutput());
 			SigSpec sig_q = module->addWire(NEW_ID);
 
-			if (verbose) {
+			if (verific_verbose) {
 				log("    %sedge FF with D=%s, Q=%s, C=%s.\n", clock_edge.posedge ? "pos" : "neg",
 						log_signal(sig_d), log_signal(sig_q), log_signal(clock_edge.clock_sig));
 				log("    XNOR with A=%s, B=%s, Y=%s.\n",
@@ -1177,7 +1152,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
 			SigBit sig_d = net_map_at(inst->GetInput1());
 			SigBit sig_q = net_map_at(inst->GetOutput());
 
-			if (verbose)
+			if (verific_verbose)
 				log("    %sedge FF with D=%s, Q=%s, C=%s.\n", clock_edge.posedge ? "pos" : "neg",
 						log_signal(sig_d), log_signal(sig_q), log_signal(clock_edge.clock_sig));
 
@@ -1188,7 +1163,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
 		}
 
 		if (!mode_keep && verific_sva_prims.count(inst->Type())) {
-			if (verbose)
+			if (verific_verbose)
 				log("    skipping SVA cell in non k-mode\n");
 			continue;
 		}
@@ -1215,11 +1190,11 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
 
 		dict<IdString, vector<SigBit>> cell_port_conns;
 
-		if (verbose)
+		if (verific_verbose)
 			log("    ports in verific db:\n");
 
 		FOREACH_PORTREF_OF_INST(inst, mi2, pr) {
-			if (verbose)
+			if (verific_verbose)
 				log("      .%s(%s)\n", pr->GetPort()->Name(), pr->GetNet()->Name());
 			const char *port_name = pr->GetPort()->Name();
 			int port_offset = 0;
@@ -1238,11 +1213,11 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
 			sigvec[port_offset] = net_map_at(pr->GetNet());
 		}
 
-		if (verbose)
+		if (verific_verbose)
 			log("    ports in yosys db:\n");
 
 		for (auto &it : cell_port_conns) {
-			if (verbose)
+			if (verific_verbose)
 				log("      .%s(%s)\n", log_id(it.first), log_signal(it.second));
 			cell->setPort(it.first, it.second);
 		}
@@ -1292,7 +1267,6 @@ VerificClockEdge::VerificClockEdge(VerificImporter *importer, Instance *inst)
 struct VerificExtNets
 {
 	int portname_cnt = 0;
-	bool verbose = false;
 
 	// a map from Net to the same Net one level up in the design hierarchy
 	std::map<Net*, Net*> net_level_up;
@@ -1347,7 +1321,7 @@ struct VerificExtNets
 			if (!net->IsExternalTo(nl))
 				continue;
 
-			if (verbose)
+			if (verific_verbose)
 				log("Fixing external net reference on port %s.%s.%s:\n", get_full_netlist_name(nl).c_str(), inst->Name(), port->Name());
 
 			while (net->IsExternalTo(nl))
@@ -1355,12 +1329,12 @@ struct VerificExtNets
 				Net *newnet = get_net_level_up(net);
 				if (newnet == net) break;
 
-				if (verbose)
+				if (verific_verbose)
 					log("  external net: %s.%s\n", get_full_netlist_name(net->Owner()).c_str(), net->Name());
 				net = newnet;
 			}
 
-			if (verbose)
+			if (verific_verbose)
 				log("  final net: %s.%s%s\n", get_full_netlist_name(net->Owner()).c_str(), net->Name(), net->IsExternalTo(nl) ? " (external)" : "");
 			todo_connect.push_back(tuple<Instance*, Port*, Net*>(inst, port, net));
 		}
@@ -1444,9 +1418,6 @@ struct VerificPass : public Pass {
 		log("  -nosva\n");
 		log("    Ignore SVA properties, do not infer checker logic.\n");
 		log("\n");
-		log("  -nosvapp\n");
-		log("    Disable SVA properties pre-processing pass. This implies -nosva.\n");
-		log("\n");
 		log("  -n\n");
 		log("    Keep all Verific names on instances and nets. By default only\n");
 		log("    user-declared names are preserved.\n");
@@ -1469,6 +1440,8 @@ struct VerificPass : public Pass {
 		veri_file::DefineCmdLineMacro("VERIFIC");
 		veri_file::DefineCmdLineMacro("SYNTHESIS");
 
+		verific_verbose = false;
+
 		const char *release_str = Message::ReleaseString();
 		time_t release_time = Message::ReleaseDate();
 		char *release_tmstr = ctime(&release_time);
@@ -1581,8 +1554,8 @@ struct VerificPass : public Pass {
 		{
 			std::set<Netlist*> nl_todo, nl_done;
 			bool mode_all = false, mode_gates = false, mode_keep = false;
-			bool mode_nosva = false, mode_nosvapp = false, mode_names = false;
-			bool verbose = false, flatten = false, extnets = false;
+			bool mode_nosva = false, mode_names = false;
+			bool flatten = false, extnets = false;
 			string dumpfile;
 
 			for (argidx++; argidx < GetSize(args); argidx++) {
@@ -1610,17 +1583,12 @@ struct VerificPass : public Pass {
 					mode_nosva = true;
 					continue;
 				}
-				if (args[argidx] == "-nosvapp") {
-					mode_nosva = true;
-					mode_nosvapp = true;
-					continue;
-				}
 				if (args[argidx] == "-n") {
 					mode_names = true;
 					continue;
 				}
 				if (args[argidx] == "-v") {
-					verbose = true;
+					verific_verbose = true;
 					continue;
 				}
 				if (args[argidx] == "-d" && argidx+1 < GetSize(args)) {
@@ -1697,7 +1665,6 @@ struct VerificPass : public Pass {
 
 			if (extnets) {
 				VerificExtNets worker;
-				worker.verbose = verbose;
 				for (auto nl : nl_todo)
 					worker.run(nl);
 			}
@@ -1710,7 +1677,7 @@ struct VerificPass : public Pass {
 			while (!nl_todo.empty()) {
 				Netlist *nl = *nl_todo.begin();
 				if (nl_done.count(nl) == 0) {
-					VerificImporter importer(mode_gates, mode_keep, mode_nosva, mode_nosvapp, mode_names, verbose);
+					VerificImporter importer(mode_gates, mode_keep, mode_nosva, mode_names);
 					importer.import_netlist(design, nl, nl_todo);
 				}
 				nl_todo.erase(nl);
diff --git a/frontends/verific/verific.h b/frontends/verific/verific.h
index 4f1cb5d0f..28a0c174b 100644
--- a/frontends/verific/verific.h
+++ b/frontends/verific/verific.h
@@ -23,6 +23,8 @@
 
 YOSYS_NAMESPACE_BEGIN
 
+extern bool verific_verbose;
+
 extern pool<int> verific_sva_prims;
 
 struct VerificImporter;
@@ -42,9 +44,9 @@ struct VerificImporter
 	std::map<Verific::Net*, RTLIL::SigBit> net_map;
 	std::map<Verific::Net*, Verific::Net*> sva_posedge_map;
 
-	bool mode_gates, mode_keep, mode_nosva, mode_nosvapp, mode_names, verbose;
+	bool mode_gates, mode_keep, mode_nosva, mode_names;
 
-	VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_nosvapp, bool mode_names, bool verbose);
+	VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_names);
 
 	RTLIL::SigBit net_map_at(Verific::Net *net);
 
@@ -70,10 +72,6 @@ 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 svapp_assert(Verific::Instance *inst);
-void svapp_assume(Verific::Instance *inst);
-void svapp_cover(Verific::Instance *inst);
-
 YOSYS_NAMESPACE_END
 
 #endif
diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc
index 94443cd3e..2185e4596 100644
--- a/frontends/verific/verificsva.cc
+++ b/frontends/verific/verificsva.cc
@@ -24,7 +24,6 @@
 //   not prop
 //   prop or prop
 //   prop and prop
-//   seq |-> prop
 //   seq |=> prop
 //   if (expr) prop [else prop]
 //   prop until prop
@@ -35,7 +34,6 @@
 //
 // seq:
 //   expr
-//   expr ##N seq
 //   expr ##[N:M] seq
 //   seq or seq
 //   seq and seq
@@ -43,12 +41,25 @@
 //   first_match (seq)
 //   expr throughout seq
 //   seq within seq
-//   seq [*N]
 //   seq [*N:M]
-//   expr [=N]
 //   expr [=N:M]
-//   expr [->N]
 //   expr [->N:M]
+//
+// Notes:
+//   |=> is a placeholder for |-> and |=>
+//   "until" is a placeholder for all until operators
+//   ##[N:M], [*N:M], [=N:M], [->N:M] includes ##N, [*N], [=N], [->N]
+//
+// Currently supported property styles:
+//   not seq
+//   seq |=> seq
+//   seq |=> not seq
+//   seq |=> seq until seq
+//
+// Currently supported sequence operators:
+//   ##[N:M]
+//   [*N:M]
+//   throughout
 
 
 #include "kernel/yosys.h"
@@ -60,351 +71,652 @@ USING_YOSYS_NAMESPACE
 using namespace Verific;
 #endif
 
-YOSYS_NAMESPACE_BEGIN
+PRIVATE_NAMESPACE_BEGIN
 
-pool<int> verific_sva_prims = {
-	// Copy&paste from Verific 3.16_484_32_170630 Netlist.h
-	PRIM_SVA_IMMEDIATE_ASSERT, PRIM_SVA_ASSERT, PRIM_SVA_COVER, PRIM_SVA_ASSUME,
-	PRIM_SVA_EXPECT, PRIM_SVA_POSEDGE, PRIM_SVA_NOT, PRIM_SVA_FIRST_MATCH,
-	PRIM_SVA_ENDED, PRIM_SVA_MATCHED, PRIM_SVA_CONSECUTIVE_REPEAT,
-	PRIM_SVA_NON_CONSECUTIVE_REPEAT, PRIM_SVA_GOTO_REPEAT,
-	PRIM_SVA_MATCH_ITEM_TRIGGER, PRIM_SVA_AND, PRIM_SVA_OR, PRIM_SVA_SEQ_AND,
-	PRIM_SVA_SEQ_OR, PRIM_SVA_EVENT_OR, PRIM_SVA_OVERLAPPED_IMPLICATION,
-	PRIM_SVA_NON_OVERLAPPED_IMPLICATION, PRIM_SVA_OVERLAPPED_FOLLOWED_BY,
-	PRIM_SVA_NON_OVERLAPPED_FOLLOWED_BY, PRIM_SVA_INTERSECT, PRIM_SVA_THROUGHOUT,
-	PRIM_SVA_WITHIN, PRIM_SVA_AT, PRIM_SVA_DISABLE_IFF, PRIM_SVA_SAMPLED,
-	PRIM_SVA_ROSE, PRIM_SVA_FELL, PRIM_SVA_STABLE, PRIM_SVA_PAST,
-	PRIM_SVA_MATCH_ITEM_ASSIGN, PRIM_SVA_SEQ_CONCAT, PRIM_SVA_IF,
-	PRIM_SVA_RESTRICT, PRIM_SVA_TRIGGERED, PRIM_SVA_STRONG, PRIM_SVA_WEAK,
-	PRIM_SVA_NEXTTIME, PRIM_SVA_S_NEXTTIME, PRIM_SVA_ALWAYS, PRIM_SVA_S_ALWAYS,
-	PRIM_SVA_S_EVENTUALLY, PRIM_SVA_EVENTUALLY, PRIM_SVA_UNTIL, PRIM_SVA_S_UNTIL,
-	PRIM_SVA_UNTIL_WITH, PRIM_SVA_S_UNTIL_WITH, PRIM_SVA_IMPLIES, PRIM_SVA_IFF,
-	PRIM_SVA_ACCEPT_ON, PRIM_SVA_REJECT_ON, PRIM_SVA_SYNC_ACCEPT_ON,
-	PRIM_SVA_SYNC_REJECT_ON, PRIM_SVA_GLOBAL_CLOCKING_DEF,
-	PRIM_SVA_GLOBAL_CLOCKING_REF, PRIM_SVA_IMMEDIATE_ASSUME,
-	PRIM_SVA_IMMEDIATE_COVER, OPER_SVA_SAMPLED, OPER_SVA_STABLE
+// Non-deterministic FSM
+struct SvaNFsmNode
+{
+	// Edge: Activate the target node if ctrl signal is true, consumes clock cycle
+	// Link: Activate the target node if ctrl signal is true, doesn't consume clock cycle
+	vector<pair<int, SigBit>> edges, links;
 };
 
-struct VerificSvaImporter
+// Non-deterministic FSM after resolving links
+struct SvaUFsmNode
 {
-	VerificImporter *importer = nullptr;
-	Module *module = nullptr;
+	// Edge: Activate the target node if all bits in ctrl signal are true, consumes clock cycle
+	// Accept: This node functions as an accept node if all bits in ctrl signal are true
+	vector<pair<int, SigSpec>> edges;
+	vector<SigSpec> accept;
+	bool reachable;
+};
 
-	Netlist *netlist = nullptr;
-	Instance *root = nullptr;
+// Deterministic FSM
+struct SvaDFsmNode
+{
+	// A DFSM state corresponds to a set of NFSM states. We represent DFSM states as sorted vectors
+	// of NFSM state node ids. Edge/accept controls are constants matched against the ctrl sigspec.
+	SigSpec ctrl;
+	vector<pair<vector<int>, Const>> edges;
+	vector<Const> accept, reject;
+
+	// additional temp data for getReject()
+	Wire *ffoutwire;
+	SigBit statesig;
+	SigSpec nextstate;
+};
 
-	SigBit clock = State::Sx;
-	bool clock_posedge = false;
+struct SvaFsm
+{
+	Module *module;
+	SigBit clock;
+	bool clockpol;
 
-	SigBit disable_iff = State::S0;
+	SigBit trigger_sig = State::S1, disable_sig;
+	SigBit accept_sig = State::Sz, reject_sig = State::Sz;
+	SigBit throughout_sig = State::S1;
+	bool materialized = false;
 
-	bool mode_assert = false;
-	bool mode_assume = false;
-	bool mode_cover = false;
-	bool eventually = false;
-	bool did_something = false;
+	vector<SigBit> disable_stack;
+	vector<SigBit> throughout_stack;
 
-	Instance *net_to_ast_driver(Net *n)
-	{
-		if (n == nullptr)
-			return nullptr;
+	int startNode, acceptNode;
+	vector<SvaNFsmNode> nodes;
 
-		if (n->IsMultipleDriven())
-			return nullptr;
+	SvaFsm(Module *mod, SigBit clk, bool clkpol, SigBit dis = State::S0, SigBit trig = State::S1)
+	{
+		module = mod;
+		clock = clk;
+		clockpol = clkpol;
+		disable_sig = dis;
+		trigger_sig = trig;
+
+		startNode = createNode();
+		acceptNode = createNode();
+	}
 
-		Instance *inst = n->Driver();
+	void pushDisable(SigBit sig)
+	{
+		log_assert(!materialized);
 
-		if (inst == nullptr)
-			return nullptr;
+		disable_stack.push_back(disable_sig);
 
-		if (!verific_sva_prims.count(inst->Type()))
-			return nullptr;
+		if (disable_sig == State::S0)
+			disable_sig = sig;
+		else
+			disable_sig = module->Or(NEW_ID, disable_sig, sig);
+	}
 
-		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)
-			return nullptr;
+	void popDisable()
+	{
+		log_assert(!materialized);
+		log_assert(!disable_stack.empty());
 
-		return inst;
+		disable_sig = disable_stack.back();
+		disable_stack.pop_back();
 	}
 
-	Instance *get_ast_input(Instance *inst) { return net_to_ast_driver(inst->GetInput()); }
-	Instance *get_ast_input1(Instance *inst) { return net_to_ast_driver(inst->GetInput1()); }
-	Instance *get_ast_input2(Instance *inst) { return net_to_ast_driver(inst->GetInput2()); }
-	Instance *get_ast_input3(Instance *inst) { return net_to_ast_driver(inst->GetInput3()); }
-	Instance *get_ast_control(Instance *inst) { return net_to_ast_driver(inst->GetControl()); }
+	void pushThroughout(SigBit sig)
+	{
+		log_assert(!materialized);
 
-	// ----------------------------------------------------------
-	// SVA AST Types
+		throughout_stack.push_back(throughout_sig);
 
-	struct svatype_t
+		if (throughout_sig == State::S1)
+			throughout_sig = sig;
+		else
+			throughout_sig = module->And(NEW_ID, throughout_sig, sig);
+	}
+
+	void popThroughout()
 	{
-		bool flag_linear = true;
-	};
+		log_assert(!materialized);
+		log_assert(!throughout_stack.empty());
 
-	std::map<Instance*, svatype_t> svatype_cache;
+		throughout_sig = throughout_stack.back();
+		throughout_stack.pop_back();
+	}
 
-	void svatype_visit_child(svatype_t &entry, Instance *inst)
+	int createNode()
 	{
-		if (inst == nullptr)
-			return;
+		log_assert(!materialized);
 
-		const svatype_t &child_entry = svatype(inst);
-		entry.flag_linear &= child_entry.flag_linear;
+		int idx = GetSize(nodes);
+		nodes.push_back(SvaNFsmNode());
+		return idx;
 	}
 
-	const svatype_t &svatype(Instance *inst)
+	void createEdge(int from_node, int to_node, SigBit ctrl = State::S1)
 	{
-		if (svatype_cache.count(inst) != 0)
-			return svatype_cache.at(inst);
-
-		svatype_t &entry = svatype_cache[inst];
+		log_assert(!materialized);
+		log_assert(0 <= from_node && from_node < GetSize(nodes));
+		log_assert(0 <= to_node && to_node < GetSize(nodes));
 
-		if (inst == nullptr)
-			return entry;
+		if (throughout_sig != State::S1) {
+			if (ctrl != State::S1)
+				ctrl = module->And(NEW_ID, throughout_sig, ctrl);
+			else
+				ctrl = throughout_sig;
+		}
 
-		if (inst->Type() == PRIM_SVA_SEQ_CONCAT || inst->Type() == PRIM_SVA_CONSECUTIVE_REPEAT)
-		{
-			const char *sva_low_s = inst->GetAttValue("sva:low");
-			const char *sva_high_s = inst->GetAttValue("sva:high");
+		nodes[from_node].edges.push_back(make_pair(to_node, ctrl));
+	}
 
-			int sva_low = atoi(sva_low_s);
-			int sva_high = atoi(sva_high_s);
-			bool sva_inf = !strcmp(sva_high_s, "$");
+	void createLink(int from_node, int to_node, SigBit ctrl = State::S1)
+	{
+		log_assert(!materialized);
+		log_assert(0 <= from_node && from_node < GetSize(nodes));
+		log_assert(0 <= to_node && to_node < GetSize(nodes));
 
-			if (sva_inf || sva_low != sva_high)
-				entry.flag_linear = false;
+		if (throughout_sig != State::S1) {
+			if (ctrl != State::S1)
+				ctrl = module->And(NEW_ID, throughout_sig, ctrl);
+			else
+				ctrl = throughout_sig;
 		}
 
-		svatype_visit_child(entry, get_ast_input(inst));
-		svatype_visit_child(entry, get_ast_input1(inst));
-		svatype_visit_child(entry, get_ast_input2(inst));
-		svatype_visit_child(entry, get_ast_input3(inst));
-		svatype_visit_child(entry, get_ast_control(inst));
-
-		return entry;
+		nodes[from_node].links.push_back(make_pair(to_node, ctrl));
 	}
 
-	// ----------------------------------------------------------
-	// SVA Preprocessor
+	void make_link_order(vector<int> &order, int node, int min)
+	{
+		order[node] = std::max(order[node], min);
+		for (auto &it : nodes[node].links)
+			make_link_order(order, it.first, order[node]+1);
+	}
 
-	Net *rewrite_input(Instance *inst) { return rewrite(get_ast_input(inst), inst->GetInput()); }
-	Net *rewrite_input1(Instance *inst) { return rewrite(get_ast_input1(inst), inst->GetInput1()); }
-	Net *rewrite_input2(Instance *inst) { return rewrite(get_ast_input2(inst), inst->GetInput2()); }
-	Net *rewrite_input3(Instance *inst) { return rewrite(get_ast_input3(inst), inst->GetInput3()); }
-	Net *rewrite_control(Instance *inst) { return rewrite(get_ast_control(inst), inst->GetControl()); }
+	// ----------------------------------------------------
+	// Generating NFSM circuit to acquire accept signal
 
-	Net *rewrite(Instance *inst, Net *default_net = nullptr)
+	SigBit getAccept()
 	{
-		if (inst == nullptr)
-			return default_net;
+		log_assert(!materialized);
+		materialized = true;
+
+		vector<Wire*> state_wire(GetSize(nodes));
+		vector<SigBit> state_sig(GetSize(nodes));
+		vector<SigBit> next_state_sig(GetSize(nodes));
+
+		// Create state signals
+
+		{
+			SigBit not_disable = State::S1;
+
+			if (disable_sig != State::S0)
+				not_disable = module->Not(NEW_ID, disable_sig);
+
+			for (int i = 0; i < GetSize(nodes); i++)
+			{
+				Wire *w = module->addWire(NEW_ID);
+				state_wire[i] = w;
+				state_sig[i] = w;
 
-		if (inst->Type() == PRIM_SVA_ASSERT || inst->Type() == PRIM_SVA_COVER || inst->Type() == PRIM_SVA_ASSUME ||
-				inst->Type() == PRIM_SVA_IMMEDIATE_ASSERT || inst->Type() == PRIM_SVA_IMMEDIATE_COVER || inst->Type() == PRIM_SVA_IMMEDIATE_ASSUME) {
-			Net *new_net = rewrite(get_ast_input(inst));
-			if (new_net) {
-				inst->Disconnect(inst->View()->GetInput());
-				inst->Connect(inst->View()->GetInput(), new_net);
+				if (i == startNode)
+					state_sig[i] = module->Or(NEW_ID, state_sig[i], trigger_sig);
+
+				if (disable_sig != State::S0)
+					state_sig[i] = module->And(NEW_ID, state_sig[i], not_disable);
 			}
-			return default_net;
 		}
 
-		if (inst->Type() == PRIM_SVA_AT || inst->Type() == PRIM_SVA_DISABLE_IFF) {
-			Net *new_net = rewrite(get_ast_input2(inst));
-			if (new_net) {
-				inst->Disconnect(inst->View()->GetInput2());
-				inst->Connect(inst->View()->GetInput2(), new_net);
+		// Follow Links
+
+		{
+			vector<int> node_order(GetSize(nodes));
+			vector<vector<int>> order_to_nodes;
+
+			for (int i = 0; i < GetSize(nodes); i++)
+				make_link_order(node_order, i, 0);
+
+			for (int i = 0; i < GetSize(nodes); i++) {
+				if (node_order[i] >= GetSize(order_to_nodes))
+					order_to_nodes.resize(node_order[i]+1);
+				order_to_nodes[node_order[i]].push_back(i);
+			}
+
+			for (int order = 0; order < GetSize(order_to_nodes); order++)
+			for (int node : order_to_nodes[order])
+			{
+				for (auto &it : nodes[node].links)
+				{
+					int target = it.first;
+					SigBit ctrl = state_sig[node];
+
+					if (it.second != State::S1)
+						ctrl = module->And(NEW_ID, ctrl, it.second);
+
+					state_sig[target] = module->Or(NEW_ID, state_sig[target], ctrl);
+				}
 			}
-			return default_net;
 		}
 
-		if (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION)
+		// Construct activations
+
 		{
-			if (mode_cover) {
-				did_something = true;
-				Net *new_in1 = rewrite_input1(inst);
-				Net *new_in2 = rewrite_input2(inst);
-				return netlist->SvaBinary(PRIM_SVA_SEQ_CONCAT, new_in1, new_in2, inst->Linefile());
+			vector<SigSpec> activate_sig(GetSize(nodes));
+			vector<SigBit> activate_bit(GetSize(nodes));
+
+			for (int i = 0; i < GetSize(nodes); i++) {
+				for (auto &it : nodes[i].edges)
+					activate_sig[it.first].append(module->And(NEW_ID, state_sig[i], it.second));
+			}
+
+			for (int i = 0; i < GetSize(nodes); i++) {
+				if (GetSize(activate_sig[i]) == 0)
+					next_state_sig[i] = State::S0;
+				else if (GetSize(activate_sig[i]) == 1)
+					next_state_sig[i] = activate_sig[i];
+				else
+					next_state_sig[i] = module->ReduceOr(NEW_ID, activate_sig[i]);
 			}
-			return default_net;
 		}
 
-		if (inst->Type() == PRIM_SVA_NOT)
+		// Create state FFs
+
+		for (int i = 0; i < GetSize(nodes); i++)
 		{
-			if (mode_assert || mode_assume) {
-				did_something = true;
-				Net *new_in = rewrite_input(inst);
-				Net *net_zero = netlist->Gnd(inst->Linefile());
-				return netlist->SvaBinary(PRIM_SVA_OVERLAPPED_IMPLICATION, new_in, net_zero, inst->Linefile());
+			if (next_state_sig[i] != State::S0) {
+				state_wire[i]->attributes["\\init"] = Const(0, 1);
+				module->addDff(NEW_ID, clock, next_state_sig[i], state_wire[i], clockpol);
+			} else {
+				module->connect(state_wire[i], State::S0);
 			}
-			return default_net;
 		}
 
-		return default_net;
+		return state_sig[acceptNode];
 	}
 
-	void rewrite()
+	// ----------------------------------------------------
+	// Generating quantifier-based NFSM circuit to acquire reject signal
+
+	SigBit getAnyAllRejectWorker(bool allMode)
 	{
-		netlist = root->Owner();
-		do {
-			did_something = false;
-			rewrite(root);
-		} while (did_something);
+		// FIXME
+		log_abort();
 	}
 
-	// ----------------------------------------------------------
-	// SVA Importer
+	SigBit getAnyReject()
+	{
+		return getAnyAllRejectWorker(false);
+	}
+
+	SigBit getAllReject()
+	{
+		return getAnyAllRejectWorker(true);
+	}
 
-	vector<SigBit> sva_until_list_inclusive;
-	vector<SigBit> sva_until_list_exclusive;
-	vector<vector<SigBit>*> sva_sequence_alive_list;
+	// ----------------------------------------------------
+	// Generating DFSM circuit to acquire reject signal
 
-	struct sequence_t {
-		int length = 0;
-		SigBit sig_a = State::S1;
-		SigBit sig_en = State::S1;
-	};
+	vector<SvaUFsmNode> unodes;
+	dict<vector<int>, SvaDFsmNode> dnodes;
 
-	void sequence_cond(sequence_t &seq, SigBit cond)
+	void node_to_unode(int node, int unode, SigSpec ctrl)
 	{
-		seq.sig_a = module->And(NEW_ID, seq.sig_a, cond);
+		if (node == acceptNode)
+			unodes[unode].accept.push_back(ctrl);
+
+		for (auto &it : nodes[node].edges) {
+			if (it.second != State::S1) {
+				SigSpec s = {ctrl, it.second};
+				s.sort_and_unify();
+				unodes[unode].edges.push_back(make_pair(it.first, s));
+			} else {
+				unodes[unode].edges.push_back(make_pair(it.first, ctrl));
+			}
+		}
+
+		for (auto &it : nodes[node].links) {
+			if (it.second != State::S1) {
+				SigSpec s = {ctrl, it.second};
+				s.sort_and_unify();
+				node_to_unode(it.first, unode, s);
+			} else {
+				node_to_unode(it.first, unode, ctrl);
+			}
+		}
 	}
 
-	void sequence_ff(sequence_t &seq)
+	void mark_reachable_unode(int unode)
 	{
-		if (disable_iff != State::S0)
-			seq.sig_en = module->Mux(NEW_ID, seq.sig_en, State::S0, disable_iff);
+		if (unodes[unode].reachable)
+			return;
 
-		for (auto &expr : sva_until_list_exclusive)
-			seq.sig_a = module->LogicAnd(NEW_ID, seq.sig_a, expr);
+		unodes[unode].reachable = true;
+		for (auto &it : unodes[unode].edges)
+			mark_reachable_unode(it.first);
+	}
 
-		Wire *sig_a_q = module->addWire(NEW_ID);
-		sig_a_q->attributes["\\init"] = Const(0, 1);
+	void usortint(vector<int> &vec)
+	{
+		vector<int> newvec;
+		std::sort(vec.begin(), vec.end());
+		for (int i = 0; i < GetSize(vec); i++)
+			if (i == GetSize(vec)-1 || vec[i] != vec[i+1])
+				newvec.push_back(vec[i]);
+		vec.swap(newvec);
+	}
 
-		Wire *sig_en_q = module->addWire(NEW_ID);
-		sig_en_q->attributes["\\init"] = Const(0, 1);
+	bool cmp_ctrl(const pool<SigBit> &ctrl_bits, const SigSpec &ctrl)
+	{
+		for (int i = 0; i < GetSize(ctrl); i++)
+			if (ctrl_bits.count(ctrl[i]) == 0)
+				return false;
+		return true;
+	}
+
+	void create_dnode(const vector<int> &state, bool firstmatch)
+	{
+		if (dnodes.count(state) != 0)
+			return;
 
-		for (auto list : sva_sequence_alive_list)
-			list->push_back(module->LogicAnd(NEW_ID, seq.sig_a, seq.sig_en));
+		SvaDFsmNode dnode;
+		dnodes[state] = SvaDFsmNode();
 
-		module->addDff(NEW_ID, clock, seq.sig_a, sig_a_q, clock_posedge);
-		module->addDff(NEW_ID, clock, seq.sig_en, sig_en_q, clock_posedge);
+		for (int unode : state) {
+			log_assert(unodes[unode].reachable);
+			for (auto &it : unodes[unode].edges)
+				dnode.ctrl.append(it.second);
+			for (auto &it : unodes[unode].accept)
+				dnode.ctrl.append(it);
+		}
 
-		if (seq.length >= 0)
-			seq.length++;
+		dnode.ctrl.sort_and_unify();
 
-		seq.sig_a = sig_a_q;
-		seq.sig_en = sig_en_q;
+		if (GetSize(dnode.ctrl) > 10)
+			log_error("SVA property DFSM state ctrl signal has over 10 bits. Stopping to prevent exponential design size explosion.\n");
 
-		for (auto &expr : sva_until_list_inclusive)
-			seq.sig_a = module->LogicAnd(NEW_ID, seq.sig_a, expr);
-	}
+		for (int i = 0; i < (1 << GetSize(dnode.ctrl)); i++)
+		{
+			Const ctrl_val(i, GetSize(dnode.ctrl));
+			pool<SigBit> ctrl_bits;
+
+			for (int i = 0; i < GetSize(dnode.ctrl); i++)
+				if (ctrl_val[i] == State::S1)
+					ctrl_bits.insert(dnode.ctrl[i]);
+
+			vector<int> new_state;
+			bool accept = false;
+
+			for (int unode : state)
+			for (auto &it : unodes[unode].accept)
+				if (cmp_ctrl(ctrl_bits, it))
+					accept = true;
+
+			if (!accept || !firstmatch) {
+				for (int unode : state)
+				for (auto &it : unodes[unode].edges)
+					if (cmp_ctrl(ctrl_bits, it.second))
+						new_state.push_back(it.first);
+			}
 
-	void combine_seq(sequence_t &seq, const sequence_t &other_seq)
-	{
-		if (seq.length != other_seq.length)
-			seq.length = -1;
+			if (accept)
+				dnode.accept.push_back(ctrl_val);
 
-		SigBit filtered_a = module->LogicAnd(NEW_ID, seq.sig_a, seq.sig_en);
-		SigBit other_filtered_a = module->LogicAnd(NEW_ID, other_seq.sig_a, other_seq.sig_en);
+			if (new_state.empty()) {
+				if (!accept)
+					dnode.reject.push_back(ctrl_val);
+			} else {
+				usortint(new_state);
+				dnode.edges.push_back(make_pair(new_state, ctrl_val));
+				create_dnode(new_state, firstmatch);
+			}
+		}
 
-		seq.sig_a = module->LogicOr(NEW_ID, filtered_a, other_filtered_a);
-		seq.sig_en = module->LogicOr(NEW_ID, seq.sig_en, other_seq.sig_en);
+		dnodes[state] = dnode;
 	}
 
-	void combine_seq(sequence_t &seq, SigBit other_a, SigBit other_en)
+	SigBit getReject(SigBit *accept_sigptr = nullptr)
 	{
-		SigBit filtered_a = module->LogicAnd(NEW_ID, seq.sig_a, seq.sig_en);
-		SigBit other_filtered_a = module->LogicAnd(NEW_ID, other_a, other_en);
+		// Create unlinked NFSM
 
-		seq.length = -1;
-		seq.sig_a = module->LogicOr(NEW_ID, filtered_a, other_filtered_a);
-		seq.sig_en = module->LogicOr(NEW_ID, seq.sig_en, other_en);
-	}
+		unodes.resize(GetSize(nodes));
 
-	SigBit make_temporal_one_hot(SigBit enable = State::S1, SigBit *latched = nullptr)
-	{
-		Wire *state = module->addWire(NEW_ID);
-		state->attributes["\\init"] = State::S0;
+		for (int node = 0; node < GetSize(nodes); node++)
+			node_to_unode(node, node, SigSpec());
 
-		SigBit any = module->Anyseq(NEW_ID);
-		if (enable != State::S1)
-			any = module->LogicAnd(NEW_ID, any, enable);
+		mark_reachable_unode(startNode);
 
-		SigBit next_state = module->LogicOr(NEW_ID, state, any);
-		module->addDff(NEW_ID, clock, next_state, state, clock_posedge);
+		// Create DFSM
 
-		if (latched != nullptr)
-			*latched = state;
+		create_dnode(vector<int>{startNode}, true);
+		dnodes.sort();
 
-		SigBit not_state = module->LogicNot(NEW_ID, state);
-		return module->LogicAnd(NEW_ID, next_state, not_state);
-	}
+		// Create DFSM Circuit
 
-	SigBit make_permanent_latch(SigBit enable, bool async = false)
-	{
-		Wire *state = module->addWire(NEW_ID);
-		state->attributes["\\init"] = State::S0;
+		SigSpec accept_sig, reject_sig;
 
-		SigBit next_state = module->LogicOr(NEW_ID, state, enable);
-		module->addDff(NEW_ID, clock, next_state, state, clock_posedge);
+		for (auto &it : dnodes)
+		{
+			SvaDFsmNode &dnode = it.second;
+			dnode.ffoutwire = module->addWire(NEW_ID);
+			dnode.ffoutwire->attributes["\\init"] = Const(0, 1);
+			dnode.statesig = dnode.ffoutwire;
 
-		return async ? next_state : state;
-	}
+			if (it.first == vector<int>{startNode})
+				dnode.statesig = module->Or(NEW_ID, dnode.statesig, trigger_sig);
+		}
 
-	void parse_sequence(sequence_t &seq, Net *n)
-	{
-		Instance *inst = net_to_ast_driver(n);
+		for (auto &it : dnodes)
+		{
+			SvaDFsmNode &dnode = it.second;
 
-		// Regular expression
+			for (auto &edge : dnode.edges) {
+				SigBit trig = module->Eq(NEW_ID, {dnode.ctrl, dnode.statesig}, {edge.second, State::S1});
+				dnodes.at(edge.first).nextstate.append(trig);
+			}
 
-		if (inst == nullptr) {
-			sequence_cond(seq, importer->net_map_at(n));
-			return;
+			if (accept_sigptr) {
+				for (auto &value : dnode.accept)
+					accept_sig.append(module->Eq(NEW_ID, {dnode.ctrl, dnode.statesig}, {value, State::S1}));
+			}
+
+			for (auto &value : dnode.reject)
+				reject_sig.append(module->Eq(NEW_ID, {dnode.ctrl, dnode.statesig}, {value, State::S1}));
 		}
 
-		// SVA Primitives
+		for (auto &it : dnodes)
+		{
+			SvaDFsmNode &dnode = it.second;
+			if (GetSize(dnode.nextstate) == 0) {
+				module->connect(dnode.ffoutwire, State::S0);
+			} else
+			if (GetSize(dnode.nextstate) == 1) {
+				module->addDff(NEW_ID, clock, dnode.nextstate, dnode.ffoutwire, clockpol);
+			} else {
+				SigSpec nextstate = module->ReduceOr(NEW_ID, dnode.nextstate);
+				module->addDff(NEW_ID, clock, nextstate, dnode.ffoutwire, clockpol);
+			}
+		}
 
-		if (inst->Type() == PRIM_SVA_OVERLAPPED_IMPLICATION ||
-				inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION)
+		if (accept_sigptr)
 		{
-			Instance *consequent = get_ast_input2(inst);
-			bool linear_consequent = svatype(consequent).flag_linear;
+			if (GetSize(reject_sig) == 0)
+				*accept_sigptr = State::S0;
+			else if (GetSize(reject_sig) == 1)
+				*accept_sigptr = reject_sig;
+			else
+				*accept_sigptr = module->ReduceOr(NEW_ID, reject_sig);
+		}
 
-			parse_sequence(seq, inst->GetInput1());
-			seq.sig_en = module->And(NEW_ID, seq.sig_en, seq.sig_a);
+		if (GetSize(reject_sig) == 0)
+			return State::S0;
 
-			if (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION)
-				sequence_ff(seq);
+		if (GetSize(reject_sig) == 1)
+			return reject_sig;
+
+		return module->ReduceOr(NEW_ID, reject_sig);
+	}
 
-			if (!linear_consequent && mode_assume)
-				log_error("Non-linear consequent is currently not supported in SVA assumptions.\n");
+	// ----------------------------------------------------
+	// State dump for verbose log messages
 
-			if (linear_consequent)
+	void dump()
+	{
+		if (!nodes.empty())
+		{
+			log("      non-deterministic encoding:\n");
+			for (int i = 0; i < GetSize(nodes); i++)
 			{
-				parse_sequence(seq, inst->GetInput2());
+				log("        node %d:%s\n", i, i == startNode ? " [start]" : i == acceptNode ? " [accept]" : "");
+
+				for (auto &it : nodes[i].edges) {
+					if (it.second != State::S1)
+						log("          egde %s -> %d\n", log_signal(it.second), it.first);
+					else
+						log("          egde -> %d\n", it.first);
+				}
+
+				for (auto &it : nodes[i].links) {
+					if (it.second != State::S1)
+						log("          link %s -> %d\n", log_signal(it.second), it.first);
+					else
+						log("          link -> %d\n", it.first);
+				}
 			}
-			else
+		}
+
+		if (!unodes.empty())
+		{
+			log("      unlinked non-deterministic encoding:\n");
+			for (int i = 0; i < GetSize(unodes); i++)
 			{
-				SigBit activated;
-				seq.sig_en = make_temporal_one_hot(seq.sig_en, &activated);
+				if (!unodes[i].reachable)
+					continue;
+
+				log("        unode %d:%s\n", i, i == startNode ? " [start]" : "");
 
-				SigBit pass_latch_en = module->addWire(NEW_ID);
-				SigBit pass_latch = make_permanent_latch(pass_latch_en, true);
+				for (auto &it : unodes[i].edges) {
+					if (!it.second.empty())
+						log("          egde %s -> %d\n", log_signal(it.second), it.first);
+					else
+						log("          egde -> %d\n", it.first);
+				}
 
-				vector<SigBit> alive_list;
-				sva_sequence_alive_list.push_back(&alive_list);
-				parse_sequence(seq, inst->GetInput2());
-				sva_sequence_alive_list.pop_back();
+				for (auto &ctrl : unodes[i].accept) {
+					if (!ctrl.empty())
+						log("          accept %s\n", log_signal(ctrl));
+					else
+						log("          accept\n");
+				}
+			}
+		}
 
-				module->addLogicAnd(NEW_ID, seq.sig_a, seq.sig_en, pass_latch_en);
-				alive_list.push_back(pass_latch);
+		if (!dnodes.empty())
+		{
+			log("      deterministic encoding:\n");
+			for (auto &it : dnodes)
+			{
+				log("        dnode {");
+				for (int i = 0; i < GetSize(it.first); i++)
+					log("%s%d", i ? "," : "", it.first[i]);
+				log("}:%s\n", GetSize(it.first) == 1 && it.first[0] == startNode ? " [start]" : "");
+
+				log("          ctrl %s\n", log_signal(it.second.ctrl));
+
+				for (auto &edge : it.second.edges) {
+					log("          edge %s -> {", log_signal(edge.second));
+					for (int i = 0; i < GetSize(edge.first); i++)
+						log("%s%d", i ? "," : "", edge.first[i]);
+					log("}\n");
+				}
+
+				for (auto &value : it.second.accept)
+					log("          accept %s\n", log_signal(value));
 
-				seq.length = -1;
-				seq.sig_a = module->ReduceOr(NEW_ID, SigSpec(alive_list));
-				seq.sig_en = module->ReduceOr(NEW_ID, activated);
+				for (auto &value : it.second.reject)
+					log("          reject %s\n", log_signal(value));
 			}
+		}
+	}
+};
 
-			return;
+PRIVATE_NAMESPACE_END
+
+YOSYS_NAMESPACE_BEGIN
+
+pool<int> verific_sva_prims = {
+	// Copy&paste from Verific 3.16_484_32_170630 Netlist.h
+	PRIM_SVA_IMMEDIATE_ASSERT, PRIM_SVA_ASSERT, PRIM_SVA_COVER, PRIM_SVA_ASSUME,
+	PRIM_SVA_EXPECT, PRIM_SVA_POSEDGE, PRIM_SVA_NOT, PRIM_SVA_FIRST_MATCH,
+	PRIM_SVA_ENDED, PRIM_SVA_MATCHED, PRIM_SVA_CONSECUTIVE_REPEAT,
+	PRIM_SVA_NON_CONSECUTIVE_REPEAT, PRIM_SVA_GOTO_REPEAT,
+	PRIM_SVA_MATCH_ITEM_TRIGGER, PRIM_SVA_AND, PRIM_SVA_OR, PRIM_SVA_SEQ_AND,
+	PRIM_SVA_SEQ_OR, PRIM_SVA_EVENT_OR, PRIM_SVA_OVERLAPPED_IMPLICATION,
+	PRIM_SVA_NON_OVERLAPPED_IMPLICATION, PRIM_SVA_OVERLAPPED_FOLLOWED_BY,
+	PRIM_SVA_NON_OVERLAPPED_FOLLOWED_BY, PRIM_SVA_INTERSECT, PRIM_SVA_THROUGHOUT,
+	PRIM_SVA_WITHIN, PRIM_SVA_AT, PRIM_SVA_DISABLE_IFF, PRIM_SVA_SAMPLED,
+	PRIM_SVA_ROSE, PRIM_SVA_FELL, PRIM_SVA_STABLE, PRIM_SVA_PAST,
+	PRIM_SVA_MATCH_ITEM_ASSIGN, PRIM_SVA_SEQ_CONCAT, PRIM_SVA_IF,
+	PRIM_SVA_RESTRICT, PRIM_SVA_TRIGGERED, PRIM_SVA_STRONG, PRIM_SVA_WEAK,
+	PRIM_SVA_NEXTTIME, PRIM_SVA_S_NEXTTIME, PRIM_SVA_ALWAYS, PRIM_SVA_S_ALWAYS,
+	PRIM_SVA_S_EVENTUALLY, PRIM_SVA_EVENTUALLY, PRIM_SVA_UNTIL, PRIM_SVA_S_UNTIL,
+	PRIM_SVA_UNTIL_WITH, PRIM_SVA_S_UNTIL_WITH, PRIM_SVA_IMPLIES, PRIM_SVA_IFF,
+	PRIM_SVA_ACCEPT_ON, PRIM_SVA_REJECT_ON, PRIM_SVA_SYNC_ACCEPT_ON,
+	PRIM_SVA_SYNC_REJECT_ON, PRIM_SVA_GLOBAL_CLOCKING_DEF,
+	PRIM_SVA_GLOBAL_CLOCKING_REF, PRIM_SVA_IMMEDIATE_ASSUME,
+	PRIM_SVA_IMMEDIATE_COVER, OPER_SVA_SAMPLED, OPER_SVA_STABLE
+};
+
+struct VerificSvaImporter
+{
+	VerificImporter *importer = nullptr;
+	Module *module = nullptr;
+
+	Netlist *netlist = nullptr;
+	Instance *root = nullptr;
+
+	SigBit clock = State::Sx;
+	bool clockpol = false;
+
+	SigBit disable_iff = State::S0;
+
+	bool mode_assert = false;
+	bool mode_assume = false;
+	bool mode_cover = false;
+	bool eventually = false;
+	bool did_something = false;
+
+	Instance *net_to_ast_driver(Net *n)
+	{
+		if (n == nullptr)
+			return nullptr;
+
+		if (n->IsMultipleDriven())
+			return nullptr;
+
+		Instance *inst = n->Driver();
+
+		if (inst == nullptr)
+			return nullptr;
+
+		if (!verific_sva_prims.count(inst->Type()))
+			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)
+			return nullptr;
+
+		return inst;
+	}
+
+	Instance *get_ast_input(Instance *inst) { return net_to_ast_driver(inst->GetInput()); }
+	Instance *get_ast_input1(Instance *inst) { return net_to_ast_driver(inst->GetInput1()); }
+	Instance *get_ast_input2(Instance *inst) { return net_to_ast_driver(inst->GetInput2()); }
+	Instance *get_ast_input3(Instance *inst) { return net_to_ast_driver(inst->GetInput3()); }
+	Instance *get_ast_control(Instance *inst) { return net_to_ast_driver(inst->GetControl()); }
+
+	// ----------------------------------------------------------
+	// SVA Importer
+
+	int parse_sequence(SvaFsm *fsm, int start_node, Net *net)
+	{
+		Instance *inst = net_to_ast_driver(net);
+
+		if (inst == nullptr) {
+			int node = fsm->createNode();
+			fsm->createLink(start_node, node, importer->net_map_at(net));
+			return node;
 		}
 
 		if (inst->Type() == PRIM_SVA_SEQ_CONCAT)
@@ -416,34 +728,32 @@ struct VerificSvaImporter
 			int sva_high = atoi(sva_high_s);
 			bool sva_inf = !strcmp(sva_high_s, "$");
 
-			parse_sequence(seq, inst->GetInput1());
+			int node = parse_sequence(fsm, start_node, inst->GetInput1());
 
-			for (int i = 0; i < sva_low; i++)
-				sequence_ff(seq);
+			for (int i = 0; i < sva_low; i++) {
+				int next_node = fsm->createNode();
+				fsm->createEdge(node, next_node);
+				node = next_node;
+			}
 
 			if (sva_inf)
 			{
-				SigBit latched_a = module->addWire(NEW_ID);
-				SigBit latched_en = module->addWire(NEW_ID);
-				combine_seq(seq, latched_a, latched_en);
-
-				sequence_t seq_latched = seq;
-				sequence_ff(seq_latched);
-				module->connect(latched_a, seq_latched.sig_a);
-				module->connect(latched_en, seq_latched.sig_en);
+				fsm->createEdge(node, node);
 			}
 			else
 			{
 				for (int i = sva_low; i < sva_high; i++)
 				{
-					sequence_t last_seq = seq;
-					sequence_ff(seq);
-					combine_seq(seq, last_seq);
+					int next_node = fsm->createNode();
+					fsm->createEdge(node, next_node);
+					fsm->createLink(node, next_node);
+					node = next_node;
 				}
 			}
 
-			parse_sequence(seq, inst->GetInput2());
-			return;
+			node = parse_sequence(fsm, node, inst->GetInput2());
+
+			return node;
 		}
 
 		if (inst->Type() == PRIM_SVA_CONSECUTIVE_REPEAT)
@@ -455,64 +765,47 @@ struct VerificSvaImporter
 			int sva_high = atoi(sva_high_s);
 			bool sva_inf = !strcmp(sva_high_s, "$");
 
-			parse_sequence(seq, inst->GetInput());
+			int node = parse_sequence(fsm, start_node, inst->GetInput());
 
-			for (int i = 1; i < sva_low; i++) {
-				sequence_ff(seq);
-				parse_sequence(seq, inst->GetInput());
+			for (int i = 1; i < sva_low; i++)
+			{
+				int next_node = fsm->createNode();
+				fsm->createEdge(node, next_node);
+				node = parse_sequence(fsm, next_node, inst->GetInput());
 			}
 
 			if (sva_inf)
 			{
-				SigBit latched_a = module->addWire(NEW_ID);
-				SigBit latched_en = module->addWire(NEW_ID);
-				combine_seq(seq, latched_a, latched_en);
-
-				sequence_t seq_latched = seq;
-				sequence_ff(seq_latched);
-				parse_sequence(seq_latched, inst->GetInput());
-				module->connect(latched_a, seq_latched.sig_a);
-				module->connect(latched_en, seq_latched.sig_en);
+				int next_node = fsm->createNode();
+				fsm->createEdge(node, next_node);
+				next_node = parse_sequence(fsm, next_node, inst->GetInput());
+				fsm->createLink(next_node, node);
 			}
 			else
 			{
 				for (int i = sva_low; i < sva_high; i++)
 				{
-					sequence_t last_seq = seq;
-					sequence_ff(seq);
-					parse_sequence(seq, inst->GetInput());
-					combine_seq(seq, last_seq);
+					int next_node = fsm->createNode();
+					fsm->createEdge(node, next_node);
+					next_node = parse_sequence(fsm, next_node, inst->GetInput());
+					fsm->createLink(node, next_node);
+					node = next_node;
 				}
 			}
 
-			return;
+			return node;
 		}
 
-		if (inst->Type() == PRIM_SVA_THROUGHOUT || inst->Type() == PRIM_SVA_UNTIL || inst->Type() == PRIM_SVA_S_UNTIL ||
-				inst->Type() == PRIM_SVA_UNTIL_WITH || inst->Type() == PRIM_SVA_S_UNTIL_WITH)
+		if (inst->Type() == PRIM_SVA_THROUGHOUT)
 		{
-			bool flag_with = inst->Type() == PRIM_SVA_THROUGHOUT || inst->Type() == PRIM_SVA_UNTIL_WITH || inst->Type() == PRIM_SVA_S_UNTIL_WITH;
-
-			if (get_ast_input1(inst) != nullptr)
-				log_error("Currently only simple expression properties are supported as first operand to SVA_UNTIL.\n");
-
+			log_assert(get_ast_input1(inst) == nullptr);
 			SigBit expr = importer->net_map_at(inst->GetInput1());
 
-			if (flag_with)
-			{
-				seq.sig_a = module->LogicAnd(NEW_ID, seq.sig_a, expr);
-				sva_until_list_inclusive.push_back(expr);
-				parse_sequence(seq, inst->GetInput2());
-				sva_until_list_inclusive.pop_back();
-			}
-			else
-			{
-				sva_until_list_exclusive.push_back(expr);
-				parse_sequence(seq, inst->GetInput2());
-				sva_until_list_exclusive.pop_back();
-			}
+			fsm->pushThroughout(expr);
+			int node = parse_sequence(fsm, start_node, inst->GetInput2());
+			fsm->popThroughout();
 
-			return;
+			return node;
 		}
 
 		// Handle unsupported primitives
@@ -520,6 +813,8 @@ struct VerificSvaImporter
 		if (!importer->mode_keep)
 			log_error("Verific SVA primitive %s (%s) is currently unsupported in this context.\n", inst->View()->Owner()->Name(), inst->Name());
 		log_warning("Verific SVA primitive %s (%s) is currently unsupported in this context.\n", inst->View()->Owner()->Name(), inst->Name());
+
+		return start_node;
 	}
 
 	void import()
@@ -527,6 +822,10 @@ struct VerificSvaImporter
 		module = importer->module;
 		netlist = root->Owner();
 
+		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()));
+
 		RTLIL::IdString root_name = module->uniquify(importer->mode_names || root->IsUserDeclared() ? RTLIL::escape_id(root->Name()) : NEW_ID);
 
 		// parse SVA property clock event
@@ -557,25 +856,25 @@ struct VerificSvaImporter
 
 		VerificClockEdge clock_edge(importer, get_ast_input1(at_node));
 		clock = clock_edge.clock_sig;
-		clock_posedge = clock_edge.posedge;
+		clockpol = clock_edge.posedge;
 
 		// parse disable_iff expression
 
-		Net *sequence_net = at_node->GetInput2();
+		Net *net = at_node->GetInput2();
 
 		while (1)
 		{
-			Instance *sequence_node = net_to_ast_driver(sequence_net);
+			Instance *sequence_node = net_to_ast_driver(net);
 
 			if (sequence_node && sequence_node->Type() == PRIM_SVA_S_EVENTUALLY) {
 				eventually = true;
-				sequence_net = sequence_node->GetInput();
+				net = sequence_node->GetInput();
 				continue;
 			}
 
 			if (sequence_node && sequence_node->Type() == PRIM_SVA_DISABLE_IFF) {
 				disable_iff = importer->net_map_at(sequence_node->GetInput1());
-				sequence_net = sequence_node->GetInput2();
+				net = sequence_node->GetInput2();
 				continue;
 			}
 
@@ -584,51 +883,136 @@ struct VerificSvaImporter
 
 		// parse SVA sequence into trigger signal
 
-		sequence_t seq;
-		parse_sequence(seq, sequence_net);
-		sequence_ff(seq);
+		SigBit prop_okay;
+		Instance *inst = net_to_ast_driver(net);
+
+		if (inst == nullptr)
+		{
+			prop_okay = importer->net_map_at(net);
+		}
+		else
+		if (inst->Type() == PRIM_SVA_OVERLAPPED_IMPLICATION ||
+				inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION)
+		{
+			Net *antecedent_net = inst->GetInput1();
+			Net *consequent_net = inst->GetInput2();
+			int node;
+
+			SvaFsm antecedent_fsm(module, clock, clockpol, disable_iff);
+			node = parse_sequence(&antecedent_fsm, antecedent_fsm.startNode, antecedent_net);
+			if (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION) {
+				int next_node = antecedent_fsm.createNode();
+				antecedent_fsm.createEdge(node, next_node);
+				node = next_node;
+			}
+			antecedent_fsm.createLink(node, antecedent_fsm.acceptNode);
+
+			SigBit antecedent_match = antecedent_fsm.getAccept();
+
+			if (verific_verbose) {
+				log("    Antecedent FSM:\n");
+				antecedent_fsm.dump();
+			}
+
+			bool consequent_not = false;
+			Instance *consequent_inst = net_to_ast_driver(consequent_net);
+
+			if (consequent_inst && consequent_inst->Type() == PRIM_SVA_NOT) {
+				consequent_not = true;
+				consequent_net = consequent_inst->GetInput();
+			}
+
+			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))
+			{
+				bool until_with = consequent_inst->Type() == PRIM_SVA_UNTIL_WITH || consequent_inst->Type() == PRIM_SVA_S_UNTIL_WITH;
+				consequent_net = consequent_inst->GetInput1();
+				Net *until_net = consequent_inst->GetInput2();
+
+				SvaFsm until_fsm(module, clock, clockpol, disable_iff);
+				node = parse_sequence(&until_fsm, until_fsm.startNode, until_net);
+				if (until_with) {
+					int next_node = until_fsm.createNode();
+					until_fsm.createEdge(node, next_node);
+					node = next_node;
+				}
+				until_fsm.createLink(node, until_fsm.acceptNode);
+
+				SigBit until_match = until_fsm.getAccept();
+				SigBit not_until_match = module->Not(NEW_ID, until_match);
+
+				Wire *extend_antecedent_match_q = module->addWire(NEW_ID);
+				extend_antecedent_match_q->attributes["\\init"] = Const(0, 1);
+				antecedent_match = module->Or(NEW_ID, antecedent_match, extend_antecedent_match_q);
+
+				SigBit extend_antecedent_match = module->And(NEW_ID, not_until_match, antecedent_match);
+				module->addDff(NEW_ID, clock, extend_antecedent_match, extend_antecedent_match_q, clockpol);
+			}
+
+			SvaFsm consequent_fsm(module, clock, clockpol, disable_iff, antecedent_match);
+			node = parse_sequence(&consequent_fsm, consequent_fsm.startNode, consequent_net);
+			consequent_fsm.createLink(node, consequent_fsm.acceptNode);
+
+			if (mode_cover) {
+				prop_okay = consequent_not ? consequent_fsm.getReject() : consequent_fsm.getAccept();
+			} else {
+				SigBit consequent_match = consequent_not ? consequent_fsm.getAccept() : consequent_fsm.getReject();
+				prop_okay = module->Not(NEW_ID, consequent_match);
+			}
+
+			if (verific_verbose) {
+				log("    Consequent FSM:\n");
+				consequent_fsm.dump();
+			}
+		}
+		else
+		if (inst->Type() == PRIM_SVA_NOT || mode_cover)
+		{
+			SvaFsm fsm(module, clock, clockpol, disable_iff);
+			int node = parse_sequence(&fsm, fsm.startNode, mode_cover ? net : inst->GetInput());
+			fsm.createLink(node, fsm.acceptNode);
+			SigBit accept = fsm.getAccept();
+			prop_okay = module->Not(NEW_ID, accept);
+
+			if (verific_verbose) {
+				log("    Sequence FSM:\n");
+				fsm.dump();
+			}
+		}
+		else
+		{
+			// Handle unsupported primitives
+
+			if (!importer->mode_keep)
+				log_error("Verific SVA primitive %s (%s) is currently unsupported in this context.\n", inst->View()->Owner()->Name(), inst->Name());
+			log_warning("Verific SVA primitive %s (%s) is currently unsupported in this context.\n", inst->View()->Owner()->Name(), inst->Name());
+			return;
+		}
+
+		// add final FF stage
+
+		Wire *prop_okay_q = module->addWire(NEW_ID);
+		prop_okay_q->attributes["\\init"] = Const(mode_cover ? 0 : 1, 1);
+		module->addDff(NEW_ID, clock, prop_okay, prop_okay_q, clockpol);
 
 		// generate assert/assume/cover cell
 
 		RTLIL::Cell *c = nullptr;
 
 		if (eventually) {
-			if (mode_assert) c = module->addLive(root_name, seq.sig_a, seq.sig_en);
-			if (mode_assume) c = module->addFair(root_name, seq.sig_a, seq.sig_en);
+			log_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, seq.sig_a, seq.sig_en);
-			if (mode_assume) c = module->addAssume(root_name, seq.sig_a, seq.sig_en);
-			if (mode_cover) c = module->addCover(root_name, seq.sig_a, seq.sig_en);
+			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);
 		}
 
 		importer->import_attributes(c->attributes, root);
 	}
 };
 
-void svapp_assert(Instance *inst)
-{
-	VerificSvaImporter worker;
-	worker.root = inst;
-	worker.mode_assert = true;
-	worker.rewrite();
-}
-
-void svapp_assume(Instance *inst)
-{
-	VerificSvaImporter worker;
-	worker.root = inst;
-	worker.mode_assume = true;
-	worker.rewrite();
-}
-
-void svapp_cover(Instance *inst)
-{
-	VerificSvaImporter worker;
-	worker.root = inst;
-	worker.mode_cover = true;
-	worker.rewrite();
-}
-
 void import_sva_assert(VerificImporter *importer, Instance *inst)
 {
 	VerificSvaImporter worker;