BMC: implement SVA [*] and [+] for state formulas

This implements the SVA sequence repetition operators x[*] and x[+] when x
is a state formula.

Author: kroening

CHANGELOG

@@ -1,5 +1,6 @@
 # EBMC 5.6
 
+* SystemVerilog: [*] and [+] SVA operators
 * SystemVerilog: typedefs from package scopes
 * SystemVerilog: assignment patterns with keys for structs
 * SystemVerilog: unbased unsigned literals '0, '1, 'x, 'z

regression/verilog/SVA/sequence_repetition2.desc

@@ -1,13 +1,15 @@
 CORE
 sequence_repetition2.sv
 --bound 10
-^\[main\.p0\] main\.x == 0\[\*\]: FAILURE: property not supported by BMC engine$
-^\[main\.p1\] main\.x == 1\[\*\]: FAILURE: property not supported by BMC engine$
-^\[main\.p2\] \(main\.x == 0\[\+\]\) #-# main\.x == 1: FAILURE: property not supported by BMC engine$
-^\[main\.p3\] main\.x == 0\[\+\]: FAILURE: property not supported by BMC engine$
-^\[main\.p4\] main\.half_x == 0\[\*\]: FAILURE: property not supported by BMC engine$
-^\[main\.p5\] main\.x == 1\[\+\]: FAILURE: property not supported by BMC engine$
-^\[main\.p6\] \(main\.x == 0\[\+\]\) #=# main\.x == 1: FAILURE: property not supported by BMC engine$
+^\[main\.p0\] main\.x == 0\[\*\]: PROVED up to bound 10$
+^\[main\.p1\] main\.x == 1\[\*\]: PROVED up to bound 10$
+^\[main\.p2\] \(main\.x == 0\[\+\]\) #=# main\.x == 1: PROVED up to bound 10$
+^\[main\.p3\] main\.x == 0\[\+\]: PROVED up to bound 10$
+^\[main\.p4\] main\.half_x == 0\[\*\]: PROVED up to bound 10$
+^\[main\.p5\] 0\[\*\]: PROVED up to bound 10$
+^\[main\.p6\] main\.x == 1\[\+\]: REFUTED$
+^\[main\.p7\] \(main\.x == 0\[\+\]\) #-# main\.x == 1: REFUTED$
+^\[main\.p8\] 0\[\+\]: REFUTED$
 ^EXIT=10$
 ^SIGNAL=0$
 --

regression/verilog/SVA/sequence_repetition2.sv

@@ -12,12 +12,14 @@ module main(input clk);
   // should pass
   initial p0: assert property (x==0[*]);
   initial p1: assert property (x==1[*]);
-  initial p2: assert property (x==0[+] #-# x==1);
+  initial p2: assert property (x==0[+] #=# x==1);
   initial p3: assert property (x==0[+]);
   initial p4: assert property (half_x==0[*]);
+  initial p5: assert property (0[*]); // empty match
 
   // should fail
-  initial p5: assert property (x==1[+]);
-  initial p6: assert property (x==0[+] #=# x==1);
+  initial p6: assert property (x==1[+]);
+  initial p7: assert property (x==0[+] #-# x==1);
+  initial p8: assert property (0[+]);
 
 endmodule

src/trans-word-level/property.cpp

@@ -115,14 +115,6 @@ bool bmc_supports_SVA_property(const exprt &expr)
   if(has_subexpr(expr, ID_sva_sequence_within))
     return false;
 
-  // sva_sequence_repetition_plus is not supported yet
-  if(has_subexpr(expr, ID_sva_sequence_repetition_plus))
-    return false;
-
-  // sva_sequence_repetition_star is not supported yet
-  if(has_subexpr(expr, ID_sva_sequence_repetition_star))
-    return false;
-
   // sva_sequence_non_consecutive_repetition is not supported yet
   if(has_subexpr(expr, ID_sva_sequence_non_consecutive_repetition))
     return false;

src/trans-word-level/sequence.cpp

@@ -11,8 +11,10 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/arith_tools.h>
 #include <util/ebmc_util.h>
 
+#include <temporal-logic/temporal_logic.h>
 #include <verilog/sva_expr.h>
 
+#include "instantiate_word_level.h"
 #include "obligations.h"
 #include "property.h"
 
@@ -240,6 +242,36 @@ std::vector<std::pair<mp_integer, exprt>> instantiate_sequence(
     auto &repetition = to_sva_sequence_consecutive_repetition_expr(expr);
     return instantiate_sequence(repetition.lower(), t, no_timeframes);
   }
+  else if(
+    expr.id() == ID_sva_sequence_repetition_plus ||
+    expr.id() == ID_sva_sequence_repetition_star)
+  {
+    // x[+] and x[*]
+    auto &op = to_unary_expr(expr).op();
+
+    // Is x a sequence or a state predicate?
+    if(is_SVA_sequence_operator(op))
+      PRECONDITION(false); // no support
+
+    std::vector<std::pair<mp_integer, exprt>> result;
+
+    // we incrementally add conjuncts to the condition
+    exprt::operandst conjuncts;
+
+    for(mp_integer u = t; u < no_timeframes; ++u)
+    {
+      // does x hold in state u?
+      auto cond_u = instantiate(op, u, no_timeframes);
+      conjuncts.push_back(cond_u);
+      result.push_back({u, conjunction(conjuncts)});
+    }
+
+    // In addition to the above, x[*] allows an empty match.
+    if(expr.id() == ID_sva_sequence_repetition_star)
+      result.push_back({t, true_exprt{}});
+
+    return result;
+  }
   else
   {
     // not a sequence, evaluate as state predicate