SVA: consecutive repetition

regression/verilog/SVA/sequence_repetition1.desc

@@ -1,12 +1,12 @@
 CORE
 sequence_repetition1.sv
 --bound 10
-^\[.*\] 1 \[\*\] main\.half_x == 0: FAILURE: property not supported by BMC engine$
-^\[.*\] 1 \[->\] main\.half_x == 0: FAILURE: property not supported by BMC engine$
-^\[.*\] 1 \[=\] main\.half_x == 0: FAILURE: property not supported by BMC engine$
-^\[.*\] 1 \[\*\] main\.x == 0: FAILURE: property not supported by BMC engine$
-^\[.*\] 1 \[->\] main\.x == 0: FAILURE: property not supported by BMC engine$
-^\[.*\] 1 \[=\] main\.x == 0: FAILURE: property not supported by BMC engine$
+^\[.*\] main\.half_x == 0 \[\*2\]: PROVED up to bound 10$
+^\[.*\] main\.half_x == 0 \[->2\]: FAILURE: property not supported by BMC engine$
+^\[.*\] main\.half_x == 0 \[=2\]: FAILURE: property not supported by BMC engine$
+^\[.*\] main\.x == 0 \[\*2\]: REFUTED$
+^\[.*\] main\.x == 0 \[->2\]: FAILURE: property not supported by BMC engine$
+^\[.*\] main\.x == 0 \[=2\]: FAILURE: property not supported by BMC engine$
 ^EXIT=10$
 ^SIGNAL=0$
 --

regression/verilog/SVA/sequence_repetition3.desc

@@ -0,0 +1,11 @@
+CORE
+sequence_repetition3.sv
+--bound 10
+^\[main\.p0\] \(main\.x == 0 \[\*1\]\) #=# \(main\.x == 1 \[\*1\]\): PROVED up to bound 10$
+^\[main\.p1\] \(main\.half_x == 0 \[\*2\]\) #=# \(main\.half_x == 1 \[\*2\]\): PROVED up to bound 10$
+^\[main\.p2\] main\.half_x == 0 \[\*3\]: REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/SVA/sequence_repetition3.sv

@@ -0,0 +1,19 @@
+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 (x==0[*1] #=# x==1[*1]);
+  initial p1: assert property (half_x==0[*2] #=# half_x==1[*2]);
+
+  // should fail
+  initial p2: assert property (half_x==0[*3]);
+
+endmodule

src/trans-word-level/property.cpp

@@ -138,10 +138,6 @@ bool bmc_supports_SVA_property(const exprt &expr)
   if(has_subexpr(expr, ID_sva_sequence_non_consecutive_repetition))
     return false;
 
-  // sva_sequence_consecutive_repetition is not supported yet
-  if(has_subexpr(expr, ID_sva_sequence_consecutive_repetition))
-    return false;
-
   // sva_sequence_goto_repetition is not supported yet
   if(has_subexpr(expr, ID_sva_sequence_goto_repetition))
     return false;

src/trans-word-level/sequence.cpp

@@ -176,6 +176,12 @@ std::vector<std::pair<mp_integer, exprt>> instantiate_sequence(
 
     return result;
   }
+  else if(expr.id() == ID_sva_sequence_consecutive_repetition)
+  {
+    // x[*n] is syntactic sugar for x ##1 ... ##1 x, with n repetitions
+    auto &repetition = to_sva_sequence_consecutive_repetition_expr(expr);
+    return instantiate_sequence(repetition.lower(), t, no_timeframes);
+  }
   else
   {
     // not a sequence, evaluate as state predicate

src/verilog/expr2verilog.cpp

@@ -502,6 +502,31 @@ expr2verilogt::resultt expr2verilogt::convert_sva_binary(
 
 /*******************************************************************\
 
+Function: expr2verilogt::convert_sva_binary_repetition
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+expr2verilogt::resultt expr2verilogt::convert_sva_binary_repetition(
+  const std::string &name,
+  const binary_exprt &expr)
+{
+  auto op0 = convert_rec(expr.lhs());
+  if(op0.p == verilog_precedencet::MIN)
+    op0.s = "(" + op0.s + ")";
+
+  auto op1 = convert_rec(expr.rhs());
+
+  return {verilog_precedencet::MIN, op0.s + " " + name + op1.s + "]"};
+}
+
+/*******************************************************************\
+
 Function: expr2verilogt::convert_sva_abort
 
   Inputs:
@@ -1504,17 +1529,17 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src)
 
   else if(src.id() == ID_sva_sequence_non_consecutive_repetition)
     return precedence = verilog_precedencet::MIN,
-           convert_sva_binary("[=]", to_binary_expr(src));
+           convert_sva_binary_repetition("[=", to_binary_expr(src));
   // not sure about precedence
 
   else if(src.id() == ID_sva_sequence_consecutive_repetition)
     return precedence = verilog_precedencet::MIN,
-           convert_sva_binary("[*]", to_binary_expr(src));
+           convert_sva_binary_repetition("[*", to_binary_expr(src));
   // not sure about precedence
 
   else if(src.id() == ID_sva_sequence_goto_repetition)
     return precedence = verilog_precedencet::MIN,
-           convert_sva_binary("[->]", to_binary_expr(src));
+           convert_sva_binary_repetition("[->", to_binary_expr(src));
   // not sure about precedence
 
   else if(src.id() == ID_sva_ranged_always)

src/verilog/expr2verilog_class.h

@@ -124,6 +124,9 @@ class expr2verilogt
 
   resultt convert_sva_binary(const std::string &name, const binary_exprt &);
 
+  resultt
+  convert_sva_binary_repetition(const std::string &name, const binary_exprt &);
+
   resultt convert_sva_abort(const std::string &name, const sva_abort_exprt &);
 
   resultt

src/verilog/parser.y

@@ -2262,7 +2262,10 @@ expression_or_dist_brace:
 sequence_expr:
           expression_or_dist
         | expression_or_dist boolean_abbrev
-		{ $$ = $2; mto($$, $1); }
+		{ $$ = $2;
+		  // preserve the operand ordering as in the source code
+		  stack_expr($$).operands().insert(stack_expr($$).operands().begin(), stack_expr($1));
+		}
         | cycle_delay_range sequence_expr
                 { $$=$1; mto($$, $2); }
         | expression cycle_delay_range sequence_expr

src/verilog/sva_expr.cpp

@@ -8,6 +8,9 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "sva_expr.h"
 
+#include <util/arith_tools.h>
+#include <util/mathematical_types.h>
+
 exprt sva_case_exprt::lowering() const
 {
   auto &case_items = this->case_items();
@@ -35,3 +38,21 @@ exprt sva_case_exprt::lowering() const
   return if_exprt{
     disjunction(disjuncts), case_items.front().result(), reduced_rec};
 }
+
+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");
+
+  exprt result = lhs();
+
+  for(; n >= 2; --n)
+  {
+    auto cycle_delay =
+      sva_cycle_delay_exprt{from_integer(1, integer_typet{}), lhs()};
+    result = sva_sequence_concatenation_exprt{
+      std::move(cycle_delay), std::move(result)};
+  }
+
+  return result;
+}

src/verilog/sva_expr.h

@@ -1155,4 +1155,30 @@ 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
+{
+public:
+  exprt lower() const;
+
+protected:
+  using binary_predicate_exprt::op0;
+  using binary_predicate_exprt::op1;
+};
+
+inline const sva_sequence_consecutive_repetition_exprt &
+to_sva_sequence_consecutive_repetition_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_sva_sequence_consecutive_repetition);
+  sva_sequence_consecutive_repetition_exprt::check(expr);
+  return static_cast<const sva_sequence_consecutive_repetition_exprt &>(expr);
+}
+
+inline sva_sequence_consecutive_repetition_exprt &
+to_sva_sequence_consecutive_repetition_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_sva_sequence_consecutive_repetition);
+  sva_sequence_consecutive_repetition_exprt::check(expr);
+  return static_cast<sva_sequence_consecutive_repetition_exprt &>(expr);
+}
+
 #endif

src/verilog/verilog_typecheck_expr.cpp

@@ -1716,6 +1716,35 @@ exprt verilog_typecheck_exprt::elaborate_constant_expression_check(exprt expr)
 
 /*******************************************************************\
 
+Function: verilog_typecheck_exprt::elaborate_constant_integer_expression
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+mp_integer
+verilog_typecheck_exprt::elaborate_constant_integer_expression(exprt expr)
+{
+  source_locationt source_location = expr.find_source_location();
+
+  exprt tmp = elaborate_constant_expression(std::move(expr));
+
+  if(!tmp.is_constant())
+  {
+    throw errort().with_location(source_location)
+      << "expected constant integer expression, but got `" << to_string(tmp)
+      << '\'';
+  }
+
+  return numeric_cast_v<mp_integer>(to_constant_expr(tmp));
+}
+
+/*******************************************************************\
+
 Function: verilog_typecheck_exprt::elaborate_constant_system_function_call
 
   Inputs:
@@ -2969,17 +2998,37 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr)
   else if(
     expr.id() == ID_sva_sequence_intersect ||
     expr.id() == ID_sva_sequence_throughout ||
-    expr.id() == ID_sva_sequence_within ||
-    expr.id() == ID_sva_sequence_non_consecutive_repetition ||
+    expr.id() == ID_sva_sequence_within)
+  {
+    auto &binary_expr = to_binary_expr(expr);
+
+    convert_expr(binary_expr.lhs());
+    make_boolean(binary_expr.lhs());
+    convert_expr(binary_expr.rhs());
+    make_boolean(binary_expr.rhs());
+
+    expr.type() = bool_typet();
+
+    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)
   {
     auto &binary_expr = to_binary_expr(expr);
 
     convert_expr(binary_expr.lhs());
     make_boolean(binary_expr.lhs());
+
     convert_expr(binary_expr.rhs());
-    make_boolean(binary_expr.rhs());
+
+    mp_integer n = elaborate_constant_integer_expression(binary_expr.rhs());
+    if(n < 0)
+      throw errort().with_location(binary_expr.rhs().source_location())
+        << "number of repetitions must not be negative";
+
+    binary_expr.rhs() = from_integer(n, integer_typet{});
 
     expr.type() = bool_typet();
 

src/verilog/verilog_typecheck_expr.h

@@ -156,6 +156,7 @@ class verilog_typecheck_exprt:public verilog_typecheck_baset
   std::optional<mp_integer> is_constant_integer_post_convert(const exprt &);
   exprt elaborate_constant_expression(exprt);
   exprt elaborate_constant_expression_check(exprt);
+  mp_integer elaborate_constant_integer_expression(exprt);
 
   // To be overridden, requires a Verilog interpreter.
   virtual exprt elaborate_constant_function_call(const function_call_exprt &)