ebmc: completeness threshold for SVA's always and s_always

This extends the completeness threshold logic to cover the bounded always and
s_always operators.

Author: kroening

regression/verilog/SVA/initial1.desc

@@ -5,7 +5,8 @@ initial1.sv
 ^\[main\.p1\] main\.counter == 100: REFUTED$
 ^\[main\.p2\] ##1 main\.counter == 1: PROVED up to bound 5$
 ^\[main\.p3\] ##1 main\.counter == 100: REFUTED$
-^\[main\.p4\] s_nexttime main\.counter == 1: PROVED up to bound 5$
+^\[main\.p4\] s_nexttime main\.counter == 1: PROVED$
+^\[main\.p5\] always \[1:1\] main\.counter == 1: PROVED$
 ^EXIT=10$
 ^SIGNAL=0$
 --

regression/verilog/SVA/initial1.sv

@@ -26,4 +26,7 @@ module main(input clk);
   // expected to pass if there are timeframes 0 and 1
   initial p4: assert property (s_nexttime counter == 1);
 
+  // expected to pass
+  initial p5: assert property (always [1:1] counter == 1);
+
 endmodule

src/ebmc/completeness_threshold.cpp

@@ -8,6 +8,8 @@ Author: Daniel Kroening, [email protected]
 
 #include "completeness_threshold.h"
 
+#include <util/arith_tools.h>
+
 #include <temporal-logic/ltl.h>
 #include <temporal-logic/temporal_logic.h>
 #include <verilog/sva_expr.h>
@@ -25,10 +27,41 @@ bool has_low_completeness_threshold(const exprt &expr)
     // X p
     return !has_temporal_operator(to_X_expr(expr).op());
   }
-  else if(expr.id() == ID_sva_nexttime)
+  else if(
+    expr.id() == ID_sva_nexttime || expr.id() == ID_sva_s_nexttime ||
+    expr.id() == ID_sva_s_nexttime)
+  {
+    // these are rewritten to always/s_always by normalize_property
+    PRECONDITION(false);
+  }
+  else if(expr.id() == ID_sva_ranged_always)
   {
-    // nexttime p
-    return !has_temporal_operator(to_sva_nexttime_expr(expr).op());
+    auto &always_expr = to_sva_ranged_always_expr(expr);
+    if(has_temporal_operator(always_expr.op()))
+      return false;
+    else if(always_expr.upper().is_constant())
+    {
+      auto lower_int = numeric_cast_v<mp_integer>(always_expr.lower());
+      auto upper_int =
+        numeric_cast_v<mp_integer>(to_constant_expr(always_expr.upper()));
+      return lower_int >= 0 && lower_int <= 1 && upper_int >= 0 &&
+             upper_int <= 1;
+    }
+    else
+      return false;
+  }
+  else if(expr.id() == ID_sva_s_always)
+  {
+    auto &s_always_expr = to_sva_s_always_expr(expr);
+    if(has_temporal_operator(s_always_expr.op()))
+      return false;
+    else
+    {
+      auto lower_int = numeric_cast_v<mp_integer>(s_always_expr.lower());
+      auto upper_int = numeric_cast_v<mp_integer>(s_always_expr.upper());
+      return lower_int >= 0 && lower_int <= 1 && upper_int >= 0 &&
+             upper_int <= 1;
+    }
   }
   else
     return false;