Introduce sva_sequence_repetition_exprt

This introduces sva_sequence_repetition_exprt as a base class for the SVA
repetition operators [*...], [=...], [->...].

Author: kroening

src/verilog/expr2verilog.cpp

@@ -608,31 +608,6 @@ 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_sequence_consecutive_repetition
 
   Inputs:
@@ -643,20 +618,27 @@ Function: expr2verilogt::convert_sva_sequence_consecutive_repetition
 
 \*******************************************************************/
 
-expr2verilogt::resultt
-expr2verilogt::convert_sva_sequence_consecutive_repetition(
-  const sva_sequence_consecutive_repetition_exprt &expr)
+expr2verilogt::resultt expr2verilogt::convert_sva_sequence_repetition(
+  const std::string &name,
+  const sva_sequence_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;
+  std::string dest = op.s + " [" + name;
+
+  if(expr.is_range())
+  {
+    dest += convert_rec(expr.from()).s;
 
-  if(expr.is_unbounded())
-    dest += ":$";
-  else if(expr.to().is_not_nil())
-    dest += ":" + convert_rec(expr.to()).s;
+    if(expr.is_unbounded())
+      dest += ":$";
+    else
+      dest += ":" + convert_rec(expr.to()).s;
+  }
+  else
+    dest += convert_rec(expr.repetitions()).s;
 
   dest += ']';
 
@@ -1877,20 +1859,16 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src)
   // not sure about precedence
 
   else if(src.id() == ID_sva_sequence_non_consecutive_repetition)
-    return precedence = verilog_precedencet::MIN,
-           convert_sva_binary_repetition(
-             "[=", to_sva_sequence_non_consecutive_repetition_expr(src));
-  // not sure about precedence
+    return convert_sva_sequence_repetition(
+      "=", to_sva_sequence_non_consecutive_repetition_expr(src));
 
   else if(src.id() == ID_sva_sequence_consecutive_repetition)
-    return convert_sva_sequence_consecutive_repetition(
-      to_sva_sequence_consecutive_repetition_expr(src));
+    return convert_sva_sequence_repetition(
+      "*", to_sva_sequence_consecutive_repetition_expr(src));
 
   else if(src.id() == ID_sva_sequence_goto_repetition)
-    return precedence = verilog_precedencet::MIN,
-           convert_sva_binary_repetition(
-             "[->", to_sva_sequence_goto_repetition_expr(src));
-  // not sure about precedence
+    return convert_sva_sequence_repetition(
+      "->", to_sva_sequence_goto_repetition_expr(src));
 
   else if(src.id() == ID_sva_ranged_always)
   {

src/verilog/expr2verilog_class.h

@@ -16,7 +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;
+class sva_sequence_repetition_exprt;
 class sva_sequence_first_match_exprt;
 
 // Precedences (higher means binds more strongly).
@@ -137,11 +137,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_sequence_consecutive_repetition(
-    const sva_sequence_consecutive_repetition_exprt &);
+  resultt convert_sva_sequence_repetition(
+    const std::string &name,
+    const sva_sequence_repetition_exprt &);
 
   resultt convert_sva_abort(const std::string &name, const sva_abort_exprt &);
 

src/verilog/parser.y

@@ -2707,12 +2707,28 @@ consecutive_repetition:
 
 non_consecutive_repetition:
 	  "[=" const_or_range_expression ']'
-		{ init($$, ID_sva_sequence_non_consecutive_repetition); mto($$, $2); }
+		{ init($$, ID_sva_sequence_non_consecutive_repetition);
+		  if(stack_expr($2).id() == ID_sva_cycle_delay)
+		    swapop($$, $2);
+		  else
+		  {
+		    mto($$, $2);
+		    stack_expr($$).add_to_operands(nil_exprt{});
+		  }
+		}
 	;
 
 goto_repetition:
 	  "[->" const_or_range_expression ']'
-		{ init($$, ID_sva_sequence_goto_repetition); mto($$, $2); }
+		{ init($$, ID_sva_sequence_goto_repetition);
+		  if(stack_expr($2).id() == ID_sva_cycle_delay)
+		    swapop($$, $2);
+		  else
+		  {
+		    mto($$, $2);
+		    stack_expr($$).add_to_operands(nil_exprt{});
+		  }
+		}
 	;
 
 cycle_delay_range:

src/verilog/sva_expr.cpp

@@ -44,10 +44,10 @@ exprt sva_sequence_consecutive_repetition_exprt::lower() const
   PRECONDITION(
     op().type().id() == ID_bool || op().type().id() == ID_verilog_sva_sequence);
 
-  if(to().is_nil())
+  if(!is_range())
   {
     // expand x[*n] into x ##1 x ##1 ...
-    auto n = numeric_cast_v<mp_integer>(to_constant_expr(from()));
+    auto n = numeric_cast_v<mp_integer>(repetitions());
     DATA_INVARIANT(n >= 1, "number of repetitions must be at least one");
 
     exprt result = op();
@@ -66,11 +66,11 @@ exprt sva_sequence_consecutive_repetition_exprt::lower() const
   {
     PRECONDITION(false);
   }
-  else
+  else // bounded range
   {
     // 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()));
+    auto from_int = numeric_cast_v<mp_integer>(from());
+    auto to_int = numeric_cast_v<mp_integer>(to());
 
     DATA_INVARIANT(from_int >= 1, "number of repetitions must be at least one");
     DATA_INVARIANT(