BMC world-level: empty matches

SVA empty matches do not evaluate to true when used as property.

Author: kroening

regression/verilog/SVA/empty_sequence1.desc

@@ -1,9 +1,10 @@
-KNOWNBUG
+CORE
 empty_sequence1.sv
 --bound 5
+^\[main\.p0\] 1 \[\*0\]: REFUTED$
+^\[main\.p1\] 1 \[\*0\] ##1 main\.x == 0: REFUTED$
 ^EXIT=10$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-Repetition with zero is not implemented.

regression/verilog/SVA/sequence_repetition2.desc

@@ -2,11 +2,11 @@ CORE
 sequence_repetition2.sv
 --bound 10
 ^\[main\.p0\] main\.x == 0 \[\*\]: PROVED up to bound 10$
-^\[main\.p1\] main\.x == 1 \[\*\]: PROVED up to bound 10$
-^\[main\.p2\] \(main\.x == 0 \[\+\]\) #=# main\.x == 1: PROVED up to bound 10$
-^\[main\.p3\] main\.x == 0 \[\+\]: PROVED up to bound 10$
-^\[main\.p4\] main\.half_x == 0 \[\*\]: PROVED up to bound 10$
-^\[main\.p5\] 0 \[\*\]: PROVED up to bound 10$
+^\[main\.p1\] \(main\.x == 0 \[\+\]\) #=# main\.x == 1: PROVED up to bound 10$
+^\[main\.p2\] main\.x == 0 \[\+\]: PROVED up to bound 10$
+^\[main\.p3\] main\.half_x == 0 \[\*\]: PROVED up to bound 10$
+^\[main\.p4\] main\.x == 1 \[\*\]: REFUTED$
+^\[main\.p5\] 0 \[\*\]: REFUTED$
 ^\[main\.p6\] main\.x == 1 \[\+\]: REFUTED$
 ^\[main\.p7\] \(main\.x == 0 \[\+\]\) #-# main\.x == 1: REFUTED$
 ^\[main\.p8\] 0 \[\+\]: REFUTED$

regression/verilog/SVA/sequence_repetition2.sv

@@ -11,13 +11,13 @@ module main(input clk);
 
   // should pass
   initial p0: assert property (x==0[*]);
-  initial p1: assert property (x==1[*]);
-  initial p2: assert property (x==0[+] #=# x==1);
-  initial p3: assert property (x==0[+]);
-  initial p4: assert property (half_x==0[*]);
-  initial p5: assert property (0[*]); // empty match
+  initial p1: assert property (x==0[+] #=# x==1);
+  initial p2: assert property (x==0[+]);
+  initial p3: assert property (half_x==0[*]);
 
   // should fail
+  initial p4: assert property (x==1[*]);
+  initial p5: assert property (0[*]); // empty match
   initial p6: assert property (x==1[+]);
   initial p7: assert property (x==0[+] #-# x==1);
   initial p8: assert property (0[+]);

src/trans-word-level/property.cpp

@@ -557,7 +557,8 @@ static obligationst property_obligations_rec(
       for(auto &match : matches)
       {
         // The sequence must not match.
-        obligations.add(match.end_time, not_exprt{match.condition});
+        if(!match.empty_match())
+          obligations.add(match.end_time, not_exprt{match.condition});
       }
 
       return obligations;
@@ -700,8 +701,12 @@ static obligationst property_obligations_rec(
 
     for(auto &match : matches)
     {
-      disjuncts.push_back(match.condition);
-      max = std::max(max, match.end_time);
+      // empty matches are not considered
+      if(!match.empty_match())
+      {
+        disjuncts.push_back(match.condition);
+        max = std::max(max, match.end_time);
+      }
     }
 
     return obligationst{max, disjunction(disjuncts)};

src/trans-word-level/sequence.cpp

@@ -368,7 +368,7 @@ sequence_matchest instantiate_sequence(
     if(repetition.is_empty_match())
     {
       // [*0] denotes the empty match
-      return {{t, true_exprt{}}};
+      return {sequence_matcht::empty_match(t)};
     }
     else if(repetition.is_unbounded() && repetition.repetitions_given())
     {

src/trans-word-level/sequence.h

@@ -19,12 +19,30 @@ class sequence_matcht
 {
 public:
   sequence_matcht(mp_integer __end_time, exprt __condition)
-    : end_time(std::move(__end_time)), condition(std::move(__condition))
+    : _is_empty_match(false),
+      end_time(std::move(__end_time)),
+      condition(std::move(__condition))
   {
   }
 
+  bool empty_match() const
+  {
+    return _is_empty_match;
+  }
+
+protected:
+  bool _is_empty_match;
+
+public:
   mp_integer end_time;
   exprt condition;
+
+  static sequence_matcht empty_match(mp_integer end_time)
+  {
+    auto result = sequence_matcht{end_time, true_exprt{}};
+    result._is_empty_match = true;
+    return result;
+  }
 };
 
 /// A set of matches of an SVA sequence.