From 0c3c7e98173c5d96ece7ef38ed69986cc0289e42 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Thu, 24 Apr 2025 11:14:02 -0700
Subject: [PATCH] SMV word-level output now converts SVA

Some parts of SVA map to LTL, which can be used by the SMV word-level
output.
---
 regression/ebmc/smv-word-level/verilog1.desc             | 3 ++-
 .../ebmc/smv-word-level/{verilog1.v => verilog1.sv}      | 2 ++
 src/ebmc/output_smv_word_level.cpp                       | 9 +++++++++
 3 files changed, 13 insertions(+), 1 deletion(-)
 rename regression/ebmc/smv-word-level/{verilog1.v => verilog1.sv} (68%)

diff --git a/regression/ebmc/smv-word-level/verilog1.desc b/regression/ebmc/smv-word-level/verilog1.desc
index e8af1cfaf..33aacafe2 100644
--- a/regression/ebmc/smv-word-level/verilog1.desc
+++ b/regression/ebmc/smv-word-level/verilog1.desc
@@ -1,11 +1,12 @@
 CORE
-verilog1.v
+verilog1.sv
 --smv-word-level
 ^MODULE main$
 ^VAR x : unsigned word\[32\];$
 ^INIT main\.x = 0ud32_0$
 ^INVAR Verilog::main\.x_aux0 = main\.x \+ 0ud32_1$
 ^TRANS next\(main\.x\) = Verilog::main\.x_aux0$
+^LTLSPEC F main\.x = 0sd32_10$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/ebmc/smv-word-level/verilog1.v b/regression/ebmc/smv-word-level/verilog1.sv
similarity index 68%
rename from regression/ebmc/smv-word-level/verilog1.v
rename to regression/ebmc/smv-word-level/verilog1.sv
index 77eaaad01..c6db51a74 100644
--- a/regression/ebmc/smv-word-level/verilog1.v
+++ b/regression/ebmc/smv-word-level/verilog1.sv
@@ -7,4 +7,6 @@ module main(input clk);
   always @(posedge clk)
     x = x + 1;
 
+  initial assert property (s_eventually x == 10);
+
 endmodule
diff --git a/src/ebmc/output_smv_word_level.cpp b/src/ebmc/output_smv_word_level.cpp
index ac8837eff..9a1b5fb1f 100644
--- a/src/ebmc/output_smv_word_level.cpp
+++ b/src/ebmc/output_smv_word_level.cpp
@@ -186,6 +186,15 @@ static void smv_properties(
     {
       out << "LTLSPEC " << expr2smv(property.normalized_expr, ns);
     }
+    else if(is_SVA(property.normalized_expr))
+    {
+      // we can turn some SVA properties into LTL
+      auto ltl_opt = SVA_to_LTL(property.normalized_expr);
+      if(ltl_opt.has_value())
+        out << "LTLSPEC " << expr2smv(ltl_opt.value(), ns);
+      else
+        out << "-- " << property.identifier << ": SVA not converted\n";
+    }
     else
       out << "-- " << property.identifier << ": not converted\n";