Merge pull request #861 from diffblue/sva-sequence-throughout

BMC: implement SVA sequence throughout

Author: tautschnig

CHANGELOG

@@ -4,6 +4,7 @@
 * BMC: iterative constraint strengthening is now default;
   use --bmc-with-assumptions to re-enable the previous algorithm.
 * BMC: support SVA sequence intersect
+* BMC: support SVA sequence throughout
 * SystemVerilog: streaming concatenation {<<{...}} and {>>{...}}
 * SystemVerilog: set membership operator
 * SystemVerilog: named sequences

regression/verilog/SVA/sequence_throughout1.desc

@@ -1,7 +1,9 @@
 CORE
 sequence_throughout1.sv
-
-^\[.*\] main\.x == 0 throughout main\.x == 1: FAILURE: property not supported by BMC engine$
+--bound 10
+^\[main\.p0\] main\.x >= 0 throughout \(main\.x == 0 ##1 main\.x == 1 ##1 main\.x == 2\): PROVED up to bound 10$
+^\[main\.p1\] main\.x <= 1 throughout \(main\.x == 0 ##1 main\.x == 1 ##1 main\.x == 2\): REFUTED$
+^\[main\.p2\] 1 throughout \(main\.x == 0 ##1 main\.x == 1 ##1 main\.x == 3\): REFUTED$
 ^EXIT=10$
 ^SIGNAL=0$
 --

regression/verilog/SVA/sequence_throughout1.sv

@@ -5,6 +5,13 @@ module main(input clk);
   always @(posedge clk)
     x<=x+1;
 
-  initial p0: assert property (x == 0 throughout x == 1);
+  // should pass
+  initial p0: assert property (x >= 0 throughout x==0 ##1 x==1 ##1 x==2);
+
+  // should fail owing to LHS
+  initial p1: assert property (x <= 1 throughout x==0 ##1 x==1 ##1 x==2);
+
+  // should fail owing to RHS
+  initial p2: assert property (1 throughout x==0 ##1 x==1 ##1 x==3);
 
 endmodule

src/trans-word-level/property.cpp

@@ -115,10 +115,6 @@ bool bmc_supports_SVA_property(const exprt &expr)
   if(has_subexpr(expr, ID_sva_sequence_first_match))
     return false;
 
-  // sva_sequence_troughout is not supported yet
-  if(has_subexpr(expr, ID_sva_sequence_throughout))
-    return false;
-
   // sva_sequence_within is not supported yet
   if(has_subexpr(expr, ID_sva_sequence_within))
     return false;

src/trans-word-level/sequence.cpp

@@ -166,7 +166,32 @@ std::vector<std::pair<mp_integer, exprt>> instantiate_sequence(
   }
   else if(expr.id() == ID_sva_sequence_throughout)
   {
-    PRECONDITION(false);
+    // IEEE 1800-2017 16.9.9
+    // exp throughout seq matches along an interval provided
+    // - seq matches along the interval and
+    // - exp evaluates to true at each clock tick of the interval.
+    auto &throughout = to_sva_sequence_throughout_expr(expr);
+
+    const auto rhs_match_points =
+      instantiate_sequence(throughout.rhs(), t, no_timeframes);
+
+    std::vector<std::pair<mp_integer, exprt>> result;
+
+    for(auto &rhs_match : rhs_match_points)
+    {
+      exprt::operandst conjuncts = {rhs_match.second};
+
+      for(mp_integer new_t = t; new_t <= rhs_match.first; ++new_t)
+      {
+        auto obligations =
+          property_obligations(throughout.lhs(), new_t, no_timeframes);
+        conjuncts.push_back(obligations.conjunction().second);
+      }
+
+      result.emplace_back(rhs_match.first, conjunction(conjuncts));
+    }
+
+    return result;
   }
   else if(expr.id() == ID_sva_sequence_within)
   {

src/verilog/sva_expr.h

@@ -1206,4 +1206,29 @@ to_sva_sequence_intersect_expr(exprt &expr)
   return static_cast<sva_sequence_intersect_exprt &>(expr);
 }
 
+class sva_sequence_throughout_exprt : public binary_exprt
+{
+public:
+  sva_sequence_throughout_exprt(exprt op0, exprt op1)
+    : binary_exprt(std::move(op0), ID_sva_sequence_throughout, std::move(op1))
+  {
+  }
+};
+
+static inline const sva_sequence_throughout_exprt &
+to_sva_sequence_throughout_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_sva_sequence_throughout);
+  sva_sequence_throughout_exprt::check(expr, validation_modet::INVARIANT);
+  return static_cast<const sva_sequence_throughout_exprt &>(expr);
+}
+
+static inline sva_sequence_throughout_exprt &
+to_sva_sequence_throughout_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_sva_sequence_throughout);
+  sva_sequence_throughout_exprt::check(expr, validation_modet::INVARIANT);
+  return static_cast<sva_sequence_throughout_exprt &>(expr);
+}
+
 #endif