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,12 @@
+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
+--
+Implementation of [=x:y] is missing.

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

regression/verilog/SVA/sequence2.desc

@@ -1,11 +1,10 @@
-KNOWNBUG
+CORE
 sequence2.sv
---bound 10 --numbered-trace
-^\[main\.p0] ##\[0:\$\] main\.x == 10: PROVED up to bound 10$
-^\[main\.p1] ##\[0:\$\] main\.x == 10: REFUTED$
+--bound 10
+^\[main\.p0] weak\(##\[0:\$\] main\.x == 10\): PROVED up to bound 10$
+^\[main\.p1] strong\(##\[0:\$\] main\.x == 10\): REFUTED$
 ^EXIT=10$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-strong(...) is missing.

regression/verilog/SVA/sequence3.desc

@@ -1,13 +1,12 @@
-KNOWNBUG
+CORE
 sequence3.sv
 --bound 20 --numbered-trace
-^\[main\.p0\] ##\[\*\] main\.x == 6: REFUTED$
-^\[main\.p1\] ##\[\*\] main\.x == 5: PROVED up to bound 20$
-^\[main\.p2\] ##\[\+\] main\.x == 0: REFUTED$
-^\[main\.p3\] ##\[\+\] main\.x == 5: PROVED up to bound 20$
+^\[main\.p0\] strong\(##\[\*\] main\.x == 6\): REFUTED$
+^\[main\.p1\] strong\(##\[\*\] main\.x == 5\): PROVED up to bound 20$
+^\[main\.p2\] strong\(##\[\+\] main\.x == 0\): REFUTED$
+^\[main\.p3\] strong\(##\[\+\] main\.x == 5\): PROVED up to bound 20$
 ^EXIT=10$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-strong(...) is missing

regression/verilog/SVA/strong1.desc

@@ -1,7 +1,7 @@
 CORE
 strong1.sv
---bound 20
-^\[main\.p0\] strong\(##\[0:9\] main\.x == 100\): REFUTED$
+--bound 4
+^\[main\.p0\] strong\(##\[0:9\] main\.x == 5\): REFUTED$
 ^EXIT=10$
 ^SIGNAL=0$
 --

regression/verilog/SVA/strong1.sv

@@ -8,7 +8,7 @@ module main;
   always @(posedge clk)
     x<=x+1;
 
-  // fails
-  initial p0: assert property (strong(##[0:9] x==100));
+  // fails if bound is too low
+  initial p0: assert property (strong(##[0:9] x==5));
 
 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;