bugfix for SVA cover

This changes the implicit 'always' used for SVA cover properties from LTL G
to SVA always.  This avoids a mixture of LTL and SVA, which is not supported
by the BMC backend.

Author: kroening

regression/verilog/SVA/cover_sequence1.desc

@@ -0,0 +1,11 @@
+CORE
+cover_sequence1.sv
+--bound 10 --numbered-trace
+^\[main\.p0\] cover \(main\.x == 2 ##1 main\.x == 3 ##1 main\.x == 4\): PROVED$
+^Trace with 5 states:$
+^\[main\.p1\] cover \(main\.x == 2 ##1 main\.x == 3 ##1 main\.x == 5\): REFUTED up to bound 10$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/SVA/cover_sequence1.sv

@@ -0,0 +1,15 @@
+module main(input clk);
+
+  // count up
+  reg [7:0] x = 0;
+
+  always @(posedge clk)
+    x++;
+
+  // expected to pass
+  p0: cover property (x==2 ##1 x==3 ##1 x==4);
+
+  // expected to fail
+  p1: cover property (x==2 ##1 x==3 ##1 x==5);
+
+endmodule

src/temporal-logic/normalize_property.cpp

@@ -119,7 +119,7 @@ exprt normalize_property(exprt expr)
 {
   // top-level only
   if(expr.id() == ID_sva_cover)
-    expr = G_exprt{not_exprt{to_sva_cover_expr(expr).op()}};
+    expr = sva_always_exprt{not_exprt{to_sva_cover_expr(expr).op()}};
 
   expr = trivial_sva(expr);
 

src/temporal-logic/normalize_property.h

@@ -34,6 +34,7 @@ Author: Daniel Kroening, [email protected]
 /// weak(φ) --> φ
 /// ¬ sva_s_eventually φ --> sva_always ¬φ
 /// ¬ sva_always φ --> sva_s_eventually ¬φ
+/// cover φ --> sva_always_exprt ¬φ
 ///
 /// ----LTL-----
 /// ¬Xφ --> X¬φ