BMC: SVA sequence within

This implements the SVA sequence within operator in the word-level BMC
backend.

Author: kroening

CHANGELOG

@@ -6,6 +6,7 @@
 * SystemVerilog: unbased unsigned literals '0, '1, 'x, 'z
 * SystemVerilog: first_match
 * SystemVerilog: [->n] and [=n]
+* SystemVerilog: within
 * SystemVerilog: bugfix for |-> and |=>
 * SystemVerilog: bugfix for SVA sequence and
 * Verilog: 'dx, 'dz

regression/verilog/SVA/sequence_within1.desc

@@ -1,7 +1,11 @@
 CORE
 sequence_within1.sv
---bound 5
-^\[.*\] main\.x == 0 within main\.x == 1: FAILURE: property not supported by BMC engine$
+--bound 20
+^\[main\.p0\] main\.x == 0 within main\.x == 1: REFUTED$
+^\[main\.p1\] main\.x == 0 within \(##10 1\): PROVED up to bound 20$
+^\[main\.p2\] main\.x == 5 within \(##10 1\): PROVED up to bound 20$
+^\[main\.p3\] main\.x == 10 within \(##10 1\): PROVED up to bound 20$
+^\[main\.p4\] main\.x == 11 within \(##10 1\): REFUTED$
 ^EXIT=10$
 ^SIGNAL=0$
 --

regression/verilog/SVA/sequence_within1.sv

@@ -1,10 +1,23 @@
 module main(input clk);
 
-  reg [31:0] x = 0;
+  reg [7:0] x = 0;
 
   always @(posedge clk)
     x<=x+1;
 
+  // fails, no rhs match
   initial p0: assert property (x == 0 within x == 1);
 
+  // passes, lhs match at beginning of rhs match
+  initial p1: assert property (x == 0 within ##10 1);
+
+  // passes, lhs match in the middle of rhs match
+  initial p2: assert property (x == 5 within ##10 1);
+
+  // passes, lhs match at the end of rhs match
+  initial p3: assert property (x == 10 within ##10 1);
+
+  // fails, lhs match just beyond the rhs match
+  initial p4: assert property (x == 11 within ##10 1);
+
 endmodule

src/trans-word-level/property.cpp

@@ -111,10 +111,6 @@ Function: bmc_supports_SVA_property
 
 bool bmc_supports_SVA_property(const exprt &expr)
 {
-  // sva_sequence_within is not supported yet
-  if(has_subexpr(expr, ID_sva_sequence_within))
-    return false;
-
   return true;
 }
 

src/trans-word-level/sequence.cpp

@@ -205,7 +205,37 @@ sequence_matchest instantiate_sequence(
   }
   else if(expr.id() == ID_sva_sequence_within)
   {
-    PRECONDITION(false);
+    // If the lhs match is contained anywhere within the rhs match,
+    // then return the rhs match.
+
+    auto &within_expr = to_sva_sequence_within_expr(expr);
+    const auto matches_rhs =
+      instantiate_sequence(within_expr.rhs(), t, no_timeframes);
+
+    sequence_matchest result;
+
+    for(auto &match_rhs : matches_rhs)
+    {
+      for(auto start_lhs = t; start_lhs <= match_rhs.end_time; ++start_lhs)
+      {
+        auto matches_lhs =
+          instantiate_sequence(within_expr.lhs(), start_lhs, no_timeframes);
+
+        for(auto &match_lhs : matches_lhs)
+        {
+          // The end_time of the lhs match must be no later than the
+          // end_time of the rhs match.
+          if(match_lhs.end_time <= match_rhs.end_time)
+          {
+            // return the rhs end_time
+            auto cond = and_exprt{match_lhs.condition, match_rhs.condition};
+            result.emplace_back(match_rhs.end_time, std::move(cond));
+          }
+        }
+      }
+    }
+
+    return result;
   }
   else if(expr.id() == ID_sva_and)
   {

src/verilog/sva_expr.h

@@ -1498,6 +1498,35 @@ to_sva_sequence_intersect_expr(exprt &expr)
   return static_cast<sva_sequence_intersect_exprt &>(expr);
 }
 
+class sva_sequence_within_exprt : public binary_exprt
+{
+public:
+  explicit sva_sequence_within_exprt(exprt op0, exprt op1)
+    : binary_exprt(
+        std::move(op0),
+        ID_sva_sequence_within,
+        std::move(op1),
+        verilog_sva_sequence_typet{})
+  {
+  }
+};
+
+static inline const sva_sequence_within_exprt &
+to_sva_sequence_within_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_sva_sequence_within);
+  sva_sequence_within_exprt::check(expr, validation_modet::INVARIANT);
+  return static_cast<const sva_sequence_within_exprt &>(expr);
+}
+
+static inline sva_sequence_within_exprt &
+to_sva_sequence_within_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_sva_sequence_within);
+  sva_sequence_within_exprt::check(expr, validation_modet::INVARIANT);
+  return static_cast<sva_sequence_within_exprt &>(expr);
+}
+
 class sva_sequence_throughout_exprt : public binary_exprt
 {
 public:

src/verilog/verilog_typecheck_sva.cpp

@@ -239,7 +239,6 @@ exprt verilog_typecheck_exprt::convert_binary_sva(binary_exprt expr)
 
     convert_sva(expr.rhs());
     require_sva_sequence(expr.rhs());
-    expr.type() = bool_typet{};
 
     expr.type() = verilog_sva_sequence_typet{};