SVA's [->x:y] and [*x:y]

kroening · kroening · commit fd9b801bd766 · 2025-04-22T21:21:12.000-07:00
Both the goto repetition operator and the consecutive repetition operator
can either take a singleton number of repetition or a range.

This adds support for the range case.
diff --git a/src/trans-word-level/sequence.cpp b/src/trans-word-level/sequence.cpp
@@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/arith_tools.h>
 #include <util/ebmc_util.h>
+#include <util/std_expr.h>
 
 #include <temporal-logic/temporal_logic.h>
 #include <verilog/sva_expr.h>
@@ -18,6 +19,39 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "obligations.h"
 #include "property.h"
 
+exprt sequence_count_condition(
+  const sva_sequence_repetition_exprt &expr,
+  const exprt &counter)
+{
+  if(expr.is_range())
+  {
+    // number of repetitions inside a range
+    auto lower = numeric_cast_v<mp_integer>(
+      expr.lower());
+
+    if(expr.is_unbounded())
+    {
+      return binary_relation_exprt{counter, ID_ge, from_integer(lower, counter.type())};
+    }
+    else
+    {
+      auto upper = numeric_cast_v<mp_integer>(
+        to_constant_expr(expr.upper()));
+
+      return and_exprt{binary_relation_exprt{counter, ID_ge, from_integer(lower, counter.type())},
+        binary_relation_exprt{counter, ID_le, from_integer(upper, counter.type())}};
+    }
+  }
+  else
+  {
+    // fixed number of repetitions
+    auto repetitions_int = numeric_cast_v<mp_integer>(
+      expr.repetitions());
+
+    return equal_exprt{counter, from_integer(repetitions_int, counter.type())};
+  }
+}
+
 sequence_matchest instantiate_sequence(
   exprt expr,
   const mp_integer &t,
@@ -311,11 +345,8 @@ sequence_matchest instantiate_sequence(
   }
   else if(expr.id() == ID_sva_sequence_goto_repetition)
   {
-    // The 'op' is a Boolean condition, not a sequence.
-    auto &op = to_sva_sequence_goto_repetition_expr(expr).op();
-    auto repetitions_int = numeric_cast_v<mp_integer>(
-      to_sva_sequence_goto_repetition_expr(expr).repetitions());
-    PRECONDITION(repetitions_int >= 1);
+    auto &repetition = to_sva_sequence_goto_repetition_expr(expr);
+    auto &condition = repetition.condition();
 
     sequence_matchest result;
 
@@ -324,32 +355,28 @@ sequence_matchest instantiate_sequence(
     const auto bits = address_bits(no_timeframes);
     const auto zero = from_integer(0, unsignedbv_typet{bits});
     const auto one = from_integer(1, unsignedbv_typet{bits});
-    const auto repetitions = from_integer(repetitions_int, zero.type());
     exprt matches = zero;
 
     for(mp_integer u = t; u < no_timeframes; ++u)
     {
       // match of op in timeframe u?
-      auto rec_op = instantiate(op, u, no_timeframes);
+      auto rec_op = instantiate(condition, u, no_timeframes);
 
       // add up
       matches = plus_exprt{matches, if_exprt{rec_op, one, zero}};
 
       // We have a match for op[->n] if there is a match in timeframe
       // u and matches is n.
       result.emplace_back(
-        u, and_exprt{rec_op, equal_exprt{matches, repetitions}});
+        u, sequence_count_condition(repetition, matches));
     }
 
     return result;
   }
   else if(expr.id() == ID_sva_sequence_non_consecutive_repetition)
   {
-    // The 'op' is a Boolean condition, not a sequence.
-    auto &op = to_sva_sequence_non_consecutive_repetition_expr(expr).op();
-    auto repetitions_int = numeric_cast_v<mp_integer>(
-      to_sva_sequence_non_consecutive_repetition_expr(expr).repetitions());
-    PRECONDITION(repetitions_int >= 1);
+    auto &repetition = to_sva_sequence_non_consecutive_repetition_expr(expr);
+    auto &condition = repetition.condition();
 
     sequence_matchest result;
 
@@ -358,19 +385,18 @@ sequence_matchest instantiate_sequence(
     const auto bits = address_bits(no_timeframes);
     const auto zero = from_integer(0, unsignedbv_typet{bits});
     const auto one = from_integer(1, zero.type());
-    const auto repetitions = from_integer(repetitions_int, zero.type());
     exprt matches = zero;
 
     for(mp_integer u = t; u < no_timeframes; ++u)
     {
       // match of op in timeframe u?
-      auto rec_op = instantiate(op, u, no_timeframes);
+      auto rec_op = instantiate(condition, u, no_timeframes);
 
       // add up
       matches = plus_exprt{matches, if_exprt{rec_op, one, zero}};
 
       // We have a match for op[=n] if matches is n.
-      result.emplace_back(u, equal_exprt{matches, repetitions});
+      result.emplace_back(u, sequence_count_condition(repetition, matches));
     }
 
     return result;
diff --git a/src/verilog/expr2verilog.cpp b/src/verilog/expr2verilog.cpp
@@ -608,7 +608,7 @@ expr2verilogt::resultt expr2verilogt::convert_sva_binary(
 
 /*******************************************************************\
 
-Function: expr2verilogt::convert_sva_binary_repetition
+Function: expr2verilogt::convert_sva_sequence_repetition
 
   Inputs:
 
@@ -618,17 +618,26 @@ Function: expr2verilogt::convert_sva_binary_repetition
 
 \*******************************************************************/
 
-expr2verilogt::resultt expr2verilogt::convert_sva_binary_repetition(
+expr2verilogt::resultt expr2verilogt::convert_sva_sequence_repetition(
   const std::string &name,
-  const binary_exprt &expr)
+  const sva_sequence_repetition_exprt &expr)
 {
-  auto op0 = convert_rec(expr.lhs());
-  if(op0.p == verilog_precedencet::MIN)
-    op0.s = "(" + op0.s + ")";
+  auto condition = convert_rec(expr.condition());
 
-  auto op1 = convert_rec(expr.rhs());
+  if(condition.p == verilog_precedencet::MIN)
+    condition.s = "(" + condition.s + ")";
+
+  if(expr.is_range())
+  {
+    PRECONDITION(false);
+  }
+  else
+  {
+    auto repetitions = convert_rec(expr.repetitions());
 
-  return {verilog_precedencet::MIN, op0.s + " " + name + op1.s + "]"};
+    return {
+      verilog_precedencet::MIN, condition.s + " " + name + repetitions.s + "]"};
+  }
 }
 
 /*******************************************************************\
@@ -1878,7 +1887,7 @@ 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_repetition(
+           convert_sva_sequence_repetition(
              "[=", to_sva_sequence_non_consecutive_repetition_expr(src));
   // not sure about precedence
 
@@ -1888,7 +1897,7 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src)
 
   else if(src.id() == ID_sva_sequence_goto_repetition)
     return precedence = verilog_precedencet::MIN,
-           convert_sva_binary_repetition(
+           convert_sva_sequence_repetition(
              "[->", to_sva_sequence_goto_repetition_expr(src));
   // not sure about precedence
 
diff --git a/src/verilog/expr2verilog_class.h b/src/verilog/expr2verilog_class.h
@@ -17,6 +17,7 @@ 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,8 +138,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_repetition(
+    const std::string &name,
+    const sva_sequence_repetition_exprt &);
 
   resultt convert_sva_sequence_consecutive_repetition(
     const sva_sequence_consecutive_repetition_exprt &);
diff --git a/src/verilog/parser.y b/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:
diff --git a/src/verilog/sva_expr.h b/src/verilog/sva_expr.h
@@ -1364,24 +1364,29 @@ to_sva_sequence_consecutive_repetition_expr(exprt &expr)
   return static_cast<sva_sequence_consecutive_repetition_exprt &>(expr);
 }
 
-class sva_sequence_goto_repetition_exprt : public binary_exprt
+/// [->...] and [*...]
+class sva_sequence_repetition_exprt : public ternary_exprt
 {
 public:
-  sva_sequence_goto_repetition_exprt(exprt __op, constant_exprt __repetitions)
-    : binary_exprt{
+  sva_sequence_repetition_exprt(
+    irep_idt __id,
+    exprt __op,
+    constant_exprt __repetitions)
+    : ternary_exprt{
+        __id,
         std::move(__op),
-        ID_sva_sequence_goto_repetition,
         std::move(__repetitions),
-        bool_typet{}}
+        nil_exprt{},
+        verilog_sva_sequence_typet{}}
   {
   }
 
-  const exprt &op() const
+  const exprt &condition() const
   {
     return op0();
   }
 
-  exprt &op()
+  exprt &condition()
   {
     return op0();
   }
@@ -1397,9 +1402,67 @@ class sva_sequence_goto_repetition_exprt : public binary_exprt
     return static_cast<constant_exprt &>(op1());
   }
 
+  bool is_range() const
+  {
+    return upper().is_not_nil();
+  }
+
+  bool is_unbounded() const
+  {
+    return upper().id() == ID_infinity;
+  }
+
+  const constant_exprt &lower() const
+  {
+    return static_cast<const constant_exprt &>(op1());
+  }
+
+  constant_exprt &lower()
+  {
+    return static_cast<constant_exprt &>(op1());
+  }
+
+  // might be $
+  const exprt &upper() const
+  {
+    return op2();
+  }
+
+  exprt &upper()
+  {
+    return op2();
+  }
+
 protected:
-  using binary_exprt::op0;
-  using binary_exprt::op1;
+  using ternary_exprt::op0;
+  using ternary_exprt::op1;
+  using ternary_exprt::op2;
+};
+
+inline const sva_sequence_repetition_exprt &
+to_sva_sequence_repetition_expr(const exprt &expr)
+{
+  sva_sequence_repetition_exprt::check(expr);
+  return static_cast<const sva_sequence_repetition_exprt &>(expr);
+}
+
+inline sva_sequence_repetition_exprt &
+to_sva_sequence_repetition_expr(exprt &expr)
+{
+  sva_sequence_repetition_exprt::check(expr);
+  return static_cast<sva_sequence_repetition_exprt &>(expr);
+}
+
+class sva_sequence_goto_repetition_exprt : public sva_sequence_repetition_exprt
+{
+public:
+  sva_sequence_goto_repetition_exprt(exprt __op, constant_exprt __repetitions)
+    : sva_sequence_repetition_exprt{
+        ID_sva_sequence_goto_repetition,
+        std::move(__op),
+        std::move(__repetitions)}
+  {
+  }
 };
 
 inline const sva_sequence_goto_repetition_exprt &
@@ -1418,44 +1481,19 @@ to_sva_sequence_goto_repetition_expr(exprt &expr)
   return static_cast<sva_sequence_goto_repetition_exprt &>(expr);
 }
 
-class sva_sequence_non_consecutive_repetition_exprt : public binary_exprt
+class sva_sequence_non_consecutive_repetition_exprt
+  : public sva_sequence_repetition_exprt
 {
 public:
   sva_sequence_non_consecutive_repetition_exprt(
     exprt __op,
     constant_exprt __repetitions)
-    : binary_exprt{
-        std::move(__op),
+    : sva_sequence_repetition_exprt{
         ID_sva_sequence_non_consecutive_repetition,
-        std::move(__repetitions),
-        bool_typet{}}
-  {
-  }
-
-  const exprt &op() const
-  {
-    return op0();
-  }
-
-  exprt &op()
-  {
-    return op0();
-  }
-
-  // The number of repetitions must be a constant after elaboration.
-  const constant_exprt &repetitions() const
-  {
-    return static_cast<const constant_exprt &>(op1());
-  }
-
-  constant_exprt &repetitions()
+        std::move(__op),
+        std::move(__repetitions)}
   {
-    return static_cast<constant_exprt &>(op1());
   }
-
-protected:
-  using binary_exprt::op0;
-  using binary_exprt::op1;
 };
 
 inline const sva_sequence_non_consecutive_repetition_exprt &
diff --git a/src/verilog/verilog_typecheck_sva.cpp b/src/verilog/verilog_typecheck_sva.cpp
