BMC: Implement SVA sequence intersect

Author: kroening

CHANGELOG

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

regression/verilog/SVA/sequence_intersect1.desc

@@ -1,7 +1,12 @@
 CORE
 sequence_intersect1.sv
-
-^\[.*\] main\.x == 0 intersect main\.x == 1: FAILURE: property not supported by BMC engine$
+--bound 10
+^\[main\.p0\] main\.x == 0 intersect main\.x == 1: REFUTED$
+^\[main\.p1\] always main\.x >= 0: PROVED up to bound 10$
+^\[main\.p2\] always main\.x <= 5: PROVED up to bound 10$
+^\[main\.p3\] always main\.x <= 3: REFUTED$
+^\[main\.p4\] always \(main\.x >= 0 intersect main\.x <= 5\): PROVED up to bound 10$
+^\[main\.p5\] always \(main\.x >= 0 intersect main\.x <= 3\): REFUTED$
 ^EXIT=10$
 ^SIGNAL=0$
 --

regression/verilog/SVA/sequence_intersect1.sv

@@ -2,9 +2,27 @@ module main(input clk);
 
   reg [31:0] x = 0;
 
+  // 0, 1, 2, 3, 4, 5, 5, ...
   always @(posedge clk)
-    x<=x+1;
+    if(x<5)
+      x<=x+1;
 
+  // should fail
   initial p0: assert property (x == 0 intersect x == 1);
 
+  // should pass
+  p1: assert property (x >= 0);
+
+  // should pass
+  p2: assert property (x <= 5);
+
+  // should fail
+  p3: assert property (x <= 3);
+
+  // should pass
+  p4: assert property (x >= 0 intersect x <= 5);
+
+  // should fail
+  p5: assert property (x >= 0 intersect x <= 3);
+
 endmodule

src/trans-word-level/property.cpp

@@ -119,10 +119,6 @@ bool bmc_supports_SVA_property(const exprt &expr)
   if(has_subexpr(expr, ID_sva_sequence_throughout))
     return false;
 
-  // sva_sequence_intersect is not supported yet
-  if(has_subexpr(expr, ID_sva_sequence_intersect))
-    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

@@ -132,7 +132,33 @@ std::vector<std::pair<mp_integer, exprt>> instantiate_sequence(
   else if(expr.id() == ID_sva_sequence_intersect)
   {
     // IEEE 1800-2017 16.9.6
-    PRECONDITION(false);
+    // For the intersection of the two operand sequences to match, the following
+    // must hold:
+    // — Both the operands shall match.
+    // — The lengths of the two matches of the operand sequences shall be the same.
+    auto &intersect = to_sva_sequence_intersect_expr(expr);
+
+    const auto lhs_match_points =
+      instantiate_sequence(intersect.lhs(), t, no_timeframes);
+    const auto rhs_match_points =
+      instantiate_sequence(intersect.rhs(), t, no_timeframes);
+
+    std::vector<std::pair<mp_integer, exprt>> result;
+
+    for(auto &lhs_match : lhs_match_points)
+    {
+      for(auto &rhs_match : rhs_match_points)
+      {
+        // Same length?
+        if(lhs_match.first == rhs_match.first)
+        {
+          result.emplace_back(
+            lhs_match.first, and_exprt{lhs_match.second, rhs_match.second});
+        }
+      }
+    }
+
+    return result;
   }
   else if(expr.id() == ID_sva_sequence_first_match)
   {

src/verilog/sva_expr.h

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