Merge pull request #773 from diffblue/issue669-implies

Update issue669.sv to use 'implies'

Author: tautschnig

regression/verilog/SVA/issue669.desc

@@ -1,6 +1,15 @@
-KNOWNBUG
+CORE
 issue669.sv
 --bound 5 --top top
+\[top\.assert\.1\] always not s_eventually 0: PROVED up to bound 5$
+\[top\.assert\.2\] always \(\(top\.a until_with top\.b\) implies \(not \(\(not top\.b\) s_until \(not top\.a\)\)\)\): PROVED up to bound 5$
+\[top\.assert\.3\] always \(\(not \(\(not top\.b\) s_until \(not top\.a\)\)\) implies \(top\.a until_with top\.b\)\): PROVED up to bound 5$
+\[top\.assert\.4\] always \(\(top\.a until_with top\.b\) implies \(top\.a until \(top\.a and top\.b\)\)\): PROVED up to bound 5$
+\[top\.assert\.5\] always \(\(top\.a until \(top\.a and top\.b\)\) implies \(top\.a until_with top\.b\)\): PROVED up to bound 5$
+\[top\.assert\.6\] always \(\(s_eventually top\.a\) implies \(1 s_until top\.a\)\): PROVED up to bound 5$
+\[top\.assert\.7\] always \(\(1 s_until top\.a\) implies \(s_eventually top\.a\)\): PROVED up to bound 5$
+\[top\.assert\.8\] always \(\(top\.a s_until top\.b\) implies \(\(s_eventually top\.b\) and \(top\.a until top\.b\)\)\): PROVED up to bound 5$
+\[top\.assert\.9\] always \(\(\(s_eventually top\.b\) and \(top\.a until top\.b\)\) implies \(top\.a s_until top\.b\)\): PROVED up to bound 5$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/SVA/issue669.sv

@@ -10,25 +10,19 @@ module top(input x, input y, input clk);
   assert property (not s_eventually 0);
 
   // Using until_with
-  assert property (a until_with b |-> not ((not b) s_until (not a)));
-  assert property (not ((not b) s_until (not a)) |-> a until_with b);
+  assert property ((a until_with b) implies not ((not b) s_until (not a)));
+  assert property (not ((not b) s_until (not a)) implies (a until_with b));
 
   // Until_with equivalence with until
-  assert property ((a until_with b) |-> (a until (a and b)));
-  assert property ((a until (a and b)) |-> (a until_with b));
-
-  // Property implies itself should always be true
-  assert property ((b or (always b)) |-> (b or (always b)));
-  assert property ((b or (always b)) implies (b or (always b)));
+  assert property ((a until_with b) implies (a until (a and b)));
+  assert property ((a until (a and b)) implies (a until_with b));
 
   // Definitions of strong eventually
-  assert property ((s_eventually a) |-> (1 s_until a));
-  assert property ((1 s_until a) |-> (s_eventually a));
+  assert property ((s_eventually a) implies (1 s_until a));
+  assert property ((1 s_until a) implies (s_eventually a));
 
   // Definitions of strong until
-  assert property ((a s_until b) |-> ((s_eventually b) and (a until b)));
   assert property ((a s_until b) implies ((s_eventually b) and (a until b)));
-  assert property (((s_eventually b) and (a until b)) |-> (a s_until b));
   assert property (((s_eventually b) and (a until b)) implies (a s_until b));
 
 endmodule