From 707ddb77bcb416399f7c61a2670731adbb97fc83 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Sat, 3 Mar 2018 16:34:28 +0100
Subject: Add SVA support for sequence OR

Signed-off-by: Clifford Wolf <clifford@clifford.at>
---
 frontends/verific/verificsva.cc | 55 ++++++++++++++++++++++++-----------------
 1 file changed, 33 insertions(+), 22 deletions(-)

(limited to 'frontends/verific/verificsva.cc')

diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc
index fd464909f..05d5b6577 100644
--- a/frontends/verific/verificsva.cc
+++ b/frontends/verific/verificsva.cc
@@ -18,13 +18,36 @@
  */
 
 
-// SVA Properties Simplified Syntax:
+// Currently supported property styles:
+//   seq
+//   not seq
+//   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:
+//   expr ##[N:M] seq
+//   seq or seq
+//   expr throughout seq
+//   seq [*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]
+//
+// -------------------------------------------------------
+//
+// SVA Properties Simplified Syntax (essentially a todo-list):
 //
 // prop:
 //   not prop
 //   prop or prop
 //   prop and prop
-//   seq |=> prop
+//   seq |-> prop
 //   if (expr) prop [else prop]
 //   always prop
 //   prop until prop
@@ -45,26 +68,6 @@
 //   seq [*N:M]
 //   expr [=N:M]
 //   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:
-//   seq
-//   not seq
-//   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:
-//   ##[N:M]
-//   [*N:M]
-//   throughout
 
 
 #include "kernel/yosys.h"
@@ -844,6 +847,14 @@ struct VerificSvaImporter
 			return node;
 		}
 
+		if (inst->Type() == PRIM_SVA_SEQ_OR)
+		{
+			int node = parse_sequence(fsm, start_node, inst->GetInput1());
+			int node2 = parse_sequence(fsm, start_node, inst->GetInput2());
+			fsm->createLink(node2, node);
+			return node;
+		}
+
 		if (inst->Type() == PRIM_SVA_THROUGHOUT)
 		{
 			log_assert(get_ast_input1(inst) == nullptr);
-- 
cgit v1.2.3