Merge pull request #616 from diffblue/sequence-repetition

SystemVerilog: sequence repetition operators

Author: kroening

regression/verilog/SVA/sequence_repetition1.desc

@@ -0,0 +1,9 @@
+KNOWNBUG
+sequence_repetition1.sv
+--bound 10
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+currently not implemented

regression/verilog/SVA/sequence_repetition1.sv

@@ -0,0 +1,22 @@
+module main(input clk);
+
+  reg [31:0] x = 0;
+
+  // 0 1 2 3 4 ...
+  always_ff @(posedge clk)
+    x<=x+1;
+
+  // 0 0 1 1 2 2 3 3 ...
+  wire [31:0] half_x = x/2;
+
+  // should pass
+  initial p0: assert property (half_x==0[*2]);
+  initial p1: assert property (half_x==0[->2]);
+  initial p2: assert property (half_x==0[=2]);
+
+  // should fail
+  initial p3: assert property (x==0[*2]);
+  initial p4: assert property (x==0[->2]);
+  initial p5: assert property (x==0[=2]);
+
+endmodule

src/hw_cbmc_irep_ids.h

@@ -23,8 +23,13 @@ IREP_ID_ONE(sva_cycle_delay)
 IREP_ID_ONE(sva_cycle_delay_star)
 IREP_ID_ONE(sva_cycle_delay_plus)
 IREP_ID_ONE(sva_sequence_concatenation)
+IREP_ID_ONE(sva_sequence_consecutive_repetition)
 IREP_ID_ONE(sva_sequence_first_match)
+IREP_ID_ONE(sva_sequence_goto_repetition)
 IREP_ID_ONE(sva_sequence_intersect)
+IREP_ID_ONE(sva_sequence_non_consecutive_repetition)
+IREP_ID_ONE(sva_sequence_repetition_star)
+IREP_ID_ONE(sva_sequence_repetition_plus)
 IREP_ID_ONE(sva_sequence_throughout)
 IREP_ID_ONE(sva_sequence_within)
 IREP_ID_ONE(sva_always)

src/verilog/parser.y

@@ -375,6 +375,10 @@ int yyverilogerror(const char *error)
 %token TOK_HASHMINUSHASH    "#-#"
 %token TOK_HASHEQUALHASH    "#=#"
 %token TOK_COLONCOLON       "::"
+%token TOK_LSQASTERIC       "[*"
+%token TOK_LSQPLUS          "[+"
+%token TOK_LSQEQUAL         "[="
+%token TOK_LSQMINUSGREATER  "[->"
 
 /* System Verilog Keywords */
 %token TOK_ACCEPT_ON        "accept_on"
@@ -538,7 +542,7 @@ int yyverilogerror(const char *error)
 %left "and"
 %nonassoc "not" "nexttime" "s_nexttime"
 %left "##"
-%nonassoc "[*]" "[=]" "[->]"
+%nonassoc "[*" "[=" "[->"
 
 // Precendence of Verilog operators,
 // following System Verilog 1800-2017 Table 11-2.
@@ -2184,7 +2188,9 @@ expression_or_dist_brace:
 	;
 
 sequence_expr:
-          expression
+          expression_or_dist
+        | expression_or_dist boolean_abbrev
+		{ $$ = $2; mto($$, $1); }
         | cycle_delay_range sequence_expr
                 { $$=$1; mto($$, $2); }
         | expression cycle_delay_range sequence_expr
@@ -2199,17 +2205,51 @@ sequence_expr:
                 { init($$, ID_sva_sequence_within); mto($$, $1); mto($$, $3); }
         ;
 
+boolean_abbrev:
+	  consecutive_repetition
+	| non_consecutive_repetition
+	| goto_repetition
+	;
+
+sequence_abbrev:
+	  consecutive_repetition
+	;
+
+consecutive_repetition:
+	  "[*" const_or_range_expression ']'
+		{ init($$, ID_sva_sequence_consecutive_repetition); mto($$, $2); }
+	| "[*" ']'
+		{ init($$, ID_sva_sequence_repetition_star); }
+	| "[+" ']'
+		{ init($$, ID_sva_sequence_repetition_plus); }
+	;
+
+non_consecutive_repetition:
+	  "[=" const_or_range_expression ']'
+		{ init($$, ID_sva_sequence_non_consecutive_repetition); mto($$, $2); }
+	;
+
+goto_repetition:
+	  "[->" const_or_range_expression ']'
+		{ init($$, ID_sva_sequence_goto_repetition); mto($$, $2); }
+	;
+
 cycle_delay_range:
           "##" number
                 { init($$, ID_sva_cycle_delay); mto($$, $2); stack_expr($$).operands().push_back(nil_exprt()); }
         | "##" '[' cycle_delay_const_range_expression ']'
                 { $$ = $3; }
-        | "##" '[' TOK_ASTERIC ']'
+        | "##" "[*" ']'
                 { init($$, ID_sva_cycle_delay_star); }
-        | "##" '[' TOK_PLUS ']'
+        | "##" "[+" ']'
                 { init($$, ID_sva_cycle_delay_plus); }
         ;
 
+const_or_range_expression:
+	  constant_expression
+	| cycle_delay_const_range_expression
+	;
+
 cycle_delay_const_range_expression:
 	  constant_expression TOK_COLON constant_expression
                 { init($$, ID_sva_cycle_delay); mto($$, $1); mto($$, $3); }

src/verilog/scanner.l

@@ -264,6 +264,11 @@ void verilog_scanner_init()
 "->"            { SYSTEM_VERILOG_OPERATOR(TOK_MINUSGREATER, "->"); }
 "'"             { SYSTEM_VERILOG_OPERATOR('\'', "'"); }
 "::"            { SYSTEM_VERILOG_OPERATOR(TOK_COLONCOLON, "::"); }
+                /* Table 16-1 in 1800-2017 suggests the following tokens for sequence operators */
+"[*"            { SYSTEM_VERILOG_OPERATOR(TOK_LSQASTERIC, "[*"); }
+"[+"            { SYSTEM_VERILOG_OPERATOR(TOK_LSQPLUS, "[+"); }
+"[="            { SYSTEM_VERILOG_OPERATOR(TOK_LSQEQUAL, "[="); }
+"[->"           { SYSTEM_VERILOG_OPERATOR(TOK_LSQMINUSGREATER, "[->"); }
 
                 /* Verilog 1364-1995 keywords */
 

src/verilog/verilog_typecheck_expr.cpp

@@ -2163,6 +2163,16 @@ exprt verilog_typecheck_exprt::convert_unary_expr(unary_exprt expr)
     throw errort().with_location(expr.source_location())
       << "no support for 'first_match'";
   }
+  else if(expr.id() == ID_sva_sequence_repetition_plus)
+  {
+    throw errort().with_location(expr.source_location())
+      << "currently no support for [+]";
+  }
+  else if(expr.id() == ID_sva_sequence_repetition_star)
+  {
+    throw errort().with_location(expr.source_location())
+      << "currently no support for [*]";
+  }
   else if(expr.id() == ID_verilog_explicit_cast)
   {
     // SystemVerilog has got type'(expr). This is an explicit
@@ -2624,6 +2634,21 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr)
     expr.type() = bool_typet();
     return std::move(expr);
   }
+  else if(expr.id() == ID_sva_sequence_non_consecutive_repetition)
+  {
+    throw errort().with_location(expr.source_location())
+      << "currently no support for [=]";
+  }
+  else if(expr.id() == ID_sva_sequence_consecutive_repetition)
+  {
+    throw errort().with_location(expr.source_location())
+      << "currently no support for [*]";
+  }
+  else if(expr.id() == ID_sva_sequence_goto_repetition)
+  {
+    throw errort().with_location(expr.source_location())
+      << "currently no support for [->]";
+  }
   else
   {
     // type is guessed for now