From f8751f8f70b3da755b5bb84684809e5be932b8d0 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Fri, 2 May 2025 10:13:02 -0700
Subject: [PATCH] implement NNF for SVA s_always

This adds the missing case of s_always when generating NNF for SVA.
---
 regression/verilog/SVA/s_always1.desc | 10 ++++++++++
 regression/verilog/SVA/s_always1.sv   | 14 ++++++++++++++
 src/temporal-logic/nnf.cpp            |  7 +++++++
 3 files changed, 31 insertions(+)
 create mode 100644 regression/verilog/SVA/s_always1.desc
 create mode 100644 regression/verilog/SVA/s_always1.sv

diff --git a/regression/verilog/SVA/s_always1.desc b/regression/verilog/SVA/s_always1.desc
new file mode 100644
index 000000000..758fb6e0a
--- /dev/null
+++ b/regression/verilog/SVA/s_always1.desc
@@ -0,0 +1,10 @@
+CORE
+s_always1.sv
+--bound 20
+^\[main\.p0\] s_always \[0:9\] main\.x < 10: PROVED up to bound 20$
+^\[main\.p1\] not \(s_always \[0:9\] main\.x < 10\): REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/verilog/SVA/s_always1.sv b/regression/verilog/SVA/s_always1.sv
new file mode 100644
index 000000000..f46b0523c
--- /dev/null
+++ b/regression/verilog/SVA/s_always1.sv
@@ -0,0 +1,14 @@
+module main(input clk);
+
+  reg [31:0] x = 0;
+
+  always_ff @(posedge clk)
+    x<=x+1;
+
+  // should pass
+  initial p0: assert property (s_always [0:9] x<10);
+
+  // should fail
+  initial p1: assert property (not s_always [0:9] x<10);
+
+endmodule
diff --git a/src/temporal-logic/nnf.cpp b/src/temporal-logic/nnf.cpp
index cd20e974c..74eecc486 100644
--- a/src/temporal-logic/nnf.cpp
+++ b/src/temporal-logic/nnf.cpp
@@ -81,6 +81,13 @@ std::optional<exprt> negate_property_node(const exprt &expr)
     return sva_ranged_s_eventually_exprt{
       always.lower(), always.upper(), not_exprt{always.op()}};
   }
+  else if(expr.id() == ID_sva_s_always)
+  {
+    // not s_always [x:y] p --> eventually [x:y] not p
+    auto &s_always = to_sva_s_always_expr(expr);
+    return sva_eventually_exprt{
+      s_always.lower(), s_always.upper(), not_exprt{s_always.op()}};
+  }
   else if(expr.id() == ID_sva_s_eventually)
   {
     // not s_eventually p --> always not p