Merge pull request #530 from diffblue/SVA-followed-by

SVA followed-by operators

Author: kroening

regression/verilog/SVA/sequence_followed_by1.desc

@@ -0,0 +1,10 @@
+CORE
+sequence_followed_by1.sv
+--bound 20 --numbered-trace
+^\[main\.property\.p0\] main\.x == 0 #=# \(main\.x == 1 #=# main\.x == 2\): FAILURE: property not supported by BMC engine$
+^\[main\.property\.p1\] main\.x == 0 #-# \(\(##1 main\.x == 1\) #-# \(##1 main\.x == 2\)\): FAILURE: property not supported by BMC engine$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

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 p1: assert property (x == 0 #-# ##1 x == 1 #-# ##1 x == 2);
+
+endmodule

src/hw_cbmc_irep_ids.h

@@ -37,6 +37,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)

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)

src/verilog/expr2verilog.cpp

@@ -1162,6 +1162,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

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 */
@@ -2063,6 +2065,8 @@ property_expr_proper:
 		{ init($$, ID_sva_if); mto($$, $3); mto($$, $5); stack_expr($$).add_to_operands(nil_exprt()); }
         | "if" '(' expression_or_dist ')' property_expr "else" property_expr
 		{ init($$, ID_sva_if); mto($$, $3); mto($$, $5); mto($$, $7); }
+        | 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"

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('\'', "'"); }

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