Continue refactoring of Verific SVA importer code

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

1 files changed, 139 insertions, 603 deletions

diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc
index ceaca287d..5857c4496 100644
--- a/frontends/verific/verificsva.cc
+++ b/frontends/verific/verificsva.cc
@@ -72,11 +72,23 @@ using namespace Verific;
 
 PRIVATE_NAMESPACE_BEGIN
 
-struct SvaFsmNode
+// 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;
 };
 
+// Non-deterministic FSM after resolving links
+struct SvaUFsmNode
+{
+	// 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;
+};
+
 struct SvaFsm
 {
 	Module *module;
@@ -91,8 +103,11 @@ struct SvaFsm
 	vector<SigBit> disable_stack;
 	vector<SigBit> throughout_stack;
 
-	int startNode, acceptNode, rejectNode;
-	vector<SvaFsmNode> nodes;
+	int startNode, acceptNode;
+	vector<SvaNFsmNode> nodes;
+
+	// ----------------------------------------------------
+	// API for creating FSM
 
 	SvaFsm(Module *mod, SigBit clk, bool clkpol, SigBit dis = State::S0, SigBit trig = State::S1)
 	{
@@ -104,7 +119,6 @@ struct SvaFsm
 
 		startNode = createNode();
 		acceptNode = createNode();
-		rejectNode = createNode();
 	}
 
 	void pushDisable(SigBit sig)
@@ -149,32 +163,12 @@ struct SvaFsm
 		throughout_stack.pop_back();
 	}
 
-	SigBit getAccept()
-	{
-		if (accept_sig != State::Sz)
-			return accept_sig;
-
-		log_assert(!materialized);
-		accept_sig = module->addWire(NEW_ID);
-		return accept_sig;
-	}
-
-	SigBit getReject()
-	{
-		if (reject_sig != State::Sz)
-			return reject_sig;
-
-		log_assert(!materialized);
-		reject_sig = module->addWire(NEW_ID);
-		return reject_sig;
-	}
-
 	int createNode()
 	{
 		log_assert(!materialized);
 
 		int idx = GetSize(nodes);
-		nodes.push_back(SvaFsmNode());
+		nodes.push_back(SvaNFsmNode());
 		return idx;
 	}
 
@@ -217,15 +211,19 @@ struct SvaFsm
 			make_link_order(order, it.first, order[node]+1);
 	}
 
-	void materialize_ndfsm()
+	// ----------------------------------------------------
+	// API for generating NFSM circuit to acquire accept signal
+
+	SigBit getAccept()
 	{
 		log_assert(!materialized);
 		materialized = true;
 
-		vector<SigBit> next_state_sig(GetSize(nodes));
+		vector<Wire*> state_wire(GetSize(nodes));
 		vector<SigBit> state_sig(GetSize(nodes));
+		vector<SigBit> next_state_sig(GetSize(nodes));
 
-		// Create state FFs
+		// Create state signals
 
 		{
 			SigBit not_disable = State::S1;
@@ -235,14 +233,10 @@ struct SvaFsm
 
 			for (int i = 0; i < GetSize(nodes); i++)
 			{
-				next_state_sig[i] = module->addWire(NEW_ID);
-
 				Wire *w = module->addWire(NEW_ID);
-				w->attributes["\\init"] = Const(0, 1);
+				state_wire[i] = w;
 				state_sig[i] = w;
 
-				module->addDff(NEW_ID, clock, next_state_sig[i], state_sig[i], clockpol);
-
 				if (i == startNode)
 					state_sig[i] = module->Or(NEW_ID, state_sig[i], trigger_sig);
 
@@ -295,86 +289,92 @@ struct SvaFsm
 
 			for (int i = 0; i < GetSize(nodes); i++) {
 				if (GetSize(activate_sig[i]) == 0)
-					activate_bit[i] = State::S0;
+					next_state_sig[i] = State::S0;
 				else if (GetSize(activate_sig[i]) == 1)
-					activate_bit[i] = activate_sig[i];
+					next_state_sig[i] = activate_sig[i];
 				else
-					activate_bit[i] = module->ReduceOr(NEW_ID, activate_sig[i]);
-			}
-
-			if (activate_bit[rejectNode] != State::S0)
-			{
-				SigBit not_rej = module->Not(NEW_ID, next_state_sig[rejectNode]);
-				for (int i = 0; i < GetSize(nodes); i++)
-					if (i != rejectNode && activate_bit[i] != State::S0)
-						activate_bit[i] = module->And(NEW_ID, activate_bit[i], not_rej);
-				activate_bit[rejectNode] = State::S0;
-			}
-
-			for (int i = 0; i < GetSize(nodes); i++) {
-				module->connect(next_state_sig[i], activate_bit[i]);
+					next_state_sig[i] = module->ReduceOr(NEW_ID, activate_sig[i]);
 			}
 		}
 
-		// Construct output signals
-
-		if (accept_sig != State::Sz) {
-			module->connect(accept_sig, state_sig[acceptNode]);
-		}
+		// Create state FFs
 
-		if (reject_sig != State::Sz)
+		for (int i = 0; i < GetSize(nodes); i++)
 		{
-			SigBit fsm_active = module->ReduceOr(NEW_ID, state_sig);
-			SigBit fsm_next_active = module->ReduceOr(NEW_ID, next_state_sig);
-			module->addEq(NEW_ID, {state_sig[acceptNode], fsm_next_active, fsm_active}, SigSpec(1, 3), reject_sig);
+			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 state_sig[acceptNode];
 	}
 
-	void materialize_dfsm()
+	// ----------------------------------------------------
+	// API for generating quantifier-based NFSM circuit to acquire reject signal
+
+	SigBit getAnyAllRejectWorker(bool allMode)
 	{
 		// FIXME
 		log_abort();
 	}
 
-	bool is_linear()
+	SigBit getAnyReject()
 	{
-		for (int i = 0; i < GetSize(nodes); i++)
-			if (GetSize(nodes[i].edges) + GetSize(nodes[i].links) > 1)
-				return false;
-		return true;
+		return getAnyAllRejectWorker(false);
+	}
+
+	SigBit getAllReject()
+	{
+		return getAnyAllRejectWorker(true);
+	}
+
+	// ----------------------------------------------------
+	// API for generating DFSM circuit to acquire reject signal
+
+	SigBit getReject()
+	{
+		// FIXME
+		log("-----------------\n");
+		dump();
+		log_abort();
 	}
 
+	// ----------------------------------------------------
+	// State dump for verbose log messages
+
 	void dump()
 	{
-		log("-----------\n");
-		for (int i = 0; i < GetSize(nodes); i++)
+		if (!nodes.empty())
 		{
-			log("node %d:\n", i);
-
-			if (i == startNode)
-				log("  startNode\n");
+			log("      non-deterministic encoding:\n");
+			for (int i = 0; i < GetSize(nodes); i++)
+			{
+				log("        node %d:\n", i);
 
-			if (i == rejectNode)
-				log("  rejectNode\n");
+				if (i == startNode)
+					log("          startNode\n");
 
-			if (i == acceptNode)
-				log("  acceptNode\n");
+				if (i == acceptNode)
+					log("          acceptNode\n");
 
-			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].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);
+				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);
+				}
 			}
 		}
-		log("-----------\n");
 	}
 };
 
@@ -414,7 +414,7 @@ struct VerificSvaImporter
 	Instance *root = nullptr;
 
 	SigBit clock = State::Sx;
-	bool clock_posedge = false;
+	bool clockpol = false;
 
 	SigBit disable_iff = State::S0;
 
@@ -454,124 +454,6 @@ struct VerificSvaImporter
 	Instance *get_ast_control(Instance *inst) { return net_to_ast_driver(inst->GetControl()); }
 
 	// ----------------------------------------------------------
-	// SVA AST Types
-
-	struct svatype_t
-	{
-		bool flag_linear = true;
-	};
-
-	std::map<Instance*, svatype_t> svatype_cache;
-
-	void svatype_visit_child(svatype_t &entry, Instance *inst)
-	{
-		if (inst == nullptr)
-			return;
-
-		const svatype_t &child_entry = svatype(inst);
-		entry.flag_linear &= child_entry.flag_linear;
-	}
-
-	const svatype_t &svatype(Instance *inst)
-	{
-		if (svatype_cache.count(inst) != 0)
-			return svatype_cache.at(inst);
-
-		svatype_t &entry = svatype_cache[inst];
-
-		if (inst == nullptr)
-			return entry;
-
-		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");
-
-			int sva_low = atoi(sva_low_s);
-			int sva_high = atoi(sva_high_s);
-			bool sva_inf = !strcmp(sva_high_s, "$");
-
-			if (sva_inf || sva_low != sva_high)
-				entry.flag_linear = false;
-		}
-
-		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;
-	}
-
-	// ----------------------------------------------------------
-	// SVA Preprocessor
-
-	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()); }
-
-	Net *rewrite(Instance *inst, Net *default_net = nullptr)
-	{
-		if (inst == nullptr)
-			return default_net;
-
-		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);
-			}
-			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);
-			}
-			return default_net;
-		}
-
-		if (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION)
-		{
-			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());
-			}
-			return default_net;
-		}
-
-		if (inst->Type() == PRIM_SVA_NOT)
-		{
-			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());
-			}
-			return default_net;
-		}
-
-		return default_net;
-	}
-
-	void rewrite()
-	{
-		netlist = root->Owner();
-		do {
-			did_something = false;
-			rewrite(root);
-		} while (did_something);
-	}
-
-	// ----------------------------------------------------------
 	// SVA Importer
 
 	int parse_sequence(SvaFsm *fsm, int start_node, Net *net)
@@ -687,6 +569,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
@@ -717,25 +603,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;
 			}
 
@@ -745,11 +631,11 @@ struct VerificSvaImporter
 		// parse SVA sequence into trigger signal
 
 		SigBit prop_okay;
-		Instance *inst = net_to_ast_driver(sequence_net);
+		Instance *inst = net_to_ast_driver(net);
 
 		if (inst == nullptr)
 		{
-			prop_okay = importer->net_map_at(sequence_net);
+			prop_okay = importer->net_map_at(net);
 		}
 		else
 		if (inst->Type() == PRIM_SVA_OVERLAPPED_IMPLICATION ||
@@ -759,7 +645,7 @@ struct VerificSvaImporter
 			Net *consequent_net = inst->GetInput2();
 			int node;
 
-			SvaFsm antecedent_fsm(module, clock, clock_posedge, disable_iff);
+			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();
@@ -768,21 +654,50 @@ struct VerificSvaImporter
 			}
 			antecedent_fsm.createLink(node, antecedent_fsm.acceptNode);
 
-			SigBit antecedent_accept = antecedent_fsm.getAccept();
-			antecedent_fsm.materialize_ndfsm();
-			antecedent_fsm.dump();
+			SigBit antecedent_match = antecedent_fsm.getAccept();
 
-			SvaFsm consequent_fsm(module, clock, clock_posedge, disable_iff, antecedent_accept);
+			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();
+			}
+
+			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);
 
-			SigBit consequent_reject = consequent_fsm.getReject();
-			prop_okay = module->Not(NEW_ID, consequent_reject);
+			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");
+				antecedent_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 (consequent_fsm.is_linear())
-				consequent_fsm.materialize_ndfsm();
-			else
-				log_error("Currently only linear sequences are allowed as impliciation consequent.\n");
+			if (verific_verbose) {
+				log("    Sequence FSM:\n");
+				fsm.dump();
+			}
 		}
 		else
 		{
@@ -798,7 +713,7 @@ struct VerificSvaImporter
 
 		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, clock_posedge);
+		module->addDff(NEW_ID, clock, prop_okay, prop_okay_q, clockpol);
 
 		// generate assert/assume/cover cell
 
@@ -816,387 +731,8 @@ struct VerificSvaImporter
 
 		importer->import_attributes(c->attributes, root);
 	}
-
-#if 0
-	// ----------------------------------------------------------
-	// Old SVA Importer
-
-	vector<SigBit> sva_until_list_inclusive;
-	vector<SigBit> sva_until_list_exclusive;
-	vector<vector<SigBit>*> sva_sequence_alive_list;
-
-	struct sequence_t {
-		int length = 0;
-		SigBit sig_a = State::S1;
-		SigBit sig_en = State::S1;
-	};
-
-	void sequence_cond(sequence_t &seq, SigBit cond)
-	{
-		seq.sig_a = module->And(NEW_ID, seq.sig_a, cond);
-	}
-
-	void sequence_ff(sequence_t &seq)
-	{
-		if (disable_iff != State::S0)
-			seq.sig_en = module->Mux(NEW_ID, seq.sig_en, State::S0, disable_iff);
-
-		for (auto &expr : sva_until_list_exclusive)
-			seq.sig_a = module->LogicAnd(NEW_ID, seq.sig_a, expr);
-
-		Wire *sig_a_q = module->addWire(NEW_ID);
-		sig_a_q->attributes["\\init"] = Const(0, 1);
-
-		Wire *sig_en_q = module->addWire(NEW_ID);
-		sig_en_q->attributes["\\init"] = Const(0, 1);
-
-		for (auto list : sva_sequence_alive_list)
-			list->push_back(module->LogicAnd(NEW_ID, seq.sig_a, seq.sig_en));
-
-		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);
-
-		if (seq.length >= 0)
-			seq.length++;
-
-		seq.sig_a = sig_a_q;
-		seq.sig_en = sig_en_q;
-
-		for (auto &expr : sva_until_list_inclusive)
-			seq.sig_a = module->LogicAnd(NEW_ID, seq.sig_a, expr);
-	}
-
-	void combine_seq(sequence_t &seq, const sequence_t &other_seq)
-	{
-		if (seq.length != other_seq.length)
-			seq.length = -1;
-
-		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);
-
-		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);
-	}
-
-	void combine_seq(sequence_t &seq, SigBit other_a, SigBit other_en)
-	{
-		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);
-
-		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);
-	}
-
-	SigBit make_temporal_one_hot(SigBit enable = State::S1, SigBit *latched = nullptr)
-	{
-		Wire *state = module->addWire(NEW_ID);
-		state->attributes["\\init"] = State::S0;
-
-		SigBit any = module->Anyseq(NEW_ID);
-		if (enable != State::S1)
-			any = module->LogicAnd(NEW_ID, any, enable);
-
-		SigBit next_state = module->LogicOr(NEW_ID, state, any);
-		module->addDff(NEW_ID, clock, next_state, state, clock_posedge);
-
-		if (latched != nullptr)
-			*latched = state;
-
-		SigBit not_state = module->LogicNot(NEW_ID, state);
-		return module->LogicAnd(NEW_ID, next_state, not_state);
-	}
-
-	SigBit make_permanent_latch(SigBit enable, bool async = false)
-	{
-		Wire *state = module->addWire(NEW_ID);
-		state->attributes["\\init"] = State::S0;
-
-		SigBit next_state = module->LogicOr(NEW_ID, state, enable);
-		module->addDff(NEW_ID, clock, next_state, state, clock_posedge);
-
-		return async ? next_state : state;
-	}
-
-	void parse_sequence(sequence_t &seq, Net *n)
-	{
-		Instance *inst = net_to_ast_driver(n);
-
-		// Regular expression
-
-		if (inst == nullptr) {
-			sequence_cond(seq, importer->net_map_at(n));
-			return;
-		}
-
-		// SVA Primitives
-
-		if (inst->Type() == PRIM_SVA_OVERLAPPED_IMPLICATION ||
-				inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION)
-		{
-			Instance *consequent = get_ast_input2(inst);
-			bool linear_consequent = svatype(consequent).flag_linear;
-
-			parse_sequence(seq, inst->GetInput1());
-			seq.sig_en = module->And(NEW_ID, seq.sig_en, seq.sig_a);
-
-			if (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION)
-				sequence_ff(seq);
-
-			if (!linear_consequent && mode_assume)
-				log_error("Non-linear consequent is currently not supported in SVA assumptions.\n");
-
-			if (linear_consequent)
-			{
-				parse_sequence(seq, inst->GetInput2());
-			}
-			else
-			{
-				SigBit activated;
-				seq.sig_en = make_temporal_one_hot(seq.sig_en, &activated);
-
-				SigBit pass_latch_en = module->addWire(NEW_ID);
-				SigBit pass_latch = make_permanent_latch(pass_latch_en, true);
-
-				vector<SigBit> alive_list;
-				sva_sequence_alive_list.push_back(&alive_list);
-				parse_sequence(seq, inst->GetInput2());
-				sva_sequence_alive_list.pop_back();
-
-				module->addLogicAnd(NEW_ID, seq.sig_a, seq.sig_en, pass_latch_en);
-				alive_list.push_back(pass_latch);
-
-				seq.length = -1;
-				seq.sig_a = module->ReduceOr(NEW_ID, SigSpec(alive_list));
-				seq.sig_en = module->ReduceOr(NEW_ID, activated);
-			}
-
-			return;
-		}
-
-		if (inst->Type() == PRIM_SVA_SEQ_CONCAT)
-		{
-			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);
-			bool sva_inf = !strcmp(sva_high_s, "$");
-
-			parse_sequence(seq, inst->GetInput1());
-
-			for (int i = 0; i < sva_low; i++)
-				sequence_ff(seq);
-
-			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);
-			}
-			else
-			{
-				for (int i = sva_low; i < sva_high; i++)
-				{
-					sequence_t last_seq = seq;
-					sequence_ff(seq);
-					combine_seq(seq, last_seq);
-				}
-			}
-
-			parse_sequence(seq, inst->GetInput2());
-			return;
-		}
-
-		if (inst->Type() == PRIM_SVA_CONSECUTIVE_REPEAT)
-		{
-			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);
-			bool sva_inf = !strcmp(sva_high_s, "$");
-
-			parse_sequence(seq, inst->GetInput());
-
-			for (int i = 1; i < sva_low; i++) {
-				sequence_ff(seq);
-				parse_sequence(seq, 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);
-			}
-			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);
-				}
-			}
-
-			return;
-		}
-
-		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)
-		{
-			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");
-
-			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();
-			}
-
-			return;
-		}
-
-		// 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());
-	}
-
-	void import()
-	{
-		module = importer->module;
-		netlist = root->Owner();
-
-		RTLIL::IdString root_name = module->uniquify(importer->mode_names || root->IsUserDeclared() ? RTLIL::escape_id(root->Name()) : NEW_ID);
-
-		// parse SVA property clock event
-
-		Instance *at_node = get_ast_input(root);
-
-		// asynchronous immediate assertion/assumption/cover
-		if (at_node == nullptr && (root->Type() == PRIM_SVA_IMMEDIATE_ASSERT ||
-				root->Type() == PRIM_SVA_IMMEDIATE_COVER || root->Type() == PRIM_SVA_IMMEDIATE_ASSUME))
-		{
-			SigSpec sig_a = importer->net_map_at(root->GetInput());
-			RTLIL::Cell *c = nullptr;
-
-			if (eventually) {
-				if (mode_assert) c = module->addLive(root_name, sig_a, State::S1);
-				if (mode_assume) c = module->addFair(root_name, sig_a, State::S1);
-			} else {
-				if (mode_assert) c = module->addAssert(root_name, sig_a, State::S1);
-				if (mode_assume) c = module->addAssume(root_name, sig_a, State::S1);
-				if (mode_cover) c = module->addCover(root_name, sig_a, State::S1);
-			}
-
-			importer->import_attributes(c->attributes, root);
-			return;
-		}
-
-		log_assert(at_node && at_node->Type() == PRIM_SVA_AT);
-
-		VerificClockEdge clock_edge(importer, get_ast_input1(at_node));
-		clock = clock_edge.clock_sig;
-		clock_posedge = clock_edge.posedge;
-
-		// parse disable_iff expression
-
-		Net *sequence_net = at_node->GetInput2();
-
-		while (1)
-		{
-			Instance *sequence_node = net_to_ast_driver(sequence_net);
-
-			if (sequence_node && sequence_node->Type() == PRIM_SVA_S_EVENTUALLY) {
-				eventually = true;
-				sequence_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();
-				continue;
-			}
-
-			break;
-		}
-
-		// parse SVA sequence into trigger signal
-
-		sequence_t seq;
-		parse_sequence(seq, sequence_net);
-		sequence_ff(seq);
-
-		// 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);
-		} 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);
-		}
-
-		importer->import_attributes(c->attributes, root);
-	}
-#endif
 };
 
-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;