Add support for SVA sequence concatenation ranges via verific

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

3 files changed, 144 insertions, 16 deletions

diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc
index 760f03e2f..c32095927 100644
--- a/frontends/verific/verificsva.cc
+++ b/frontends/verific/verificsva.cc
@@ -128,16 +128,16 @@ struct VerificSvaImporter
 		if (inst == nullptr)
 			return entry;
 
-		if (inst->Type() == PRIM_SVA_UNTIL || inst->Type() == PRIM_SVA_S_UNTIL ||
-				inst->Type() == PRIM_SVA_UNTIL_WITH || inst->Type() == PRIM_SVA_S_UNTIL_WITH)
-			entry.flag_linear = false;
-
 		if (inst->Type() == PRIM_SVA_SEQ_CONCAT || inst->Type() == PRIM_SVA_CONSECUTIVE_REPEAT)
 		{
-			int sva_low = atoi(inst->GetAttValue("sva:low"));
-			int sva_high = atoi(inst->GetAttValue("sva:high"));
+			const char *sva_low_s = inst->GetAttValue("sva:low");
+			const char *sva_high_s = inst->GetAttValue("sva:high");
 
-			if (sva_low != 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;
 		}
 
@@ -222,6 +222,7 @@ struct VerificSvaImporter
 
 	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;
@@ -248,10 +249,15 @@ struct VerificSvaImporter
 		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);
 
-		seq.length++;
+		if (seq.length >= 0)
+			seq.length++;
+
 		seq.sig_a = sig_a_q;
 		seq.sig_en = sig_en_q;
 
@@ -259,6 +265,58 @@ struct VerificSvaImporter
 			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);
@@ -287,33 +345,83 @@ struct VerificSvaImporter
 			if (!linear_consequent && mode_assume)
 				log_error("Non-linear consequent is currently not supported in SVA assumptions.\n");
 
-			parse_sequence(seq, inst->GetInput2());
+			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)
 		{
-			int sva_low = atoi(inst->GetAttValue("sva:low"));
-			int sva_high = atoi(inst->GetAttValue("sva:high"));
+			const char *sva_low_s = inst->GetAttValue("sva:low");
+			const char *sva_high_s = inst->GetAttValue("sva:high");
 
-			if (sva_low != sva_high)
-				log_error("Ranges on SVA sequence concatenation operator are not supported at the moment.\n");
+			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)
 		{
-			int sva_low = atoi(inst->GetAttValue("sva:low"));
-			int sva_high = atoi(inst->GetAttValue("sva:high"));
+			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_low != sva_high)
+			if (sva_inf || sva_low != sva_high)
 				log_error("Ranges on SVA consecutive repeat operator are not supported at the moment.\n");
 
 			parse_sequence(seq, inst->GetInput());
diff --git a/tests/sva/runtest.sh b/tests/sva/runtest.sh
index 4c8e16542..1b65ca9c9 100644
--- a/tests/sva/runtest.sh
+++ b/tests/sva/runtest.sh
@@ -35,6 +35,7 @@ generate_sby() {
 	cat <<- EOT
 		verific -import -extnets -all top
 		prep -top top
+		chformal -early -assume
 
 		[files]
 	EOT
diff --git a/tests/sva/sva_range.sv b/tests/sva/sva_range.sv
new file mode 100644
index 000000000..38199bff1
--- /dev/null
+++ b/tests/sva/sva_range.sv
@@ -0,0 +1,19 @@
+module top (
+	input clk,
+	input a, b, c, d
+);
+	default clocking @(posedge clk); endclocking
+
+	assert property (
+		a ##[*] b |=> c until ##[*] d
+	);
+
+`ifndef FAIL
+	assume property (
+		b |=> ##5 d
+	);
+	assume property (
+		b || (c && !d) |=> c
+	);
+`endif
+endmodule