From db323685a4357ae0a04a8def9de29ef3a8ba16c2 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Fri, 22 Nov 2019 16:11:56 +0100
Subject: [PATCH] Add Verific support for SVA nexttime properties
Signed-off-by: Clifford Wolf <clifford@clifford.at>
---
frontends/verific/verificsva.cc | 22 ++++++++++++++++++++++
1 file changed, 22 insertions(+)
diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc
index 225fd3e4a..49c0c40ac 100644
--- a/frontends/verific/verificsva.cc
+++ b/frontends/verific/verificsva.cc
@@ -36,6 +36,8 @@
// basic_property:
// sequence
// not basic_property
+// nexttime basic_property
+// nexttime[N] basic_property
// sequence #-# basic_property
// sequence #=# basic_property
// basic_property or basic_property (cover only)
@@ -1264,6 +1266,26 @@ struct VerificSvaImporter
return node;
}
+ if (inst->Type() == PRIM_SVA_NEXTTIME || inst->Type() == PRIM_SVA_S_NEXTTIME)
+ {
+ 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);
+ log_assert(sva_low == sva_high);
+
+ int node = start_node;
+
+ for (int i = 0; i < sva_low; i++) {
+ int next_node = fsm.createNode();
+ fsm.createEdge(node, next_node);
+ node = next_node;
+ }
+
+ return parse_sequence(fsm, node, inst->GetInput());
+ }
+
if (inst->Type() == PRIM_SVA_SEQ_CONCAT)
{
const char *sva_low_s = inst->GetAttValue("sva:low");