world-level BMC: implement two empty match rules

This implements two SVA empty match rules in the word-level BMC encoding.

Author: kroening

regression/verilog/SVA/empty_sequence1.bmc.desc

@@ -0,0 +1,13 @@
+CORE
+empty_sequence1.sv
+--bound 5
+^\[main\.p0\] 1 \[\*0\]: REFUTED$
+^\[main\.p1\] \(1 \[\*0\]\) ##1 main\.x == 0: PROVED up to bound 5$
+^\[main\.p2\] main\.x == 0 ##1 \(1 \[\*0\]\): PROVED up to bound 5$
+^\[main\.p3\] \(1 \[\*0\]\) ##0 1: REFUTED$
+^\[main\.p4\] 1 ##0 \(1 \[\*0\]\): PROVED up to bound 5$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/SVA/empty_sequence1.desc

@@ -8,7 +8,12 @@ module main(input clk);
   // The empty sequence does not match
   initial p0: assert property (1[*0]);
 
-  // But can be concatenated
+  // But can be concatenated -- expected to pass
   initial p1: assert property (1[*0] ##1 x == 0);
+  initial p2: assert property (x == 0 ##1 1[*0]);
+
+  // But can be concatenated -- expected to fail
+  initial p3: assert property (1[*0] ##0 1);
+  initial p4: assert property (1 ##0 1[*0]);
 
 endmodule

regression/verilog/SVA/empty_sequence1.sv

@@ -109,6 +109,7 @@ sequence_matchest instantiate_sequence(
     {
       // now delay
       const auto from = numeric_cast_v<mp_integer>(sva_cycle_delay_expr.from());
+      DATA_INVARIANT(from >= 0, "##n must not be negative");
 
       auto t_rhs_from = lhs_match.end_time + from;
       mp_integer t_rhs_to;
@@ -128,6 +129,24 @@ sequence_matchest instantiate_sequence(
         t_rhs_to = t_rhs_from + to;
       }
 
+      // Implement 1800-2017 16.9.2.1
+      if(lhs_match.empty_match())
+      {
+        if(from == 0)
+        {
+          // (empty ##0 seq) does not result in a match.
+          continue;
+        }
+        else
+        {
+          // (empty ##n seq), where n is greater than 0,
+          // is equivalent to (##(n-1) seq).
+          t_rhs_from = t_rhs_from - 1;
+          if(t_rhs_to != no_timeframes)
+            t_rhs_to = t_rhs_to - 1;
+        }
+      }
+
       // Add a potential match for each timeframe in the range
       for(mp_integer t_rhs = t_rhs_from; t_rhs <= t_rhs_to; ++t_rhs)
       {