Merge pull request #1085 from diffblue/sva-until-to-ltl

convert `s_until` and `s_until_with` to LTL

Author: kroening

regression/ebmc/smv-netlist/s_until1.desc

@@ -0,0 +1,8 @@
+CORE
+s_until1.sv
+--smv-netlist
+^LTLSPEC \(\!node144\) U node151$
+^LTLSPEC \(1\) U node158$
+^EXIT=0$
+^SIGNAL=0$
+--

regression/ebmc/smv-netlist/s_until1.sv

@@ -0,0 +1,18 @@
+module main(input clk);
+
+  // count up from 0 to 10
+  reg [7:0] counter = 0;
+
+  always_ff @(posedge clk)
+    if(counter == 10)
+      counter = 0;
+    else
+      counter = counter + 1;
+
+  // expected to pass
+  initial p0: assert property ($past(counter)<=counter s_until counter==10);
+
+  // expected to fail
+  initial p1: assert property (1 s_until counter==11);
+
+endmodule

regression/verilog/SVA/s_until1.desc

@@ -0,0 +1,8 @@
+CORE
+s_until1.sv
+--bound 11
+^\[.*\] \$past\(main\.counter\) <= main\.counter s_until main\.counter == 10: PROVED up to bound 11$
+^\[.*\] 1 s_until main\.counter == 11: REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--

regression/verilog/SVA/s_until1.sv

@@ -0,0 +1,18 @@
+module main(input clk);
+
+  // count up from 0 to 10
+  reg [7:0] counter = 0;
+
+  always_ff @(posedge clk)
+    if(counter == 10)
+      counter = 0;
+    else
+      counter = counter + 1;
+
+  // expected to pass
+  initial p0: assert property ($past(counter)<=counter s_until counter==10);
+
+  // expected to fail
+  initial p1: assert property (1 s_until counter==11);
+
+endmodule

src/temporal-logic/temporal_logic.cpp

@@ -338,6 +338,27 @@ std::optional<exprt> SVA_to_LTL(exprt expr)
     else
       return {};
   }
+  else if(expr.id() == ID_sva_s_until)
+  {
+    auto &until = to_sva_s_until_expr(expr);
+    auto rec_lhs = SVA_to_LTL(until.lhs());
+    auto rec_rhs = SVA_to_LTL(until.rhs());
+    if(rec_lhs.has_value() && rec_rhs.has_value())
+      return U_exprt{rec_lhs.value(), rec_rhs.value()};
+    else
+      return {};
+  }
+  else if(expr.id() == ID_sva_s_until_with)
+  {
+    // This is release with swapped operands
+    auto &until_with = to_sva_s_until_with_expr(expr);
+    auto rec_lhs = SVA_to_LTL(until_with.lhs());
+    auto rec_rhs = SVA_to_LTL(until_with.rhs());
+    if(rec_lhs.has_value() && rec_rhs.has_value())
+      return R_exprt{rec_rhs.value(), rec_lhs.value()}; // swapped
+    else
+      return {};
+  }
   else if(!has_temporal_operator(expr))
   {
     return expr;