Verilog: ranged always and s_always properties

kroening · kroening · commit f664e6bc2d7f · 2024-04-15T08:26:52.000-07:00
This adds support for always property expressions with a given range and for
s_always properties.
diff --git a/regression/verilog/SVA/always_with_range1.desc b/regression/verilog/SVA/always_with_range1.desc
@@ -0,0 +1,11 @@
+CORE
+always_with_range1.sv
+--bound 20
+^\[main\.property\.1\] always \[0:9\] main\.x < 10: PROVED up to bound 20$
+^\[main\.property\.2\] always \[0:\$\] main\.x < 10: REFUTED$
+^\[main\.property\.3\] s_always \[0:9\] main\.x < 10: PROVED up to bound 20$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/verilog/SVA/always_with_range1.sv b/regression/verilog/SVA/always_with_range1.sv
@@ -0,0 +1,20 @@
+module main;
+
+  reg [31:0] x;
+  wire clk;
+
+  initial x=0;
+
+  always @(posedge clk)
+    x<=x+1;
+
+  // holds owing to the range
+  initial p0: assert property (always [0:9] x<10);
+
+  // unbounded, fails
+  initial p1: assert property (always [0:$] x<10);
+
+  // strong variant
+  initial p2: assert property (s_always [0:9] x<10);
+
+endmodule
diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h
@@ -16,6 +16,8 @@ IREP_ID_ONE(sva_sequence_throughout)
 IREP_ID_ONE(sva_sequence_concatenation)
 IREP_ID_ONE(sva_sequence_first_match)
 IREP_ID_ONE(sva_always)
+IREP_ID_ONE(sva_ranged_always)
+IREP_ID_ONE(sva_s_always)
 IREP_ID_ONE(sva_cover)
 IREP_ID_ONE(sva_nexttime)
 IREP_ID_ONE(sva_s_nexttime)
diff --git a/src/temporal-logic/temporal_logic.cpp b/src/temporal-logic/temporal_logic.cpp
@@ -17,11 +17,12 @@ bool is_temporal_operator(const exprt &expr)
          expr.id() == ID_A || expr.id() == ID_E || expr.id() == ID_U ||
          expr.id() == ID_R || expr.id() == ID_G || expr.id() == ID_F ||
          expr.id() == ID_X || expr.id() == ID_sva_always ||
-         expr.id() == ID_sva_always || expr.id() == ID_sva_nexttime ||
-         expr.id() == ID_sva_s_nexttime || expr.id() == ID_sva_until ||
-         expr.id() == ID_sva_s_until || expr.id() == ID_sva_until_with ||
-         expr.id() == ID_sva_s_until_with || expr.id() == ID_sva_eventually ||
-         expr.id() == ID_sva_s_eventually || expr.id() == ID_sva_cycle_delay;
+         expr.id() == ID_sva_always || expr.id() == ID_sva_ranged_always ||
+         expr.id() == ID_sva_nexttime || expr.id() == ID_sva_s_nexttime ||
+         expr.id() == ID_sva_until || expr.id() == ID_sva_s_until ||
+         expr.id() == ID_sva_until_with || expr.id() == ID_sva_s_until_with ||
+         expr.id() == ID_sva_eventually || expr.id() == ID_sva_s_eventually ||
+         expr.id() == ID_sva_cycle_delay;
 }
 
 bool has_temporal_operator(const exprt &expr)
diff --git a/src/trans-word-level/property.cpp b/src/trans-word-level/property.cpp
@@ -8,11 +8,13 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "property.h"
 
+#include <util/arith_tools.h>
 #include <util/expr_iterator.h>
 #include <util/namespace.h>
 #include <util/std_expr.h>
 #include <util/symbol_table.h>
 
+#include <ebmc/ebmc_error.h>
 #include <temporal-logic/temporal_expr.h>
 #include <temporal-logic/temporal_logic.h>
 #include <verilog/sva_expr.h>
@@ -56,6 +58,8 @@ bool bmc_supports_property(const exprt &expr)
     return bmc_supports_property(to_X_expr(expr).op());
   else if(expr.id() == ID_sva_always)
     return true;
+  else if(expr.id() == ID_sva_ranged_always)
+    return true;
   else
     return false;
 }
@@ -75,12 +79,12 @@ Function: property_obligations_rec
 static void property_obligations_rec(
   const exprt &property_expr,
   decision_proceduret &solver,
-  std::size_t current,
-  std::size_t no_timeframes,
+  const mp_integer &current,
+  const mp_integer &no_timeframes,
   const namespacet &ns,
-  std::map<std::size_t, exprt::operandst> &obligations)
+  std::map<mp_integer, exprt::operandst> &obligations)
 {
-  PRECONDITION(current < no_timeframes);
+  PRECONDITION(current >= 0 && current < no_timeframes);
 
   if(property_expr.id() == ID_X)
   {
@@ -108,7 +112,43 @@ static void property_obligations_rec(
         PRECONDITION(false);
     }(property_expr);
 
-    for(std::size_t c = current; c < no_timeframes; c++)
+    for(mp_integer c = current; c < no_timeframes; ++c)
+    {
+      property_obligations_rec(phi, solver, c, no_timeframes, ns, obligations);
+    }
+  }
+  else if(
+    property_expr.id() == ID_sva_ranged_always ||
+    property_expr.id() == ID_sva_s_always)
+  {
+    auto &phi = property_expr.id() == ID_sva_ranged_always
+                  ? to_sva_ranged_always_expr(property_expr).op()
+                  : to_sva_s_always_expr(property_expr).op();
+    auto &range = property_expr.id() == ID_sva_ranged_always
+                    ? to_sva_ranged_always_expr(property_expr).range()
+                    : to_sva_s_always_expr(property_expr).range();
+
+    auto from_opt = numeric_cast<mp_integer>(range.op0());
+    if(!from_opt.has_value())
+      throw ebmc_errort() << "failed to convert SVA always from index";
+
+    auto from = std::max(mp_integer{0}, *from_opt);
+
+    mp_integer to;
+
+    if(range.op1().id() == ID_infinity)
+    {
+      to = no_timeframes - 1;
+    }
+    else
+    {
+      auto to_opt = numeric_cast<mp_integer>(range.op1());
+      if(!to_opt.has_value())
+        throw ebmc_errort() << "failed to convert SVA always to index";
+      to = std::min(*to_opt, no_timeframes - 1);
+    }
+
+    for(mp_integer c = from; c <= to; ++c)
     {
       property_obligations_rec(phi, solver, c, no_timeframes, ns, obligations);
     }
@@ -133,13 +173,13 @@ Function: property_obligations
 
 \*******************************************************************/
 
-static std::map<std::size_t, exprt::operandst> property_obligations(
+static std::map<mp_integer, exprt::operandst> property_obligations(
   const exprt &property_expr,
   decision_proceduret &solver,
-  std::size_t no_timeframes,
+  const mp_integer &no_timeframes,
   const namespacet &ns)
 {
-  std::map<std::size_t, exprt::operandst> obligations;
+  std::map<mp_integer, exprt::operandst> obligations;
 
   property_obligations_rec(
     property_expr, solver, 0, no_timeframes, ns, obligations);
@@ -178,8 +218,10 @@ void property(
   for(auto &obligation_it : obligations)
   {
     auto t = obligation_it.first;
-    DATA_INVARIANT(t < no_timeframes, "obligation must have valid timeframe");
-    prop_handles[t] = conjunction(obligation_it.second);
+    DATA_INVARIANT(
+      t >= 0 && t < no_timeframes, "obligation must have valid timeframe");
+    auto t_int = numeric_cast_v<std::size_t>(t);
+    prop_handles[t_int] = conjunction(obligation_it.second);
   }
 }
 
diff --git a/src/verilog/expr2verilog.cpp b/src/verilog/expr2verilog.cpp
@@ -394,8 +394,12 @@ std::string expr2verilogt::convert_sva(
   if(range.has_value())
   {
     auto &range_binary = to_binary_expr(range.value());
-    range_str = "[" + convert(range_binary.lhs()) + ':' +
-                convert(range_binary.rhs()) + "] ";
+    range_str = "[" + convert(range_binary.lhs()) + ':';
+    if(range_binary.rhs().id() == ID_infinity)
+      range_str += "$";
+    else
+      range_str += convert(range_binary.rhs());
+    range_str += "] ";
   }
 
   unsigned p;
@@ -1088,6 +1092,22 @@ std::string expr2verilogt::convert(
   else if(src.id()==ID_sva_always)
     return precedence = 0, convert_sva("always", to_sva_always_expr(src).op());
 
+  else if(src.id() == ID_sva_ranged_always)
+  {
+    return precedence = 0, convert_sva(
+                             "always",
+                             to_sva_ranged_always_expr(src).range(),
+                             to_sva_ranged_always_expr(src).op());
+  }
+
+  else if(src.id() == ID_sva_s_always)
+  {
+    return precedence = 0, convert_sva(
+                             "s_always",
+                             to_sva_s_always_expr(src).range(),
+                             to_sva_s_always_expr(src).op());
+  }
+
   else if(src.id() == ID_sva_cover)
     return precedence = 0, convert_sva("cover", to_sva_cover_expr(src).op());
 
diff --git a/src/verilog/parser.y b/src/verilog/parser.y
@@ -1965,8 +1965,11 @@ property_expr_proper:
         | property_expr "|=>" property_expr { init($$, ID_sva_non_overlapped_implication); mto($$, $1); mto($$, $3); }
         | "nexttime" property_expr          { init($$, "sva_nexttime"); mto($$, $2); }
         | "s_nexttime" property_expr        { init($$, "sva_s_nexttime"); mto($$, $2); }
+        | "always" '[' cycle_delay_const_range_expression ']' property_expr %prec "always"
+		{ init($$, ID_sva_ranged_always); mto($$, $3); mto($$, $5); }
         | "always" property_expr            { init($$, "sva_always"); mto($$, $2); }
-        | "s_always" property_expr          { init($$, "sva_s_always"); mto($$, $2); }
+        | "s_always" '[' constant_range ']' property_expr %prec "s_always"
+		{ init($$, ID_sva_s_always); mto($$, $3); mto($$, $5); }
         | "s_eventually" property_expr
 		{ init($$, "sva_s_eventually"); mto($$, $2); }
         | "eventually" '[' constant_range ']' property_expr %prec "eventually"
@@ -2008,8 +2011,10 @@ cycle_delay_range:
         ;
 
 cycle_delay_const_range_expression:
-	  constant_expression ':' constant_expression
-	| constant_expression ':' '$'
+	  constant_expression TOK_COLON constant_expression
+                { init($$, ID_sva_cycle_delay); mto($$, $1); mto($$, $3); }
+	| constant_expression TOK_COLON '$'
+                { init($$, ID_sva_cycle_delay); mto($$, $1); stack_expr($$).add_to_operands(exprt(ID_infinity)); }
 	;
 
 expression_or_dist:
diff --git a/src/verilog/sva_expr.h b/src/verilog/sva_expr.h
@@ -170,6 +170,129 @@ static inline sva_always_exprt &to_sva_always_expr(exprt &expr)
   return static_cast<sva_always_exprt &>(expr);
 }
 
+class sva_ranged_always_exprt : public binary_predicate_exprt
+{
+public:
+  sva_ranged_always_exprt(binary_exprt range, exprt op)
+    : binary_predicate_exprt(std::move(range), ID_sva_always, std::move(op))
+  {
+  }
+
+  // These come with a range, which is binary
+  const binary_exprt &range() const
+  {
+    return static_cast<const binary_exprt &>(op0());
+  }
+
+  binary_exprt &range()
+  {
+    return static_cast<binary_exprt &>(op0());
+  }
+
+  const exprt &op() const
+  {
+    return op1();
+  }
+
+  exprt &op()
+  {
+    return op1();
+  }
+
+  const exprt &lhs() const = delete;
+  exprt &lhs() = delete;
+  const exprt &rhs() const = delete;
+  exprt &rhs() = delete;
+
+  static void check(
+    const exprt &expr,
+    const validation_modet vm = validation_modet::INVARIANT)
+  {
+    binary_exprt::check(expr, vm);
+    binary_exprt::check(to_binary_expr(expr).op0(), vm);
+  }
+
+protected:
+  using binary_predicate_exprt::op0;
+  using binary_predicate_exprt::op1;
+};
+
+static inline const sva_ranged_always_exprt &
+to_sva_ranged_always_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_sva_ranged_always);
+  sva_ranged_always_exprt::check(expr, validation_modet::INVARIANT);
+  return static_cast<const sva_ranged_always_exprt &>(expr);
+}
+
+static inline sva_ranged_always_exprt &to_sva_ranged_always_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_sva_ranged_always);
+  sva_ranged_always_exprt::check(expr, validation_modet::INVARIANT);
+  return static_cast<sva_ranged_always_exprt &>(expr);
+}
+
+class sva_s_always_exprt : public binary_predicate_exprt
+{
+public:
+  sva_s_always_exprt(binary_exprt range, exprt op)
+    : binary_predicate_exprt(std::move(range), ID_sva_s_always, std::move(op))
+  {
+  }
+
+  // These come with a range, which is binary
+  const binary_exprt &range() const
+  {
+    return static_cast<const binary_exprt &>(op0());
+  }
+
+  binary_exprt &range()
+  {
+    return static_cast<binary_exprt &>(op0());
+  }
+
+  const exprt &op() const
+  {
+    return op1();
+  }
+
+  exprt &op()
+  {
+    return op1();
+  }
+
+  const exprt &lhs() const = delete;
+  exprt &lhs() = delete;
+  const exprt &rhs() const = delete;
+  exprt &rhs() = delete;
+
+  static void check(
+    const exprt &expr,
+    const validation_modet vm = validation_modet::INVARIANT)
+  {
+    binary_exprt::check(expr, vm);
+    binary_exprt::check(to_binary_expr(expr).op0(), vm);
+  }
+
+protected:
+  using binary_predicate_exprt::op0;
+  using binary_predicate_exprt::op1;
+};
+
+static inline const sva_s_always_exprt &to_sva_s_always_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_sva_s_always);
+  sva_s_always_exprt::check(expr, validation_modet::INVARIANT);
+  return static_cast<const sva_s_always_exprt &>(expr);
+}
+
+static inline sva_s_always_exprt &to_sva_s_always_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_sva_s_always);
+  sva_s_always_exprt::check(expr, validation_modet::INVARIANT);
+  return static_cast<sva_s_always_exprt &>(expr);
+}
+
 class sva_cover_exprt : public unary_predicate_exprt
 {
 public:
diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp
