Merge pull request #529 from diffblue/sequence3

Operators `##[*]` and `##[+]`

Author: tautschnig

regression/verilog/SVA/sequence3.sv

@@ -0,0 +1,15 @@
+module main;
+
+  reg [31:0] x;
+  wire clk;
+
+  initial x=0;
+
+  always @(posedge clk)
+    if(x < 5)
+      x<=x+1;
+
+  initial p0: assert property (##[*] x==6); // same as [0:$]
+  initial p1: assert property (##[+] x==0); // same as [1:$]
+
+endmodule

src/hw_cbmc_irep_ids.h

@@ -16,6 +16,8 @@ IREP_ID_ONE(E)
 IREP_ID_ONE(G)
 IREP_ID_ONE(X)
 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_first_match)
 IREP_ID_ONE(sva_sequence_intersect)

src/temporal-logic/normalize_property.cpp

@@ -117,6 +117,10 @@ exprt normalize_property(exprt expr)
     expr = X_exprt{to_sva_s_nexttime_expr(expr).op()};
   else if(expr.id() == ID_sva_cycle_delay)
     expr = normalize_pre_sva_cycle_delay(to_sva_cycle_delay_expr(expr));
+  else if(expr.id() == ID_sva_cycle_delay_plus)
+    expr = F_exprt{X_exprt{to_sva_cycle_delay_plus_expr(expr).op()}};
+  else if(expr.id() == ID_sva_cycle_delay_star)
+    expr = X_exprt{to_sva_cycle_delay_star_expr(expr).op()};
 
   // normalize the operands
   for(auto &op : expr.operands())

src/temporal-logic/normalize_property.h

@@ -24,6 +24,8 @@ Author: Daniel Kroening, dkr@amazon.com
 /// ¬¬φ --> φ
 /// ¬Gφ --> F¬φ
 /// ¬Fφ --> G¬φ
+/// [*] φ --> F φ
+/// [+] φ --> X F φ
 exprt normalize_property(exprt);
 
 #endif

src/verilog/expr2verilog.cpp

@@ -1106,6 +1106,12 @@ std::string expr2verilogt::convert(
   else if(src.id()==ID_sva_non_overlapped_implication)
     return precedence = 0, convert_sva_binary("|=>", to_binary_expr(src));
 
+  else if(src.id() == ID_sva_cycle_delay_star)
+    return convert_sva_unary("##[*]", to_unary_expr(src));
+
+  else if(src.id() == ID_sva_cycle_delay_plus)
+    return convert_sva_unary("##[+]", to_unary_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

@@ -2106,6 +2106,10 @@ cycle_delay_range:
                 { 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); }
         ;
 
 cycle_delay_const_range_expression:

src/verilog/sva_expr.h

@@ -521,4 +521,54 @@ static inline sva_cycle_delay_exprt &to_sva_cycle_delay_expr(exprt &expr)
   return static_cast<sva_cycle_delay_exprt &>(expr);
 }
 
+class sva_cycle_delay_plus_exprt : public unary_exprt
+{
+public:
+  explicit sva_cycle_delay_plus_exprt(exprt op)
+    : unary_exprt(ID_sva_cycle_delay_plus, std::move(op), bool_typet())
+  {
+  }
+};
+
+static inline const sva_cycle_delay_plus_exprt &
+to_sva_cycle_delay_plus_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_sva_cycle_delay_plus);
+  sva_cycle_delay_plus_exprt::check(expr);
+  return static_cast<const sva_cycle_delay_plus_exprt &>(expr);
+}
+
+static inline sva_cycle_delay_plus_exprt &
+to_sva_cycle_delay_plus_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_sva_cycle_delay_plus);
+  sva_cycle_delay_plus_exprt::check(expr);
+  return static_cast<sva_cycle_delay_plus_exprt &>(expr);
+}
+
+class sva_cycle_delay_star_exprt : public unary_exprt
+{
+public:
+  explicit sva_cycle_delay_star_exprt(exprt op)
+    : unary_exprt(ID_sva_cycle_delay_star, std::move(op), bool_typet())
+  {
+  }
+};
+
+static inline const sva_cycle_delay_star_exprt &
+to_sva_cycle_delay_star_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_sva_cycle_delay_star);
+  sva_cycle_delay_star_exprt::check(expr);
+  return static_cast<const sva_cycle_delay_star_exprt &>(expr);
+}
+
+static inline sva_cycle_delay_star_exprt &
+to_sva_cycle_delay_star_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_sva_cycle_delay_star);
+  sva_cycle_delay_star_exprt::check(expr);
+  return static_cast<sva_cycle_delay_star_exprt &>(expr);
+}
+
 #endif

src/verilog/verilog_typecheck_expr.cpp

@@ -1906,7 +1906,9 @@ exprt verilog_typecheck_exprt::convert_unary_expr(unary_exprt expr)
   }
   else if(
     expr.id() == ID_sva_always || expr.id() == ID_sva_nexttime ||
-    expr.id() == ID_sva_s_nexttime || expr.id() == ID_sva_s_eventually)
+    expr.id() == ID_sva_s_nexttime || expr.id() == ID_sva_s_eventually ||
+    expr.id() == ID_sva_cycle_delay_plus ||
+    expr.id() == ID_sva_cycle_delay_star)
   {
     assert(expr.operands().size()==1);
     convert_expr(expr.op());