Merge pull request #1343 from diffblue/cover_sequence_statement

SVA: add cover sequence

Author: tautschnig

CHANGELOG

@@ -1,5 +1,7 @@
 # EBMC 5.8
 
+* SystemVerilog: cover sequence
+
 # EBMC 5.7
 
 * Verilog: --initial-zero changes the default value from nondet to zero

regression/verilog/SVA/cover_sequence1.sv

@@ -7,9 +7,9 @@ module main(input clk);
     x++;
 
   // expected to pass
-  p0: cover property (x==2 ##1 x==3 ##1 x==4);
+  p0: cover sequence (x==2 ##1 x==3 ##1 x==4);
 
   // expected to fail
-  p1: cover property (x==2 ##1 x==3 ##1 x==5);
+  p1: cover sequence (x==2 ##1 x==3 ##1 x==5);
 
 endmodule

regression/verilog/SVA/cover_sequence2.sv

@@ -7,15 +7,15 @@ module main(input clk);
     x++;
 
   // expected to fail
-  p0: cover property (x==2 ##1 x==3 ##1 x==100);
+  p0: cover sequence (x==2 ##1 x==3 ##1 x==100);
 
   // expected to fail until x reaches 100
-  p1: cover property (x==98 ##1 x==99 ##1 x==100);
+  p1: cover sequence (x==98 ##1 x==99 ##1 x==100);
 
   // expected to pass once x reaches 5
-  p2: cover property (x==3 ##1 x==4 ##1 x==5);
+  p2: cover sequence (x==3 ##1 x==4 ##1 x==5);
 
   // expected to pass once x reaches 6
-  p3: cover property (x==4 ##1 x==5 ##1 x==6);
+  p3: cover sequence (x==4 ##1 x==5 ##1 x==6);
 
 endmodule

regression/verilog/SVA/cover_sequence3.sv

@@ -7,12 +7,12 @@ module main(input clk);
     x++;
 
   // passes with bound >=9
-  p0: cover property (1[*10]);
+  p0: cover sequence (1[*10]);
 
   // passes with bound >=3
-  p1: cover property (1[*4:10]);
+  p1: cover sequence (1[*4:10]);
 
   // passes with bound >=4
-  p2: cover property (1[*5:10]);
+  p2: cover sequence (1[*5:10]);
 
 endmodule

regression/verilog/SVA/cover_sequence4.sv

@@ -7,12 +7,12 @@ module main(input clk);
     x++;
 
   // passes with bound >=9
-  p0: cover property (1[=10]);
+  p0: cover sequence (1[=10]);
 
   // passes with bound >=3
-  p1: cover property (1[=4:10]);
+  p1: cover sequence (1[=4:10]);
 
   // passes with bound >=4
-  p2: cover property (1[=5:10]);
+  p2: cover sequence (1[=5:10]);
 
 endmodule

src/hw_cbmc_irep_ids.h

@@ -69,6 +69,7 @@ IREP_ID_ONE(sva_cycle_delay)
 IREP_ID_ONE(sva_cycle_delay_star)
 IREP_ID_ONE(sva_cycle_delay_plus)
 IREP_ID_ONE(sva_disable_iff)
+IREP_ID_ONE(sva_sequence_disable_iff)
 IREP_ID_ONE(sva_sequence_first_match)
 IREP_ID_ONE(sva_sequence_goto_repetition)
 IREP_ID_ONE(sva_sequence_intersect)
@@ -210,6 +211,7 @@ IREP_ID_ONE(verilog_immediate_cover)
 IREP_ID_ONE(verilog_assert_property)
 IREP_ID_ONE(verilog_assume_property)
 IREP_ID_ONE(verilog_cover_property)
+IREP_ID_ONE(verilog_cover_sequence)
 IREP_ID_ONE(verilog_covergroup)
 IREP_ID_ONE(verilog_restrict_property)
 IREP_ID_ONE(verilog_expect_property)

src/temporal-logic/temporal_logic.cpp

@@ -112,7 +112,8 @@ bool is_SVA_sequence_operator(const exprt &expr)
          id == ID_sva_sequence_goto_repetition ||
          id == ID_sva_sequence_non_consecutive_repetition ||
          id == ID_sva_sequence_repetition_star ||
-         id == ID_sva_sequence_repetition_plus || id == ID_sva_boolean;
+         id == ID_sva_sequence_repetition_plus || id == ID_sva_boolean ||
+         id == ID_sva_sequence_disable_iff;
 }
 
 bool is_SVA_operator(const exprt &expr)

src/temporal-logic/trivial_sva.cpp

@@ -110,6 +110,14 @@ exprt trivial_sva(exprt expr)
     auto &disable_iff_expr = to_sva_disable_iff_expr(expr);
     expr = or_exprt{disable_iff_expr.lhs(), disable_iff_expr.rhs()};
   }
+  else if(expr.id() == ID_sva_sequence_disable_iff)
+  {
+    auto &disable_iff_expr = to_sva_sequence_disable_iff_expr(expr);
+    expr = sva_or_exprt{
+      sva_boolean_exprt{disable_iff_expr.lhs(), verilog_sva_sequence_typet{}},
+      disable_iff_expr.rhs(),
+      verilog_sva_sequence_typet{}};
+  }
   else if(expr.id() == ID_sva_accept_on || expr.id() == ID_sva_sync_accept_on)
   {
     auto &sva_abort_expr = to_sva_abort_expr(expr);

src/verilog/expr2verilog.cpp

@@ -680,10 +680,10 @@ Function: expr2verilogt::convert_sva_abort
 
 expr2verilogt::resultt expr2verilogt::convert_sva_abort(
   const std::string &text,
-  const sva_abort_exprt &expr)
+  const binary_exprt &expr)
 {
-  auto op0 = convert_rec(expr.condition());
-  auto op1 = convert_rec(expr.property());
+  auto op0 = convert_rec(expr.op0());
+  auto op1 = convert_rec(expr.op1());
 
   return {verilog_precedencet::MIN, text + " (" + op0.s + ") " + op1.s};
 }
@@ -1937,6 +1937,11 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src)
     return precedence = verilog_precedencet::MIN,
            convert_sva_abort("disable iff", to_sva_abort_expr(src));
 
+  else if(src.id() == ID_sva_sequence_disable_iff)
+    return precedence = verilog_precedencet::MIN,
+           convert_sva_abort(
+             "disable iff", to_sva_sequence_disable_iff_expr(src));
+
   else if(src.id()==ID_sva_eventually)
   {
     return precedence = verilog_precedencet::MIN,

src/verilog/expr2verilog_class.h

@@ -12,7 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/bitvector_expr.h>
 #include <util/std_expr.h>
 
-class sva_abort_exprt;
 class sva_case_exprt;
 class sva_if_exprt;
 class sva_ranged_predicate_exprt;
@@ -145,7 +144,7 @@ class expr2verilogt
     const std::string &name,
     const sva_sequence_repetition_exprt &);
 
-  resultt convert_sva_abort(const std::string &name, const sva_abort_exprt &);
+  resultt convert_sva_abort(const std::string &name, const binary_exprt &);
 
   resultt
   convert_sva_indexed_binary(const std::string &name, const binary_exprt &);