From 774bc02005892ce1f66bb7f17be6e51c89a1eeb6 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Thu, 24 Apr 2025 07:08:32 -0700
Subject: [PATCH] convert s_until and s_until_with to LTL

This adds conversion for the SVA operators s_until and s_until_with to LTL.
---
 regression/ebmc/smv-netlist/s_until1.desc |  8 ++++++++
 regression/ebmc/smv-netlist/s_until1.sv   | 18 ++++++++++++++++++
 regression/verilog/SVA/s_until1.desc      |  8 ++++++++
 regression/verilog/SVA/s_until1.sv        | 18 ++++++++++++++++++
 src/temporal-logic/temporal_logic.cpp     | 21 +++++++++++++++++++++
 5 files changed, 73 insertions(+)
 create mode 100644 regression/ebmc/smv-netlist/s_until1.desc
 create mode 100644 regression/ebmc/smv-netlist/s_until1.sv
 create mode 100644 regression/verilog/SVA/s_until1.desc
 create mode 100644 regression/verilog/SVA/s_until1.sv

diff --git a/regression/ebmc/smv-netlist/s_until1.desc b/regression/ebmc/smv-netlist/s_until1.desc
new file mode 100644
index 000000000..4d59d8c20
--- /dev/null
+++ b/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$
+--
diff --git a/regression/ebmc/smv-netlist/s_until1.sv b/regression/ebmc/smv-netlist/s_until1.sv
new file mode 100644
index 000000000..7607fb288
--- /dev/null
+++ b/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
diff --git a/regression/verilog/SVA/s_until1.desc b/regression/verilog/SVA/s_until1.desc
new file mode 100644
index 000000000..db361fc61
--- /dev/null
+++ b/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$
+--
diff --git a/regression/verilog/SVA/s_until1.sv b/regression/verilog/SVA/s_until1.sv
new file mode 100644
index 000000000..7607fb288
--- /dev/null
+++ b/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
diff --git a/src/temporal-logic/temporal_logic.cpp b/src/temporal-logic/temporal_logic.cpp
index 832447485..9a14c3976 100644
--- a/src/temporal-logic/temporal_logic.cpp
+++ b/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;