From a0640a9062adce09bca61c32aace74a5a5f44d6a Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Sun, 8 Sep 2024 12:14:53 +0100
Subject: [PATCH] =?UTF-8?q?SVA:=20fix=20normalization=20of=20##[*]=20?=
 =?UTF-8?q?=CF=86?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This fixes the normalization of ##[*] φ.
---
 regression/verilog/SVA/sequence3.desc     | 6 ++++--
 regression/verilog/SVA/sequence3.sv       | 9 +++++++--
 src/temporal-logic/normalize_property.cpp | 2 +-
 src/temporal-logic/normalize_property.h   | 4 ++--
 4 files changed, 14 insertions(+), 7 deletions(-)

diff --git a/regression/verilog/SVA/sequence3.desc b/regression/verilog/SVA/sequence3.desc
index e15d20dc2..4db1f8979 100644
--- a/regression/verilog/SVA/sequence3.desc
+++ b/regression/verilog/SVA/sequence3.desc
@@ -2,9 +2,11 @@ CORE
 sequence3.sv
 --bound 20 --numbered-trace
 ^\[main\.p0\] ##\[\*\] main\.x == 6: REFUTED$
-^Counterexample with 2 states:$
-^\[main\.p1\] ##\[\+\] main\.x == 0: REFUTED$
 ^Counterexample with 7 states:$
+^\[main\.p1\] ##\[\*\] main\.x == 5: PROVED up to bound 20$
+^\[main\.p2\] ##\[\+\] main\.x == 0: REFUTED$
+^Counterexample with 7 states:$
+^\[main\.p3\] ##\[\+\] main\.x == 5: PROVED up to bound 20$
 ^EXIT=10$
 ^SIGNAL=0$
 --
diff --git a/regression/verilog/SVA/sequence3.sv b/regression/verilog/SVA/sequence3.sv
index 0d2ce130d..bcea5c87f 100644
--- a/regression/verilog/SVA/sequence3.sv
+++ b/regression/verilog/SVA/sequence3.sv
@@ -9,7 +9,12 @@ module main;
     if(x < 5)
       x<=x+1;
 
-  initial p0: assert property (##[*] x==6); // same as [0:$]
-  initial p1: assert property (##[+] x==0); // same as [1:$]
+  // ##[*] is the same as [0:$]
+  initial p0: assert property (##[*] x==6); // should fail
+  initial p1: assert property (##[*] x==5); // should pass
+
+  // ##[+] is the same as [1:$]
+  initial p2: assert property (##[+] x==0); // should fail
+  initial p3: assert property (##[+] x==5); // should pass
 
 endmodule
diff --git a/src/temporal-logic/normalize_property.cpp b/src/temporal-logic/normalize_property.cpp
index 9286a3ecc..65b979720 100644
--- a/src/temporal-logic/normalize_property.cpp
+++ b/src/temporal-logic/normalize_property.cpp
@@ -172,7 +172,7 @@ exprt normalize_property(exprt expr)
   else if(expr.id() == ID_sva_cycle_delay_plus)
     expr = F_exprt{X_exprt{to_sva_cycle_delay_plus_expr(expr).op()}};
   else if(expr.id() == ID_sva_cycle_delay_star)
-    expr = X_exprt{to_sva_cycle_delay_star_expr(expr).op()};
+    expr = F_exprt{to_sva_cycle_delay_star_expr(expr).op()};
   else if(expr.id() == ID_sva_if)
   {
     auto &sva_if_expr = to_sva_if_expr(expr);
diff --git a/src/temporal-logic/normalize_property.h b/src/temporal-logic/normalize_property.h
index 8c7a75e71..afffbcee2 100644
--- a/src/temporal-logic/normalize_property.h
+++ b/src/temporal-logic/normalize_property.h
@@ -35,8 +35,8 @@ Author: Daniel Kroening, dkr@amazon.com
 /// ¬¬φ --> φ
 /// ¬Gφ --> F¬φ
 /// ¬Fφ --> G¬φ
-/// [*] φ --> F φ
-/// [+] φ --> X F φ
+/// ##[*] φ --> F φ
+/// ##[+] φ --> X F φ
 /// strong(φ) --> φ
 /// weak(φ) --> φ
 /// sva_case --> ? :