Merge pull request #679 from diffblue/sequence3-fix

SVA: fix normalization of ##[*] φ

Author: tautschnig

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$
 --

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

src/temporal-logic/normalize_property.cpp

@@ -182,7 +182,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);

src/temporal-logic/normalize_property.h

@@ -37,8 +37,8 @@ Author: Daniel Kroening, [email protected]
 /// ¬¬φ --> φ
 /// ¬Gφ --> F¬φ
 /// ¬Fφ --> G¬φ
-/// [*] φ --> F φ
-/// [+] φ --> X F φ
+/// ##[*] φ --> F φ
+/// ##[+] φ --> X F φ
 /// strong(φ) --> φ
 /// weak(φ) --> φ
 /// sva_case --> ? :