BMC: implement weak/strong sequences

This implements strong semantics for SVA sequences in the word-level BMC
engine.  Strong semantics are used with an explicit strong(...) operator or
for SVA cover.

The difference between weak and strong semantics arises in BMC when the
sequence reaches the end of the unwinding: using weak semantics, the
sequence matches, whereas using strong semantics the sequence does not.

Author: kroening

regression/verilog/SVA/cover_sequence2.desc

@@ -1,11 +1,12 @@
-KNOWNBUG
+CORE
 cover_sequence2.sv
---bound 2
-^\[main\.p0\] cover \(main\.x == 2 ##1 main\.x == 3 ##1 main\.x == 100\): PROVED$
-^\[main\.p1\] cover \(main\.x == 98 ##1 main\.x == 99 ##1 main\.x == 100\): REFUTED up to bound 2$
+--bound 5
+^\[main\.p0\] cover \(main\.x == 2 ##1 main\.x == 3 ##1 main\.x == 100\): REFUTED up to bound 5$
+^\[main\.p1\] cover \(main\.x == 98 ##1 main\.x == 99 ##1 main\.x == 100\): REFUTED up to bound 5$
+^\[main\.p2\] cover \(main\.x == 3 ##1 main\.x == 4 ##1 main\.x == 5\): PROVED$
+^\[main\.p3\] cover \(main\.x == 4 ##1 main\.x == 5 ##1 main\.x == 6\): REFUTED up to bound 5$
 ^EXIT=10$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-Cover property p0 cannot ever hold, but is shown proven when using a small bound.

regression/verilog/SVA/cover_sequence2.sv

@@ -1,15 +1,21 @@
 module main(input clk);
 
   // count up
-  reg [7:0] x = 0;
+  int x = 0;
 
-  always @(posedge clk)
+  always_ff @(posedge clk)
     x++;
 
   // expected to fail
   p0: cover property (x==2 ##1 x==3 ##1 x==100);
 
-  // expected to fail until bound reaches 100
+  // expected to fail until x reaches 100
   p1: cover property (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);
+
+  // expected to pass once x reaches 6
+  p3: cover property (x==4 ##1 x==5 ##1 x==6);
+
 endmodule

regression/verilog/SVA/cover_sequence3.desc

@@ -0,0 +1,11 @@
+CORE
+cover_sequence3.sv
+--bound 3
+^\[main\.p0\] cover \(1 \[\*10\]\): REFUTED up to bound 3$
+^\[main\.p1\] cover \(1 \[\*4:10\]\): PROVED$
+^\[main\.p2\] cover \(1 \[\*5:10\]\): REFUTED up to bound 3$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/SVA/cover_sequence3.sv

@@ -0,0 +1,18 @@
+module main(input clk);
+
+  // count up
+  int x = 0;
+
+  always_ff @(posedge clk)
+    x++;
+
+  // passes with bound >=9
+  p0: cover property (1[*10]);
+
+  // passes with bound >=3
+  p1: cover property (1[*4:10]);
+
+  // passes with bound >=4
+  p2: cover property (1[*5:10]);
+
+endmodule

regression/verilog/SVA/cover_sequence4.desc

@@ -0,0 +1,11 @@
+KNOWNBUG
+cover_sequence4.sv
+--bound 3
+^\[main\.p0\] cover \(1 \[=10\]\): REFUTED up to bound 3$
+^\[main\.p1\] cover \(1 \[=4:10\]\): PROVED$
+^\[main\.p2\] cover \(1 \[=5:10\]\): REFUTED up to bound 3$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/SVA/cover_sequence4.sv

@@ -0,0 +1,18 @@
+module main(input clk);
+
+  // count up
+  int x = 0;
+
+  always_ff @(posedge clk)
+    x++;
+
+  // passes with bound >=9
+  p0: cover property (1[=10]);
+
+  // passes with bound >=3
+  p1: cover property (1[=4:10]);
+
+  // passes with bound >=4
+  p2: cover property (1[=5:10]);
+
+endmodule

src/trans-word-level/property.cpp

@@ -530,8 +530,17 @@ static obligationst property_obligations_rec(
       // The sequence must not match.
       auto &sequence = to_sva_sequence_property_expr_base(op).sequence();
 
+      // clang-format off
+      auto semantics =
+          op.id() == ID_sva_strong ? sva_sequence_semanticst::STRONG
+        : op.id() == ID_sva_weak ? sva_sequence_semanticst::WEAK
+        : op.id() == ID_sva_implicit_strong ? sva_sequence_semanticst::STRONG
+        : op.id() == ID_sva_implicit_weak ? sva_sequence_semanticst::WEAK
+        : sva_sequence_semanticst::WEAK;
+      // clang-format on
+
       const auto matches =
-        instantiate_sequence(sequence, current, no_timeframes);
+        instantiate_sequence(sequence, semantics, current, no_timeframes);
 
       obligationst obligations;
 
@@ -577,10 +586,13 @@ static obligationst property_obligations_rec(
     auto &implication = to_binary_expr(property_expr);
 
     // The LHS is a sequence, the RHS is a property.
-    // The implication must hold for _all_ matches on the LHS,
+    // The implication must hold for _all_ (strong) matches on the LHS,
     // i.e., each pair of LHS match and RHS obligation yields an obligation.
-    const auto lhs_match_points =
-      instantiate_sequence(implication.lhs(), current, no_timeframes);
+    const auto lhs_match_points = instantiate_sequence(
+      implication.lhs(),
+      sva_sequence_semanticst::STRONG,
+      current,
+      no_timeframes);
 
     obligationst result;
 
@@ -620,9 +632,12 @@ static obligationst property_obligations_rec(
     // the result is a property expression.
     auto &followed_by = to_sva_followed_by_expr(property_expr);
 
-    // get match points for LHS sequence
-    auto matches =
-      instantiate_sequence(followed_by.antecedent(), current, no_timeframes);
+    // get (proper) match points for LHS sequence
+    auto matches = instantiate_sequence(
+      followed_by.antecedent(),
+      sva_sequence_semanticst::STRONG,
+      current,
+      no_timeframes);
 
     exprt::operandst disjuncts;
     mp_integer t = current;
@@ -663,9 +678,19 @@ static obligationst property_obligations_rec(
     auto &sequence =
       to_sva_sequence_property_expr_base(property_expr).sequence();
 
+    // clang-format off
+    auto semantics =
+        property_expr.id() == ID_sva_strong ? sva_sequence_semanticst::STRONG
+      : property_expr.id() == ID_sva_weak ? sva_sequence_semanticst::WEAK
+      : property_expr.id() == ID_sva_implicit_strong ? sva_sequence_semanticst::STRONG
+      : property_expr.id() == ID_sva_implicit_weak ? sva_sequence_semanticst::WEAK
+      : sva_sequence_semanticst::WEAK;
+    // clang-format on
+
     // sequence expressions -- these may have multiple potential
     // match points, and evaluate to true if any of them matches
-    const auto matches = instantiate_sequence(sequence, current, no_timeframes);
+    const auto matches =
+      instantiate_sequence(sequence, semantics, current, no_timeframes);
     exprt::operandst disjuncts;
     disjuncts.reserve(matches.size());
     mp_integer max = current;

src/trans-word-level/sequence.cpp

@@ -9,7 +9,6 @@ Author: Daniel Kroening, [email protected]
 #include "sequence.h"
 
 #include <util/arith_tools.h>
-#include <util/ebmc_util.h>
 
 #include <temporal-logic/temporal_logic.h>
 #include <verilog/sva_expr.h>
@@ -20,6 +19,7 @@ Author: Daniel Kroening, [email protected]
 
 sequence_matchest instantiate_sequence(
   exprt expr,
+  sva_sequence_semanticst semantics,
   const mp_integer &t,
   const mp_integer &no_timeframes)
 {
@@ -32,17 +32,21 @@ sequence_matchest instantiate_sequence(
     {
       const auto u = t + from;
 
-      // Do we exceed the bound? Make it 'true'
+      // Do we exceed the bound? Make it 'false'/'true', depending
+      // on semantics.
       if(u >= no_timeframes)
       {
         DATA_INVARIANT(no_timeframes != 0, "must have timeframe");
-        return {{no_timeframes - 1, true_exprt()}};
+        if(semantics == sva_sequence_semanticst::WEAK)
+          return {{no_timeframes - 1, true_exprt{}}};
+        else         // STRONG
+          return {}; // no match
       }
       else
         return instantiate_sequence(
-          sva_cycle_delay_expr.op(), u, no_timeframes);
+          sva_cycle_delay_expr.op(), semantics, u, no_timeframes);
     }
-    else
+    else // ##[from:to] something
     {
       mp_integer to;
 
@@ -51,25 +55,34 @@ sequence_matchest instantiate_sequence(
         DATA_INVARIANT(no_timeframes != 0, "must have timeframe");
         to = no_timeframes - 1;
       }
-      else if(to_integer_non_constant(sva_cycle_delay_expr.to(), to))
+      else if(!sva_cycle_delay_expr.to().is_constant())
         throw "failed to convert sva_cycle_delay offsets";
+      else
+        to = numeric_cast_v<mp_integer>(
+          to_constant_expr(sva_cycle_delay_expr.to()));
 
       auto lower = t + from;
       auto upper = t + to;
 
-      // Do we exceed the bound? Make it 'true'
+      // Do we exceed the bound? Make it 'true' if we are doing
+      // weak semantics.
       if(upper >= no_timeframes)
       {
-        DATA_INVARIANT(no_timeframes != 0, "must have timeframe");
-        return {{no_timeframes - 1, true_exprt()}};
+        if(semantics == sva_sequence_semanticst::WEAK)
+        {
+          DATA_INVARIANT(no_timeframes != 0, "must have timeframe");
+          return {{no_timeframes - 1, true_exprt()}};
+        }
+        else
+          upper = no_timeframes - 1;
       }
 
       sequence_matchest matches;
 
       for(mp_integer u = lower; u <= upper; ++u)
       {
-        auto sub_result =
-          instantiate_sequence(sva_cycle_delay_expr.op(), u, no_timeframes);
+        auto sub_result = instantiate_sequence(
+          sva_cycle_delay_expr.op(), semantics, u, no_timeframes);
         for(auto &match : sub_result)
           matches.push_back(match);
       }
@@ -84,21 +97,25 @@ sequence_matchest instantiate_sequence(
 
     // This is the product of the match points on the LHS and RHS
     const auto lhs_matches =
-      instantiate_sequence(implication.lhs(), t, no_timeframes);
+      instantiate_sequence(implication.lhs(), semantics, t, no_timeframes);
 
     for(auto &lhs_match : lhs_matches)
     {
       auto t_rhs = lhs_match.end_time;
 
-      // Do we exceed the bound? Make it 'true'
+      // Do we exceed the bound? Make it 'false'/'true', depending
+      // on semantics.
       if(t_rhs >= no_timeframes)
       {
         DATA_INVARIANT(no_timeframes != 0, "must have timeframe");
-        return {{no_timeframes - 1, true_exprt()}};
+        if(semantics == sva_sequence_semanticst::WEAK)
+          return {{no_timeframes - 1, true_exprt{}}};
+        else         // STRONG
+          return {}; // no match
       }
 
-      const auto rhs_matches =
-        instantiate_sequence(implication.rhs(), t_rhs, no_timeframes);
+      const auto rhs_matches = instantiate_sequence(
+        implication.rhs(), semantics, t_rhs, no_timeframes);
 
       for(auto &rhs_match : rhs_matches)
       {
@@ -119,9 +136,9 @@ sequence_matchest instantiate_sequence(
     auto &intersect = to_sva_sequence_intersect_expr(expr);
 
     const auto lhs_matches =
-      instantiate_sequence(intersect.lhs(), t, no_timeframes);
+      instantiate_sequence(intersect.lhs(), semantics, t, no_timeframes);
     const auto rhs_matches =
-      instantiate_sequence(intersect.rhs(), t, no_timeframes);
+      instantiate_sequence(intersect.rhs(), semantics, t, no_timeframes);
 
     sequence_matchest result;
 
@@ -146,7 +163,7 @@ sequence_matchest instantiate_sequence(
     auto &first_match = to_sva_sequence_first_match_expr(expr);
 
     const auto lhs_matches =
-      instantiate_sequence(first_match.lhs(), t, no_timeframes);
+      instantiate_sequence(first_match.lhs(), semantics, t, no_timeframes);
 
     // the match of seq with the earliest ending clock tick is a
     // match of first_match (seq)
@@ -183,7 +200,7 @@ sequence_matchest instantiate_sequence(
     auto &throughout = to_sva_sequence_throughout_expr(expr);
 
     const auto rhs_matches =
-      instantiate_sequence(throughout.rhs(), t, no_timeframes);
+      instantiate_sequence(throughout.rhs(), semantics, t, no_timeframes);
 
     sequence_matchest result;
 
@@ -210,16 +227,16 @@ sequence_matchest instantiate_sequence(
 
     auto &within_expr = to_sva_sequence_within_expr(expr);
     const auto matches_rhs =
-      instantiate_sequence(within_expr.rhs(), t, no_timeframes);
+      instantiate_sequence(within_expr.rhs(), semantics, 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);
+        auto matches_lhs = instantiate_sequence(
+          within_expr.lhs(), semantics, start_lhs, no_timeframes);
 
         for(auto &match_lhs : matches_lhs)
         {
@@ -245,8 +262,10 @@ sequence_matchest instantiate_sequence(
     // 3. The end time of the composite sequence is
     //    the end time of the operand sequence that completes last.
     auto &and_expr = to_sva_and_expr(expr);
-    auto matches_lhs = instantiate_sequence(and_expr.lhs(), t, no_timeframes);
-    auto matches_rhs = instantiate_sequence(and_expr.rhs(), t, no_timeframes);
+    auto matches_lhs =
+      instantiate_sequence(and_expr.lhs(), semantics, t, no_timeframes);
+    auto matches_rhs =
+      instantiate_sequence(and_expr.rhs(), semantics, t, no_timeframes);
 
     sequence_matchest result;
 
@@ -268,7 +287,7 @@ sequence_matchest instantiate_sequence(
     sequence_matchest result;
 
     for(auto &op : expr.operands())
-      for(auto &match : instantiate_sequence(op, t, no_timeframes))
+      for(auto &match : instantiate_sequence(op, semantics, t, no_timeframes))
         result.push_back(match);
 
     return result;
@@ -277,7 +296,8 @@ sequence_matchest instantiate_sequence(
   {
     // x[*n] is syntactic sugar for x ##1 ... ##1 x, with n repetitions
     auto &repetition = to_sva_sequence_consecutive_repetition_expr(expr);
-    return instantiate_sequence(repetition.lower(), t, no_timeframes);
+    return instantiate_sequence(
+      repetition.lower(), semantics, t, no_timeframes);
   }
   else if(
     expr.id() == ID_sva_sequence_repetition_plus ||

src/trans-word-level/sequence.h

@@ -12,6 +12,8 @@ Author: Daniel Kroening, [email protected]
 #include <util/expr.h>
 #include <util/mp_arith.h>
 
+#include <verilog/sva_expr.h>
+
 /// A match for an SVA sequence.
 class sequence_matcht
 {
@@ -32,6 +34,7 @@ using sequence_matchest = std::vector<sequence_matcht>;
 /// for the given sequence expression starting at time t
 [[nodiscard]] sequence_matchest instantiate_sequence(
   exprt expr,
+  sva_sequence_semanticst,
   const mp_integer &t,
   const mp_integer &no_timeframes);