add word-level BMC encoding for SVA sequences

This adds a BMC encoding for SVA sequences by translating an SVA sequence
expression into a list of match point timeframe numbers and match
conditions.

Author: kroening

regression/ebmc/ring_buffer_bdd/ring_buffer.sv

@@ -19,8 +19,8 @@ module ring_buffer(input clk, input read, input write);
   wire full=count==15;
   wire empty=count==0;
 
-  assume property (empty |-> !read);
-  assume property (full |-> !write);
+  assume property (empty -> !read);
+  assume property (full -> !write);
 
   assert property (((writeptr-readptr)&'b1111)==count);
 

regression/ebmc/ring_buffer_induction/ring_buffer.sv

@@ -19,8 +19,8 @@ module ring_buffer(input clk, input read, input write);
   wire full=count==15;
   wire empty=count==0;
 
-  assume property (empty |-> !read);
-  assume property (full |-> !write);
+  assume property (empty -> !read);
+  assume property (full -> !write);
 
   assert property (((writeptr-readptr)&'b1111)==count);
 

regression/verilog/SVA/sequence_implication1.desc

@@ -1,10 +1,8 @@
-KNOWNBUG
+CORE
 sequence_implication1.sv
 --bound 20
 ^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-The sequence implication operator does not pick up the end of the chain
-sequence on the left hand side.

regression/verilog/SVA/sequence_implication1.sv

@@ -12,4 +12,7 @@ module main(input clk);
   // checks that 1 2 is followed by 0
   assert property (@(posedge clk) counter == 1 ##1 counter == 2 |-> ##1 counter == 0);
 
+  // same with non-overlapping implication
+  assert property (@(posedge clk) counter == 1 ##1 counter == 2 |=> counter == 0);
+
 endmodule : main

src/temporal-logic/normalize_property.cpp

@@ -61,20 +61,6 @@ exprt normalize_pre_implies(implies_exprt expr)
   return or_exprt{not_exprt{expr.lhs()}, expr.rhs()};
 }
 
-exprt normalize_pre_sva_overlapped_implication(
-  sva_overlapped_implication_exprt expr)
-{
-  // same as regular implication
-  return or_exprt{not_exprt{expr.lhs()}, expr.rhs()};
-}
-
-exprt normalize_pre_sva_non_overlapped_implication(
-  sva_non_overlapped_implication_exprt expr)
-{
-  // same as a->Xb
-  return or_exprt{not_exprt{expr.lhs()}, X_exprt{expr.rhs()}};
-}
-
 exprt normalize_pre_sva_cycle_delay(sva_cycle_delay_exprt expr)
 {
   if(expr.is_unbounded())
@@ -105,12 +91,6 @@ exprt normalize_property(exprt expr)
     expr = normalize_pre_implies(to_implies_expr(expr));
   else if(expr.id() == ID_sva_cover)
     expr = G_exprt{not_exprt{to_sva_cover_expr(expr).op()}};
-  else if(expr.id() == ID_sva_overlapped_implication)
-    expr = normalize_pre_sva_overlapped_implication(
-      to_sva_overlapped_implication_expr(expr));
-  else if(expr.id() == ID_sva_non_overlapped_implication)
-    expr = normalize_pre_sva_non_overlapped_implication(
-      to_sva_non_overlapped_implication_expr(expr));
   else if(expr.id() == ID_sva_nexttime)
   {
     if(!to_sva_nexttime_expr(expr).is_indexed())

src/temporal-logic/normalize_property.h

@@ -16,8 +16,6 @@ Author: Daniel Kroening, dkr@amazon.com
 /// ¬(a ∨ b) --> ¬a ∧ ¬b
 /// ¬(a ∧ b) --> ¬a ∨ ¬b
 /// (a -> b) --> ¬a ∨ b
-/// sva_overlapped_implication --> ¬a ∨ b
-/// sva_non_overlapped_implication --> ¬a ∨ Xb
 /// sva_nexttime φ --> Xφ
 /// sva_s_nexttime φ --> Xφ
 /// sva_if --> ? :

src/temporal-logic/temporal_logic.cpp

@@ -12,15 +12,14 @@ Author: Daniel Kroening, kroening@kroening.com
 
 bool is_temporal_operator(const exprt &expr)
 {
-  return is_CTL_operator(expr) || is_LTL_operator(expr) || expr.id() == ID_A ||
-         expr.id() == ID_E || expr.id() == ID_sva_always ||
-         expr.id() == ID_sva_always || expr.id() == ID_sva_ranged_always ||
-         expr.id() == ID_sva_nexttime || expr.id() == ID_sva_s_nexttime ||
-         expr.id() == ID_sva_non_overlapped_implication ||
-         expr.id() == ID_sva_until || expr.id() == ID_sva_s_until ||
-         expr.id() == ID_sva_until_with || expr.id() == ID_sva_s_until_with ||
-         expr.id() == ID_sva_eventually || expr.id() == ID_sva_s_eventually ||
-         expr.id() == ID_sva_cycle_delay ||
+  return is_CTL_operator(expr) || is_LTL_operator(expr) ||
+         is_SVA_sequence(expr) || expr.id() == ID_A || expr.id() == ID_E ||
+         expr.id() == ID_sva_always || expr.id() == ID_sva_always ||
+         expr.id() == ID_sva_ranged_always || expr.id() == ID_sva_nexttime ||
+         expr.id() == ID_sva_s_nexttime || expr.id() == ID_sva_until ||
+         expr.id() == ID_sva_s_until || expr.id() == ID_sva_until_with ||
+         expr.id() == ID_sva_s_until_with || expr.id() == ID_sva_eventually ||
+         expr.id() == ID_sva_s_eventually || expr.id() == ID_sva_cycle_delay ||
          expr.id() == ID_sva_overlapped_followed_by ||
          expr.id() == ID_sva_nonoverlapped_followed_by;
 }
@@ -66,3 +65,15 @@ bool is_LTL(const exprt &expr)
 
   return !has_subexpr(expr, non_LTL_operator);
 }
+
+bool is_SVA_sequence(const exprt &expr)
+{
+  auto id = expr.id();
+  // Note that ID_sva_overlapped_followed_by and ID_sva_nonoverlapped_followed_by
+  // are property expressions, not sequence expressions.
+  return id == ID_sva_overlapped_implication ||
+         id == ID_sva_non_overlapped_implication || id == ID_sva_cycle_delay ||
+         id == ID_sva_sequence_concatenation ||
+         id == ID_sva_sequence_intersect || id == ID_sva_sequence_first_match ||
+         id == ID_sva_sequence_throughout || id == ID_sva_sequence_within;
+}

src/temporal-logic/temporal_logic.h

@@ -36,4 +36,7 @@ bool is_LTL(const exprt &);
 /// as its root
 bool is_LTL_operator(const exprt &);
 
+/// Returns true iff the given expression is an SVA sequence expression
+bool is_SVA_sequence(const exprt &);
+
 #endif