Merge pull request #1159 from diffblue/sequence-implication-fix

world-level BMC: fix for `|->` and `|=>` for empty matches

Author: kroening

CHANGELOG

@@ -4,6 +4,7 @@
 * Verilog: fix for named generate blocks
 * Verilog: $onehot and $onehot0 are now elaboration-time constant
 * SystemVerilog: fix for #-# and #=# for empty matches
+* SystemVerilog: fix for |-> and |=> for empty matches
 * LTL/SVA to Buechi with --buechi
 
 # EBMC 5.6

regression/verilog/SVA/sequence_implication3.bdd.desc

@@ -0,0 +1,10 @@
+CORE
+sequence_implication3.sv
+--module main --bdd
+^\[main\.p0\] \(1 \[\*0\]\) \|=> main\.x == 1: REFUTED$
+^\[main\.p1\] \(1 \[\*0\]\) \|=> main\.x == 0: PROVED$
+^\[main\.p2\] \(1 \[\*0\]\) \|-> 0: PROVED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--

regression/verilog/SVA/sequence_implication3.bmc.desc

@@ -0,0 +1,10 @@
+CORE
+sequence_implication3.sv
+--module main --bound 2
+^\[main\.p0\] \(1 \[\*0\]\) \|=> main\.x == 1: REFUTED$
+^\[main\.p1\] \(1 \[\*0\]\) \|=> main\.x == 0: PROVED up to bound 2$
+^\[main\.p2\] \(1 \[\*0\]\) \|-> 0: PROVED up to bound 2$
+^EXIT=10$
+^SIGNAL=0$
+--
+--

regression/verilog/SVA/sequence_implication3.sv

@@ -0,0 +1,21 @@
+module main(input clk);
+
+  reg [31:0] x;
+
+  initial x=0;
+
+  // 0, 1, ...
+  always @(posedge clk)
+    x<=x+1;
+
+  // expected to fail: the rhs is evaluated in time frame 0
+  initial p0: assert property (1[*0] |=> x==1);
+
+  // expected to pass: the rhs is evaluated in time frame 0
+  initial p1: assert property (1[*0] |=> x==0);
+
+  // expected to pass: the lhs is an empty match, and the implication
+  // passes vacuously
+  initial p2: assert property (1[*0] |-> 0);
+
+endmodule

src/trans-word-level/property.cpp

@@ -606,12 +606,21 @@ static obligationst property_obligations_rec(
       current,
       no_timeframes);
 
+    const bool overlapped = property_expr.id() == ID_sva_overlapped_implication;
+
     obligationst result;
 
     for(auto &lhs_match_point : lhs_match_points)
     {
-      // The RHS of the non-overlapped implication starts one timeframe later
-      auto t_rhs = property_expr.id() == ID_sva_non_overlapped_implication
+      if(lhs_match_point.empty_match() && overlapped)
+      {
+        // does not yield an obligation
+        continue;
+      }
+
+      // The RHS of the non-overlapped implication starts one timeframe later,
+      // unless the LHS is an empty match.
+      auto t_rhs = !overlapped && !lhs_match_point.empty_match()
                      ? lhs_match_point.end_time + 1
                      : lhs_match_point.end_time;