BMC: implement weak/strong sequences

CHANGELOG

@@ -9,6 +9,7 @@
 * SystemVerilog: within
 * SystemVerilog: bugfix for |-> and |=>
 * SystemVerilog: bugfix for SVA sequence and
+* SystemVerilog: strong/weak sequence semantics
 * Verilog: 'dx, 'dz
 * SMV: LTL V operator, xnor operator
 * SMV: word types and operators

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/instantiate_word_level.cpp

@@ -123,40 +123,15 @@ wl_instantiatet::instantiate_rec(exprt expr, const mp_integer &t) const
     expr.id() == ID_typecast && expr.type().id() == ID_bool &&
     to_typecast_expr(expr).op().type().id() == ID_verilog_sva_sequence)
   {
-    auto &sequence = to_typecast_expr(expr).op();
-
-    // sequence expressions -- these may have multiple potential
-    // match points, and evaluate to true if any of them matches
-    const auto matches = instantiate_sequence(sequence, t, no_timeframes);
-    exprt::operandst disjuncts;
-    disjuncts.reserve(matches.size());
-    mp_integer max = t;
-
-    for(auto &match : matches)
-    {
-      disjuncts.push_back(match.condition);
-      max = std::max(max, match.end_time);
-    }
-
-    return {max, disjunction(disjuncts)};
+    // should have been done by property_obligations_rec
+    PRECONDITION(false);
   }
-  else if(expr.id() == ID_sva_sequence_property)
+  else if(
+    expr.id() == ID_sva_sequence_property || expr.id() == ID_sva_weak ||
+    expr.id() == ID_sva_strong)
   {
-    // sequence expressions -- these may have multiple potential
-    // match points, and evaluate to true if any of them matches
-    auto &sequence = to_sva_sequence_property_expr(expr);
-    const auto matches = instantiate_sequence(sequence, t, no_timeframes);
-    exprt::operandst disjuncts;
-    disjuncts.reserve(matches.size());
-    mp_integer max = t;
-
-    for(auto &match : matches)
-    {
-      disjuncts.push_back(match.condition);
-      max = std::max(max, match.end_time);
-    }
-
-    return {max, disjunction(disjuncts)};
+    // should have been done by property_obligations_rec
+    PRECONDITION(false);
   }
   else if(expr.id() == ID_verilog_past)
   {

src/trans-word-level/property.cpp

@@ -140,6 +140,32 @@ bool bmc_supports_property(const exprt &expr)
 
 /*******************************************************************\
 
+Function: sva_sequence_semantics
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+static sva_sequence_semanticst sva_sequence_semantics(irep_idt id)
+{
+  if(id == ID_sva_strong)
+    return sva_sequence_semanticst::STRONG;
+  else if(id == ID_sva_weak)
+    return sva_sequence_semanticst::WEAK;
+  else if(id == ID_sva_implicit_strong)
+    return sva_sequence_semanticst::STRONG;
+  else if(id == ID_sva_implicit_weak)
+    return sva_sequence_semanticst::WEAK;
+  else
+    PRECONDITION(false);
+}
+
+/*******************************************************************\
+
 Function: property_obligations_rec
 
   Inputs:
@@ -527,16 +553,17 @@ static obligationst property_obligations_rec(
       op.id() == ID_sva_strong || op.id() == ID_sva_weak ||
       op.id() == ID_sva_implicit_strong || op.id() == ID_sva_implicit_weak)
     {
-      // The sequence must not match.
       auto &sequence = to_sva_sequence_property_expr_base(op).sequence();
+      auto semantics = sva_sequence_semantics(op.id());
 
       const auto matches =
-        instantiate_sequence(sequence, current, no_timeframes);
+        instantiate_sequence(sequence, semantics, current, no_timeframes);
 
       obligationst obligations;
 
       for(auto &match : matches)
       {
+        // The sequence must not match.
         obligations.add(match.end_time, not_exprt{match.condition});
       }
 
@@ -577,10 +604,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 +650,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;
@@ -660,12 +693,14 @@ static obligationst property_obligations_rec(
     property_expr.id() == ID_sva_implicit_strong ||
     property_expr.id() == ID_sva_implicit_weak)
   {
+    // sequence expressions -- these may have multiple potential
+    // match points, and evaluate to true if any of them matches
     auto &sequence =
       to_sva_sequence_property_expr_base(property_expr).sequence();
+    auto semantics = sva_sequence_semantics(property_expr.id());
 
-    // 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;