SVA followed-by operators

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

Hide file tree

Showing 8 changed files with 46 additions and 7 deletions.
diff --git a/regression/verilog/SVA/sequence_followed_by1.desc b/regression/verilog/SVA/sequence_followed_by1.desc
@@ -0,0 +1,10 @@
+CORE
+sequence_followed_by1.sv
+--bound 20 --numbered-trace
+^\[main\.property\.1\] main\.x == 0 #=# \(main\.x == 1 #=# main\.x == 2\): FAILURE: property not supported by BMC engine$
+^\[main\.property\.2\] main\.x == 0 #-# \(\(##1 main\.x == 1\) #-# \(##1 main\.x == 2\)\): FAILURE: property not supported by BMC engine$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/verilog/SVA/sequence_followed_by1.sv b/regression/verilog/SVA/sequence_followed_by1.sv
@@ -0,0 +1,12 @@
+module main(input clk);
+
+  reg [31:0] x = 0;
+
+  always @(posedge clk)
+    x<=x+1;
+
+  initial p0: assert property (x == 0 #=# x == 1 #=# x == 2);
+
+  initial p0: assert property (x == 0 #-# ##1 x == 1 #-# ##1 x == 2);
+
+endmodule
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/temporal-logic/temporal_logic.cpp b/src/temporal-logic/temporal_logic.cpp
@@ -20,7 +20,9 @@ bool is_temporal_operator(const exprt &expr)
          expr.id() == ID_sva_until || expr.id() == ID_sva_s_until ||
          expr.id() == ID_sva_until_with || expr.id() == ID_sva_s_until_with ||
          expr.id() == ID_sva_eventually || expr.id() == ID_sva_s_eventually ||
-         expr.id() == ID_sva_cycle_delay;
+         expr.id() == ID_sva_cycle_delay ||
+         expr.id() == ID_sva_overlapped_followed_by ||
+         expr.id() == ID_sva_nonoverlapped_followed_by;
 }
 
 bool has_temporal_operator(const exprt &expr)

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
@@ -372,6 +372,8 @@ int yyverilogerror(const char *error)
 %token TOK_LESSLESSLESSEQUAL "<<<="
 %token TOK_GREATERGREATERGREATEREQUAL ">>>="
 %token TOK_HASHHASH         "##"
+%token TOK_HASHMINUSHASH    "#-#"
+%token TOK_HASHEQUALHASH    "#=#"
 %token TOK_COLONCOLON       "::"
 
 /* System Verilog Keywords */
@@ -2059,6 +2061,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/scanner.l b/src/verilog/scanner.l
@@ -258,6 +258,8 @@ void verilog_scanner_init()
 "<<<="          { SYSTEM_VERILOG_OPERATOR(TOK_LESSLESSLESSEQUAL, "<<<="); }
 ">>>="          { SYSTEM_VERILOG_OPERATOR(TOK_GREATERGREATERGREATEREQUAL, ">>>="); }
 "##"            { SYSTEM_VERILOG_OPERATOR(TOK_HASHHASH, "##"); }
+"#-#"           { SYSTEM_VERILOG_OPERATOR(TOK_HASHMINUSHASH, "#-#"); }
+"#=#"           { SYSTEM_VERILOG_OPERATOR(TOK_HASHEQUALHASH, "#=#"); }
 "<->"           { SYSTEM_VERILOG_OPERATOR(TOK_LESSMINUSGREATER, "<->"); }
 "->"            { SYSTEM_VERILOG_OPERATOR(TOK_MINUSGREATER, "->"); }
 "'"             { SYSTEM_VERILOG_OPERATOR('\'', "'"); }

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());