SVA followed-by operators

This adds the SVA operators #=# and #-#.
diffblue · Jun 8, 2024 · 2af35ab · 2af35ab
1 parent 1d075d4
commit 2af35ab
Show file tree

Hide file tree

Showing 4 changed files with 17 additions and 6 deletions.
diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h
@@ -36,6 +36,8 @@ IREP_ID_ONE(sva_until)
 IREP_ID_ONE(sva_s_until)
 IREP_ID_ONE(sva_until_with)
 IREP_ID_ONE(sva_s_until_with)
+IREP_ID_ONE(sva_overlapped_followed_by)
+IREP_ID_ONE(sva_nonoverlapped_followed_by)
 IREP_ID_ONE(sva_overlapped_implication)
 IREP_ID_ONE(sva_non_overlapped_implication)
 IREP_ID_ONE(module_instance)

diff --git a/src/verilog/expr2verilog.cpp b/src/verilog/expr2verilog.cpp
@@ -1141,6 +1141,12 @@ std::string expr2verilogt::convert(
   else if(src.id() == ID_sva_cycle_delay_plus)
     return convert_sva_unary("##[+]", to_unary_expr(src));
 
+  else if(src.id() == ID_sva_overlapped_followed_by)
+    return precedence = 0, convert_sva_binary("#-#", to_binary_expr(src));
+
+  else if(src.id() == ID_sva_nonoverlapped_followed_by)
+    return precedence = 0, convert_sva_binary("#=#", to_binary_expr(src));
+
   else if(src.id()==ID_sva_cycle_delay)
     return convert_sva_cycle_delay(to_ternary_expr(src), precedence = 0);
     // not sure about precedence

diff --git a/src/verilog/parser.y b/src/verilog/parser.y
@@ -2059,6 +2059,8 @@ property_expr_proper:
         | property_expr "and" property_expr { init($$, ID_and); mto($$, $1); mto($$, $3); }
         | property_expr "|->" property_expr { init($$, ID_sva_overlapped_implication); mto($$, $1); mto($$, $3); }
         | property_expr "|=>" property_expr { init($$, ID_sva_non_overlapped_implication); mto($$, $1); mto($$, $3); }
+        | sequence_expr "#-#" property_expr { init($$, ID_sva_overlapped_followed_by); mto($$, $1); mto($$, $3); }
+        | sequence_expr "#=#" property_expr { init($$, ID_sva_nonoverlapped_followed_by); mto($$, $1); mto($$, $3); }
         | "nexttime" property_expr
 		{ init($$, "sva_nexttime"); stack_expr($$).add_to_operands(nil_exprt()); mto($$, $2); }
         | "nexttime" '[' constant_expression ']' property_expr %prec "nexttime"

diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp
@@ -2260,12 +2260,13 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr)
 
     return std::move(expr);
   }
-  else if(expr.id()==ID_sva_overlapped_implication ||
-          expr.id()==ID_sva_non_overlapped_implication ||
-          expr.id()==ID_sva_until ||
-          expr.id()==ID_sva_s_until ||
-          expr.id()==ID_sva_until_with ||
-          expr.id()==ID_sva_s_until_with)
+  else if(
+    expr.id() == ID_sva_overlapped_implication ||
+    expr.id() == ID_sva_non_overlapped_implication ||
+    expr.id() == ID_sva_overlapped_followed_by ||
+    expr.id() == ID_sva_nonoverlapped_followed_by ||
+    expr.id() == ID_sva_until || expr.id() == ID_sva_s_until ||
+    expr.id() == ID_sva_until_with || expr.id() == ID_sva_s_until_with)
   {
     convert_expr(expr.op0());
     make_boolean(expr.op0());