Merge pull request #693 from diffblue/indexed_nexttime

SVA: introduce `sva_indexed_nexttime_exprt` and `sva_indexed_s_nexttime_exprt`
diffblue · Sep 16, 2024 · 35e5313 · 35e5313
2 parents 4a82eca + 7e3d3bb
commit 35e5313
Show file tree

Hide file tree

Showing 6 changed files with 117 additions and 60 deletions.
diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h
@@ -43,7 +43,9 @@ IREP_ID_ONE(sva_s_always)
 IREP_ID_ONE(sva_assume)
 IREP_ID_ONE(sva_cover)
 IREP_ID_ONE(sva_nexttime)
+IREP_ID_ONE(sva_indexed_nexttime)
 IREP_ID_ONE(sva_s_nexttime)
+IREP_ID_ONE(sva_indexed_s_nexttime)
 IREP_ID_ONE(sva_eventually)
 IREP_ID_ONE(sva_s_eventually)
 IREP_ID_ONE(sva_until)

diff --git a/src/temporal-logic/normalize_property.cpp b/src/temporal-logic/normalize_property.cpp
@@ -171,21 +171,23 @@ exprt normalize_property(exprt expr)
     expr = normalize_pre_sva_or(to_sva_or_expr(expr));
   else if(expr.id() == ID_sva_nexttime)
   {
-    auto &nexttime_expr = to_sva_nexttime_expr(expr);
-    if(nexttime_expr.is_indexed())
-      expr = sva_ranged_always_exprt{
-        nexttime_expr.index(), nexttime_expr.index(), nexttime_expr.op()};
-    else
-      expr = X_exprt{nexttime_expr.op()};
+    expr = X_exprt{to_sva_nexttime_expr(expr).op()};
   }
   else if(expr.id() == ID_sva_s_nexttime)
   {
-    auto &nexttime_expr = to_sva_s_nexttime_expr(expr);
-    if(nexttime_expr.is_indexed())
-      expr = sva_s_always_exprt{
-        nexttime_expr.index(), nexttime_expr.index(), nexttime_expr.op()};
-    else
-      expr = X_exprt{to_sva_s_nexttime_expr(expr).op()};
+    expr = X_exprt{to_sva_s_nexttime_expr(expr).op()};
+  }
+  else if(expr.id() == ID_sva_indexed_nexttime)
+  {
+    auto &nexttime_expr = to_sva_indexed_nexttime_expr(expr);
+    expr = sva_ranged_always_exprt{
+      nexttime_expr.index(), nexttime_expr.index(), nexttime_expr.op()};
+  }
+  else if(expr.id() == ID_sva_indexed_s_nexttime)
+  {
+    auto &nexttime_expr = to_sva_indexed_s_nexttime_expr(expr);
+    expr = sva_s_always_exprt{
+      nexttime_expr.index(), nexttime_expr.index(), nexttime_expr.op()};
   }
   else if(expr.id() == ID_sva_cycle_delay)
     expr = normalize_pre_sva_cycle_delay(to_sva_cycle_delay_expr(expr));

diff --git a/src/verilog/expr2verilog.cpp b/src/verilog/expr2verilog.cpp
@@ -1499,16 +1499,25 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src)
 
   else if(src.id()==ID_sva_nexttime)
     return precedence = verilog_precedencet::MIN,
-           convert_sva_indexed_binary("nexttime", to_sva_nexttime_expr(src));
+           convert_sva_unary("nexttime", to_sva_nexttime_expr(src));
 
-  else if(src.id() == ID_sva_disable_iff)
+  else if(src.id() == ID_sva_indexed_nexttime)
     return precedence = verilog_precedencet::MIN,
-           convert_sva_abort("disable iff", to_sva_abort_expr(src));
+           convert_sva_indexed_binary(
+             "nexttime", to_sva_indexed_nexttime_expr(src));
 
   else if(src.id()==ID_sva_s_nexttime)
+    return precedence = verilog_precedencet::MIN,
+           convert_sva_unary("s_nexttime", to_sva_s_nexttime_expr(src));
+
+  else if(src.id() == ID_sva_indexed_s_nexttime)
     return precedence = verilog_precedencet::MIN,
            convert_sva_indexed_binary(
-             "s_nexttime", to_sva_s_nexttime_expr(src));
+             "s_nexttime", to_sva_indexed_s_nexttime_expr(src));
+
+  else if(src.id() == ID_sva_disable_iff)
+    return precedence = verilog_precedencet::MIN,
+           convert_sva_abort("disable iff", to_sva_abort_expr(src));
 
   else if(src.id()==ID_sva_eventually)
   {

diff --git a/src/verilog/parser.y b/src/verilog/parser.y
@@ -2179,13 +2179,13 @@ property_expr_proper:
 	| sequence_expr "#=#" property_expr
 		{ init($$, ID_sva_nonoverlapped_followed_by); mto($$, $1); mto($$, $3); }
 	| "nexttime" property_expr
-		{ init($$, "sva_nexttime"); stack_expr($$).add_to_operands(nil_exprt()); mto($$, $2); }
+		{ init($$, "sva_nexttime"); mto($$, $2); }
 	| "nexttime" '[' constant_expression ']' property_expr %prec "nexttime"
-		{ init($$, "sva_nexttime"); mto($$, $3); mto($$, $5); }
+		{ init($$, "sva_indexed_nexttime"); mto($$, $3); mto($$, $5); }
 	| "s_nexttime" property_expr
-		{ init($$, "sva_s_nexttime"); stack_expr($$).add_to_operands(nil_exprt()); mto($$, $2); }
+		{ init($$, "sva_s_nexttime"); mto($$, $2); }
 	| "s_nexttime" '[' constant_expression ']' property_expr %prec "s_nexttime"
-		{ init($$, "sva_s_nexttime"); mto($$, $3); mto($$, $5); }
+		{ init($$, "sva_indexed_s_nexttime"); mto($$, $3); mto($$, $5); }
 	| "always" '[' cycle_delay_const_range_expression ']' property_expr %prec "always"
 		{ init($$, ID_sva_ranged_always); swapop($$, $3); mto($$, $5); }
 	| "always" property_expr

diff --git a/src/verilog/sva_expr.h b/src/verilog/sva_expr.h
@@ -84,18 +84,62 @@ static inline sva_disable_iff_exprt &to_sva_disable_iff_expr(exprt &expr)
   return static_cast<sva_disable_iff_exprt &>(expr);
 }
 
-class sva_nexttime_exprt : public binary_predicate_exprt
+/// nonindexed variant
+class sva_nexttime_exprt : public unary_predicate_exprt
 {
 public:
-  // nonindexed variant
   explicit sva_nexttime_exprt(exprt op)
-    : binary_predicate_exprt(nil_exprt(), ID_sva_nexttime, std::move(op))
+    : unary_predicate_exprt(ID_sva_nexttime, std::move(op))
   {
   }
+};
+
+static inline const sva_nexttime_exprt &to_sva_nexttime_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_sva_nexttime);
+  sva_nexttime_exprt::check(expr, validation_modet::INVARIANT);
+  return static_cast<const sva_nexttime_exprt &>(expr);
+}
+
+static inline sva_nexttime_exprt &to_sva_nexttime_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_sva_nexttime);
+  sva_nexttime_exprt::check(expr, validation_modet::INVARIANT);
+  return static_cast<sva_nexttime_exprt &>(expr);
+}
+
+/// nonindexed variant
+class sva_s_nexttime_exprt : public unary_predicate_exprt
+{
+public:
+  explicit sva_s_nexttime_exprt(exprt op)
+    : unary_predicate_exprt(ID_sva_s_nexttime, std::move(op))
+  {
+  }
+};
+
+static inline const sva_s_nexttime_exprt &
+to_sva_s_nexttime_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_sva_s_nexttime);
+  sva_s_nexttime_exprt::check(expr, validation_modet::INVARIANT);
+  return static_cast<const sva_s_nexttime_exprt &>(expr);
+}
+
+static inline sva_s_nexttime_exprt &to_sva_s_nexttime_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_sva_s_nexttime);
+  sva_s_nexttime_exprt::check(expr, validation_modet::INVARIANT);
+  return static_cast<sva_s_nexttime_exprt &>(expr);
+}
 
-  bool is_indexed() const
+/// indexed variant of sva_nexttime_exprt
+class sva_indexed_nexttime_exprt : public binary_predicate_exprt
+{
+public:
+  sva_indexed_nexttime_exprt(exprt index, exprt op)
+    : binary_predicate_exprt(std::move(index), ID_sva_nexttime, std::move(op))
   {
-    return index().is_not_nil();
   }
 
   const exprt &index() const
@@ -123,32 +167,32 @@ class sva_nexttime_exprt : public binary_predicate_exprt
   using binary_predicate_exprt::op1;
 };
 
-static inline const sva_nexttime_exprt &to_sva_nexttime_expr(const exprt &expr)
+static inline const sva_indexed_nexttime_exprt &
+to_sva_indexed_nexttime_expr(const exprt &expr)
 {
-  PRECONDITION(expr.id() == ID_sva_nexttime);
-  sva_nexttime_exprt::check(expr, validation_modet::INVARIANT);
-  return static_cast<const sva_nexttime_exprt &>(expr);
+  PRECONDITION(expr.id() == ID_sva_indexed_nexttime);
+  sva_indexed_nexttime_exprt::check(expr, validation_modet::INVARIANT);
+  return static_cast<const sva_indexed_nexttime_exprt &>(expr);
 }
 
-static inline sva_nexttime_exprt &to_sva_nexttime_expr(exprt &expr)
+static inline sva_indexed_nexttime_exprt &
+to_sva_indexed_nexttime_expr(exprt &expr)
 {
-  PRECONDITION(expr.id() == ID_sva_nexttime);
-  sva_nexttime_exprt::check(expr, validation_modet::INVARIANT);
-  return static_cast<sva_nexttime_exprt &>(expr);
+  PRECONDITION(expr.id() == ID_sva_indexed_nexttime);
+  sva_indexed_nexttime_exprt::check(expr, validation_modet::INVARIANT);
+  return static_cast<sva_indexed_nexttime_exprt &>(expr);
 }
 
-class sva_s_nexttime_exprt : public binary_predicate_exprt
+/// indexed variant of sva_s_nexttime_exprt
+class sva_indexed_s_nexttime_exprt : public binary_predicate_exprt
 {
 public:
-  // nonindexed variant
-  explicit sva_s_nexttime_exprt(exprt op)
-    : binary_predicate_exprt(nil_exprt(), ID_sva_s_nexttime, std::move(op))
-  {
-  }
-
-  bool is_indexed() const
+  sva_indexed_s_nexttime_exprt(exprt index, exprt op)
+    : binary_predicate_exprt(
+        std::move(index),
+        ID_sva_indexed_s_nexttime,
+        std::move(op))
   {
-    return index().is_not_nil();
   }
 
   const exprt &index() const
@@ -176,19 +220,20 @@ class sva_s_nexttime_exprt : public binary_predicate_exprt
   using binary_predicate_exprt::op1;
 };
 
-static inline const sva_s_nexttime_exprt &
-to_sva_s_nexttime_expr(const exprt &expr)
+static inline const sva_indexed_s_nexttime_exprt &
+to_sva_indexed_s_nexttime_expr(const exprt &expr)
 {
-  PRECONDITION(expr.id() == ID_sva_s_nexttime);
-  sva_s_nexttime_exprt::check(expr, validation_modet::INVARIANT);
-  return static_cast<const sva_s_nexttime_exprt &>(expr);
+  PRECONDITION(expr.id() == ID_sva_indexed_s_nexttime);
+  sva_indexed_s_nexttime_exprt::check(expr, validation_modet::INVARIANT);
+  return static_cast<const sva_indexed_s_nexttime_exprt &>(expr);
 }
 
-static inline sva_s_nexttime_exprt &to_sva_s_nexttime_expr(exprt &expr)
+static inline sva_indexed_s_nexttime_exprt &
+to_sva_indexed_s_nexttime_expr(exprt &expr)
 {
-  PRECONDITION(expr.id() == ID_sva_s_nexttime);
-  sva_s_nexttime_exprt::check(expr, validation_modet::INVARIANT);
-  return static_cast<sva_s_nexttime_exprt &>(expr);
+  PRECONDITION(expr.id() == ID_sva_indexed_s_nexttime);
+  sva_indexed_s_nexttime_exprt::check(expr, validation_modet::INVARIANT);
+  return static_cast<sva_indexed_s_nexttime_exprt &>(expr);
 }
 
 class sva_ranged_predicate_exprt : public ternary_exprt

diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp
@@ -2405,7 +2405,8 @@ exprt verilog_typecheck_exprt::convert_unary_expr(unary_exprt expr)
     expr.id() == ID_sva_always || expr.id() == ID_sva_s_eventually ||
     expr.id() == ID_sva_cycle_delay_plus ||
     expr.id() == ID_sva_cycle_delay_star || expr.id() == ID_sva_weak ||
-    expr.id() == ID_sva_strong)
+    expr.id() == ID_sva_strong || expr.id() == ID_sva_nexttime ||
+    expr.id() == ID_sva_s_nexttime)
   {
     convert_expr(expr.op());
     make_boolean(expr.op());
@@ -2821,24 +2822,22 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr)
     expr.type() = bool_typet();
     return std::move(expr);
   }
-  else if(expr.id() == ID_sva_nexttime)
+  else if(expr.id() == ID_sva_indexed_nexttime)
   {
-    if(to_sva_nexttime_expr(expr).is_indexed())
-      convert_expr(to_sva_nexttime_expr(expr).index());
+    convert_expr(to_sva_indexed_nexttime_expr(expr).index());
 
-    auto &op = to_sva_nexttime_expr(expr).op();
+    auto &op = to_sva_indexed_nexttime_expr(expr).op();
     convert_expr(op);
     make_boolean(op);
     expr.type() = bool_typet();
 
     return std::move(expr);
   }
-  else if(expr.id() == ID_sva_s_nexttime)
+  else if(expr.id() == ID_sva_indexed_s_nexttime)
   {
-    if(to_sva_s_nexttime_expr(expr).is_indexed())
-      convert_expr(to_sva_s_nexttime_expr(expr).index());
+    convert_expr(to_sva_indexed_s_nexttime_expr(expr).index());
 
-    auto &op = to_sva_s_nexttime_expr(expr).op();
+    auto &op = to_sva_indexed_s_nexttime_expr(expr).op();
     convert_expr(op);
     make_boolean(op);
     expr.type() = bool_typet();