Merge pull request #1030 from diffblue/sequence_repetition5

SVA: consecutive repetition with range

Author: tautschnig

regression/verilog/SVA/sequence_repetition5.desc

@@ -0,0 +1,10 @@
+CORE
+sequence_repetition5.sv
+--bound 20
+^\[.*\] main\.pulse ##1 \!main\.pulse \[\*1:9\] ##1 main.pulse: PROVED up to bound 20$
+^\[.*\] main\.pulse ##1 \!main\.pulse \[\*1:8\] ##1 main.pulse: REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/SVA/sequence_repetition5.sv

@@ -0,0 +1,19 @@
+module main(input clk, input data);
+
+  reg [31:0] x = 0;
+
+  always_ff @(posedge clk)
+    if(x == 9 || (x >= 1 && data))
+      x = 0;
+    else
+      x++;
+
+  wire pulse = x == 0;
+
+  // should pass
+  initial p0: assert property (pulse ##1 !pulse[*1:9] ##1 pulse);
+
+  // should fail
+  initial p1: assert property (pulse ##1 !pulse[*1:8] ##1 pulse);
+
+endmodule

src/verilog/expr2verilog.cpp

@@ -582,6 +582,38 @@ expr2verilogt::resultt expr2verilogt::convert_sva_binary_repetition(
 
 /*******************************************************************\
 
+Function: expr2verilogt::convert_sva_sequence_consecutive_repetition
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+expr2verilogt::resultt
+expr2verilogt::convert_sva_sequence_consecutive_repetition(
+  const sva_sequence_consecutive_repetition_exprt &expr)
+{
+  auto op = convert_rec(expr.op());
+  if(op.p == verilog_precedencet::MIN)
+    op.s = "(" + op.s + ")";
+
+  std::string dest = op.s + " [*" + convert_rec(expr.from()).s;
+
+  if(expr.is_unbounded())
+    dest += ":$";
+  else if(expr.to().is_not_nil())
+    dest += ":" + convert_rec(expr.to()).s;
+
+  dest += ']';
+
+  return {verilog_precedencet::MIN, dest};
+}
+
+/*******************************************************************\
+
 Function: expr2verilogt::convert_sva_abort
 
   Inputs:
@@ -1797,9 +1829,8 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src)
   // not sure about precedence
 
   else if(src.id() == ID_sva_sequence_consecutive_repetition)
-    return precedence = verilog_precedencet::MIN,
-           convert_sva_binary_repetition("[*", to_binary_expr(src));
-  // not sure about precedence
+    return convert_sva_sequence_consecutive_repetition(
+      to_sva_sequence_consecutive_repetition_expr(src));
 
   else if(src.id() == ID_sva_sequence_goto_repetition)
     return precedence = verilog_precedencet::MIN,

src/verilog/expr2verilog_class.h

@@ -16,6 +16,7 @@ class sva_abort_exprt;
 class sva_case_exprt;
 class sva_if_exprt;
 class sva_ranged_predicate_exprt;
+class sva_sequence_consecutive_repetition_exprt;
 
 // Precedences (higher means binds more strongly).
 // Follows Table 11-2 in IEEE 1800-2017.
@@ -138,6 +139,9 @@ class expr2verilogt
   resultt
   convert_sva_binary_repetition(const std::string &name, const binary_exprt &);
 
+  resultt convert_sva_sequence_consecutive_repetition(
+    const sva_sequence_consecutive_repetition_exprt &);
+
   resultt convert_sva_abort(const std::string &name, const sva_abort_exprt &);
 
   resultt

src/verilog/parser.y

@@ -2653,7 +2653,15 @@ sequence_abbrev:
 
 consecutive_repetition:
 	  "[*" const_or_range_expression ']'
-		{ init($$, ID_sva_sequence_consecutive_repetition); mto($$, $2); }
+		{ init($$, ID_sva_sequence_consecutive_repetition);
+		  if(stack_expr($2).id() == ID_sva_cycle_delay)
+		    swapop($$, $2);
+		  else
+		  {
+		    mto($$, $2);
+		    stack_expr($$).add_to_operands(nil_exprt{});
+		  }
+		}
 	| "[*" ']'
 		{ init($$, ID_sva_sequence_repetition_star); }
 	| "[+" ']'

src/verilog/sva_expr.cpp

@@ -41,18 +41,50 @@ exprt sva_case_exprt::lowering() const
 
 exprt sva_sequence_consecutive_repetition_exprt::lower() const
 {
-  auto n = numeric_cast_v<mp_integer>(to_constant_expr(rhs()));
-  DATA_INVARIANT(n >= 1, "number of repetitions must be at least one");
+  PRECONDITION(op().type().id() == ID_bool);
 
-  exprt result = lhs();
+  if(to().is_nil())
+  {
+    // expand x[*n] into x ##1 x ##1 ...
+    auto n = numeric_cast_v<mp_integer>(to_constant_expr(from()));
+    DATA_INVARIANT(n >= 1, "number of repetitions must be at least one");
+
+    exprt result = op();
+
+    for(; n >= 2; --n)
+    {
+      auto cycle_delay =
+        sva_cycle_delay_exprt{from_integer(1, integer_typet{}), op()};
+      result = sva_sequence_concatenation_exprt{
+        std::move(result), std::move(cycle_delay)};
+    }
 
-  for(; n >= 2; --n)
+    return result;
+  }
+  else if(is_unbounded())
   {
-    auto cycle_delay =
-      sva_cycle_delay_exprt{from_integer(1, integer_typet{}), lhs()};
-    result = sva_sequence_concatenation_exprt{
-      std::move(result), std::move(cycle_delay)};
+    PRECONDITION(false);
   }
+  else
+  {
+    // expand x[*a:b] into x[*a] or x[*a+1] or ... or x[*b]
+    auto from_int = numeric_cast_v<mp_integer>(to_constant_expr(from()));
+    auto to_int = numeric_cast_v<mp_integer>(to_constant_expr(to()));
 
-  return result;
+    DATA_INVARIANT(from_int >= 1, "number of repetitions must be at least one");
+    DATA_INVARIANT(
+      to_int >= from_int, "number of repetitions must be interval");
+
+    exprt result = sva_sequence_consecutive_repetition_exprt{op(), from()};
+
+    for(mp_integer n = from_int + 1; n <= to_int; ++n)
+    {
+      auto n_expr = from_integer(n, integer_typet{});
+      result = sva_or_exprt{
+        std::move(result),
+        sva_sequence_consecutive_repetition_exprt{op(), n_expr}};
+    }
+
+    return result;
+  }
 }

src/verilog/sva_expr.h

@@ -1155,14 +1155,75 @@ inline sva_case_exprt &to_sva_case_expr(exprt &expr)
   return static_cast<sva_case_exprt &>(expr);
 }
 
-class sva_sequence_consecutive_repetition_exprt : public binary_predicate_exprt
+class sva_sequence_consecutive_repetition_exprt : public ternary_exprt
 {
 public:
+  sva_sequence_consecutive_repetition_exprt(exprt __op, exprt __repetitions)
+    : ternary_exprt{
+        ID_sva_sequence_consecutive_repetition,
+        std::move(__op),
+        std::move(__repetitions),
+        nil_exprt{},
+        bool_typet{}}
+  {
+  }
+
+  sva_sequence_consecutive_repetition_exprt(
+    exprt __op,
+    exprt __from,
+    exprt __to)
+    : ternary_exprt{
+        ID_sva_sequence_consecutive_repetition,
+        std::move(__op),
+        std::move(__from),
+        std::move(__to),
+        bool_typet{}}
+  {
+  }
+
   exprt lower() const;
 
+  const exprt &op() const
+  {
+    return op0();
+  }
+
+  exprt &op()
+  {
+    return op0();
+  }
+
+  const exprt &from() const
+  {
+    return op1();
+  }
+
+  exprt &from()
+  {
+    return op1();
+  }
+
+  // may be nil (just the singleton 'from') or
+  // infinity (half-open interval starting at 'from')
+  const exprt &to() const
+  {
+    return op2();
+  }
+
+  exprt &to()
+  {
+    return op2();
+  }
+
+  bool is_unbounded() const
+  {
+    return to().id() == ID_infinity;
+  }
+
 protected:
-  using binary_predicate_exprt::op0;
-  using binary_predicate_exprt::op1;
+  using ternary_exprt::op0;
+  using ternary_exprt::op1;
+  using ternary_exprt::op2;
 };
 
 inline const sva_sequence_consecutive_repetition_exprt &

src/verilog/verilog_typecheck_sva.cpp

@@ -137,7 +137,6 @@ exprt verilog_typecheck_exprt::convert_binary_sva(binary_exprt expr)
     return std::move(expr);
   }
   else if(
-    expr.id() == ID_sva_sequence_consecutive_repetition ||
     expr.id() == ID_sva_sequence_non_consecutive_repetition ||
     expr.id() == ID_sva_sequence_goto_repetition)
   {
@@ -208,6 +207,21 @@ exprt verilog_typecheck_exprt::convert_ternary_sva(ternary_exprt expr)
 
     return std::move(expr);
   }
+  else if(expr.id() == ID_sva_sequence_consecutive_repetition) // x[*1:2]
+  {
+    auto &repetition = to_sva_sequence_consecutive_repetition_expr(expr);
+
+    convert_sva(repetition.op());
+    make_boolean(repetition.op());
+
+    convert_expr(repetition.from());
+
+    if(repetition.to().is_not_nil())
+      convert_expr(repetition.to());
+
+    expr.type() = bool_typet{};
+    return std::move(expr);
+  }
   else if(
     expr.id() == ID_sva_eventually || expr.id() == ID_sva_ranged_s_eventually ||
     expr.id() == ID_sva_s_always || expr.id() == ID_sva_ranged_always)