Merge pull request #1065 from diffblue/nexttime-to-ltl

translate `s_always` and ranged `always` into LTL

Author: tautschnig

regression/ebmc/smv-netlist/always_with_range1.desc

@@ -0,0 +1,10 @@
+CORE
+always_with_range1.sv
+--smv-netlist
+^LTLSPEC node275 & X node363 & X X node451 .*
+^LTLSPEC G node1155$
+^LTLSPEC node1243 & X node1331 & X X node1419 .*
+^LTLSPEC G \(\!node2066 \| X node2097\)$
+^EXIT=0$
+^SIGNAL=0$
+--

regression/ebmc/smv-netlist/always_with_range1.sv

@@ -0,0 +1,23 @@
+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);
+
+  // nested
+  p3: assert property (always (x==1 implies always [1:1] x==2));
+
+endmodule

regression/ebmc/smv-netlist/nexttime1.desc

@@ -0,0 +1,9 @@
+CORE
+nexttime1.sv
+--smv-netlist
+^CTLSPEC node65$
+^LTLSPEC X node72$
+^LTLSPEC X X X X X X X X node79$
+^EXIT=0$
+^SIGNAL=0$
+--

regression/ebmc/smv-netlist/nexttime1.sv

@@ -0,0 +1,23 @@
+module main(input clk);
+
+  // count up from 0 to 10
+  reg [7:0] counter;
+
+  initial counter = 0;
+
+  always @(posedge clk)
+    if(counter == 10)
+      counter = 0;
+    else
+      counter = counter + 1;
+
+  // expected to pass
+  initial p1: assert property (s_nexttime[0] counter == 0);
+
+  // expected to pass
+  initial p2: assert property (s_nexttime[1] counter == 1);
+
+  // expected to pass
+  initial p3: assert property (nexttime[8] counter == 8);
+
+endmodule

src/temporal-logic/temporal_logic.cpp

@@ -8,6 +8,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "temporal_logic.h"
 
+#include <util/arith_tools.h>
 #include <util/expr_util.h>
 
 #include <verilog/sva_expr.h>
@@ -211,6 +212,15 @@ std::optional<exprt> LTL_to_CTL(exprt expr)
     return {};
 }
 
+static exprt n_Xes(mp_integer n, exprt op)
+{
+  PRECONDITION(n >= 0);
+  if(n == 0)
+    return op;
+  else
+    return n_Xes(n - 1, X_exprt{std::move(op)});
+}
+
 std::optional<exprt> SVA_to_LTL(exprt expr)
 {
   // Some SVA is directly mappable to LTL
@@ -222,6 +232,64 @@ std::optional<exprt> SVA_to_LTL(exprt expr)
     else
       return {};
   }
+  else if(expr.id() == ID_sva_ranged_always)
+  {
+    auto &ranged_always = to_sva_ranged_always_expr(expr);
+    auto rec = SVA_to_LTL(ranged_always.op());
+    if(rec.has_value())
+    {
+      // always [l:u] op ---> X ... X (op ∧ X op ∧ ... ∧ X ... X op)
+      auto lower_int = numeric_cast_v<mp_integer>(ranged_always.lower());
+
+      // Is there an upper end of the range?
+      if(ranged_always.upper().is_constant())
+      {
+        // upper end set
+        auto upper_int =
+          numeric_cast_v<mp_integer>(to_constant_expr(ranged_always.upper()));
+        PRECONDITION(upper_int >= lower_int);
+        auto diff = upper_int - lower_int;
+
+        exprt::operandst conjuncts;
+
+        for(auto i = 0; i <= diff; i++)
+          conjuncts.push_back(n_Xes(i, rec.value()));
+
+        return n_Xes(lower_int, conjunction(conjuncts));
+      }
+      else if(ranged_always.upper().id() == ID_infinity)
+      {
+        // always [l:$] op ---> X ... X G op
+        return n_Xes(lower_int, G_exprt{rec.value()});
+      }
+      else
+        PRECONDITION(false);
+    }
+    else
+      return {};
+  }
+  else if(expr.id() == ID_sva_s_always)
+  {
+    auto &ranged_always = to_sva_s_always_expr(expr);
+    auto rec = SVA_to_LTL(ranged_always.op());
+    if(rec.has_value())
+    {
+      // s_always [l:u] op ---> X ... X (op ∧ X op ∧ ... ∧ X ... X op)
+      auto lower_int = numeric_cast_v<mp_integer>(ranged_always.lower());
+      auto upper_int = numeric_cast_v<mp_integer>(ranged_always.upper());
+      PRECONDITION(upper_int >= lower_int);
+      auto diff = upper_int - lower_int;
+
+      exprt::operandst conjuncts;
+
+      for(auto i = 0; i <= diff; i++)
+        conjuncts.push_back(n_Xes(i, rec.value()));
+
+      return n_Xes(lower_int, conjunction(conjuncts));
+    }
+    else
+      return {};
+  }
   else if(expr.id() == ID_sva_s_eventually)
   {
     auto rec = SVA_to_LTL(to_sva_s_eventually_expr(expr).op());