SVA: add eight sequence operators to Verilog Frontend

regression/verilog/SVA/sequence_first_match1.desc

@@ -1,8 +1,8 @@
 CORE
 sequence_first_match1.sv
 
-^file .* line \d+: no support for 'first_match'$
-^EXIT=2$
+^\[.*\] first_match\(main\.x == 0\): FAILURE: property not supported by BMC engine$
+^EXIT=10$
 ^SIGNAL=0$
 --
 ^warning: ignoring

regression/verilog/SVA/sequence_intersect1.desc

@@ -1,8 +1,8 @@
 CORE
 sequence_intersect1.sv
 
-^file .* line \d+: no support for 'intersect'$
-^EXIT=2$
+^\[.*\] main\.x == 0 intersect main\.x == 1: FAILURE: property not supported by BMC engine$
+^EXIT=10$
 ^SIGNAL=0$
 --
 ^warning: ignoring

regression/verilog/SVA/sequence_repetition1.desc

@@ -1,6 +1,12 @@
-KNOWNBUG
+CORE
 sequence_repetition1.sv
 --bound 10
+^\[.*\] 1 \[\*\] main\.half_x == 0: FAILURE: property not supported by BMC engine$
+^\[.*\] 1 \[->\] main\.half_x == 0: FAILURE: property not supported by BMC engine$
+^\[.*\] 1 \[=\] main\.half_x == 0: FAILURE: property not supported by BMC engine$
+^\[.*\] 1 \[\*\] main\.x == 0: FAILURE: property not supported by BMC engine$
+^\[.*\] 1 \[->\] main\.x == 0: FAILURE: property not supported by BMC engine$
+^\[.*\] 1 \[=\] main\.x == 0: FAILURE: property not supported by BMC engine$
 ^EXIT=10$
 ^SIGNAL=0$
 --

regression/verilog/SVA/sequence_repetition2.desc

@@ -0,0 +1,15 @@
+CORE
+sequence_repetition2.sv
+--bound 10
+^\[main\.p0\] main\.x == 0\[\*\]: FAILURE: property not supported by BMC engine$
+^\[main\.p1\] main\.x == 1\[\*\]: FAILURE: property not supported by BMC engine$
+^\[main\.p2\] \(main\.x == 0\[\+\]\) #-# main\.x == 1: FAILURE: property not supported by BMC engine$
+^\[main\.p3\] main\.x == 0\[\+\]: FAILURE: property not supported by BMC engine$
+^\[main\.p4\] main\.half_x == 0\[\*\]: FAILURE: property not supported by BMC engine$
+^\[main\.p5\] main\.x == 1\[\+\]: FAILURE: property not supported by BMC engine$
+^\[main\.p6\] \(main\.x == 0\[\+\]\) #=# main\.x == 1: FAILURE: property not supported by BMC engine$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/SVA/sequence_repetition2.sv

@@ -0,0 +1,23 @@
+module main(input clk);
+
+  reg [31:0] x = 0;
+
+  // 0 1 2 3 4 ...
+  always_ff @(posedge clk)
+    x<=x+1;
+
+  // 0 0 1 1 2 2 3 3 ...
+  wire [31:0] half_x = x/2;
+
+  // 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[*]);
+
+  // should fail
+  initial p5: assert property (x==1[+]);
+  initial p6: assert property (x==0[+] #=# x==1);
+
+endmodule

regression/verilog/SVA/sequence_throughout1.desc

@@ -1,8 +1,8 @@
 CORE
 sequence_throughout1.sv
 
-^file .* line \d+: no support for 'throughout'$
-^EXIT=2$
+^\[.*\] main\.x == 0 throughout main\.x == 1: FAILURE: property not supported by BMC engine$
+^EXIT=10$
 ^SIGNAL=0$
 --
 ^warning: ignoring

regression/verilog/SVA/sequence_within1.desc

@@ -1,8 +1,8 @@
 CORE
 sequence_within1.sv
 
-^file .* line \d+: no support for 'within'$
-^EXIT=2$
+^\[.*\] main\.x == 0 within main\.x == 1: FAILURE: property not supported by BMC engine$
+^EXIT=10$
 ^SIGNAL=0$
 --
 ^warning: ignoring

src/temporal-logic/temporal_logic.cpp

@@ -74,7 +74,12 @@ bool is_SVA_sequence(const exprt &expr)
          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;
+         id == ID_sva_sequence_throughout || id == ID_sva_sequence_within ||
+         id == ID_sva_sequence_goto_repetition ||
+         id == ID_sva_sequence_consecutive_repetition ||
+         id == ID_sva_sequence_non_consecutive_repetition ||
+         id == ID_sva_sequence_repetition_star ||
+         id == ID_sva_sequence_repetition_plus;
 }
 
 bool is_SVA_operator(const exprt &expr)

src/trans-word-level/property.cpp

@@ -110,6 +110,42 @@ Function: bmc_supports_SVA_property
 
 bool bmc_supports_SVA_property(const exprt &expr)
 {
+  // sva_sequence_first_match is not supported yet
+  if(has_subexpr(expr, ID_sva_sequence_first_match))
+    return false;
+
+  // sva_sequence_troughout is not supported yet
+  if(has_subexpr(expr, ID_sva_sequence_throughout))
+    return false;
+
+  // sva_sequence_intersect is not supported yet
+  if(has_subexpr(expr, ID_sva_sequence_intersect))
+    return false;
+
+  // sva_sequence_within is not supported yet
+  if(has_subexpr(expr, ID_sva_sequence_within))
+    return false;
+
+  // sva_sequence_repetition_plus is not supported yet
+  if(has_subexpr(expr, ID_sva_sequence_repetition_plus))
+    return false;
+
+  // sva_sequence_repetition_star is not supported yet
+  if(has_subexpr(expr, ID_sva_sequence_repetition_star))
+    return false;
+
+  // sva_sequence_non_consecutive_repetition is not supported yet
+  if(has_subexpr(expr, ID_sva_sequence_non_consecutive_repetition))
+    return false;
+
+  // sva_sequence_consecutive_repetition is not supported yet
+  if(has_subexpr(expr, ID_sva_sequence_consecutive_repetition))
+    return false;
+
+  // sva_sequence_goto_repetition is not supported yet
+  if(has_subexpr(expr, ID_sva_sequence_goto_repetition))
+    return false;
+
   return true;
 }
 

src/verilog/expr2verilog.cpp

@@ -453,6 +453,28 @@ expr2verilogt::resultt expr2verilogt::convert_sva_unary(
 
 /*******************************************************************\
 
+Function: expr2verilogt::convert_sva_unary
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+expr2verilogt::resultt expr2verilogt::convert_sva_unary(
+  const unary_exprt &src,
+  const std::string &name)
+{
+  auto op = convert_rec(src.op());
+  if(op.p == verilog_precedencet::MIN && src.op().operands().size() >= 2)
+    op.s = "(" + op.s + ")";
+  return {verilog_precedencet::MIN, op.s + name};
+}
+
+/*******************************************************************\
+
 Function: expr2verilogt::convert_sva_binary
 
   Inputs:
@@ -1446,6 +1468,16 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src)
            convert_sva_binary("intersect", to_binary_expr(src));
   // not sure about precedence
 
+  else if(src.id() == ID_sva_sequence_throughout)
+    return precedence = verilog_precedencet::MIN,
+           convert_sva_binary("throughout", to_binary_expr(src));
+  // not sure about precedence
+
+  else if(src.id() == ID_sva_sequence_within)
+    return precedence = verilog_precedencet::MIN,
+           convert_sva_binary("within", to_binary_expr(src));
+  // not sure about precedence
+
   else if(src.id() == ID_sva_sequence_within)
     return convert_sva_sequence_concatenation(
       to_binary_expr(src), precedence = verilog_precedencet::MIN);
@@ -1460,6 +1492,31 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src)
     return precedence = verilog_precedencet::MIN,
            convert_sva_unary("always", to_sva_always_expr(src));
 
+  else if(src.id() == ID_sva_sequence_repetition_star)
+    return precedence = verilog_precedencet::MIN,
+           convert_sva_unary(to_unary_expr(src), "[*]");
+  // not sure about precedence
+
+  else if(src.id() == ID_sva_sequence_repetition_plus)
+    return precedence = verilog_precedencet::MIN,
+           convert_sva_unary(to_unary_expr(src), "[+]");
+  // not sure about precedence
+
+  else if(src.id() == ID_sva_sequence_non_consecutive_repetition)
+    return precedence = verilog_precedencet::MIN,
+           convert_sva_binary("[=]", to_binary_expr(src));
+  // not sure about precedence
+
+  else if(src.id() == ID_sva_sequence_consecutive_repetition)
+    return precedence = verilog_precedencet::MIN,
+           convert_sva_binary("[*]", to_binary_expr(src));
+  // not sure about precedence
+
+  else if(src.id() == ID_sva_sequence_goto_repetition)
+    return precedence = verilog_precedencet::MIN,
+           convert_sva_binary("[->]", to_binary_expr(src));
+  // not sure about precedence
+
   else if(src.id() == ID_sva_ranged_always)
   {
     return precedence = verilog_precedencet::MIN,

src/verilog/expr2verilog_class.h

@@ -120,6 +120,8 @@ class expr2verilogt
 
   resultt convert_sva_unary(const std::string &name, const unary_exprt &);
 
+  resultt convert_sva_unary(const unary_exprt &, const std::string &name);
+
   resultt convert_sva_binary(const std::string &name, const binary_exprt &);
 
   resultt convert_sva_abort(const std::string &name, const sva_abort_exprt &);

src/verilog/verilog_typecheck_expr.cpp

@@ -2465,27 +2465,15 @@ exprt verilog_typecheck_exprt::convert_unary_expr(unary_exprt expr)
     expr.id() == ID_sva_cycle_delay_plus ||
     expr.id() == ID_sva_cycle_delay_star || expr.id() == ID_sva_weak ||
     expr.id() == ID_sva_strong || expr.id() == ID_sva_nexttime ||
-    expr.id() == ID_sva_s_nexttime)
+    expr.id() == ID_sva_s_nexttime ||
+    expr.id() == ID_sva_sequence_first_match ||
+    expr.id() == ID_sva_sequence_repetition_plus ||
+    expr.id() == ID_sva_sequence_repetition_star)
   {
     convert_expr(expr.op());
     make_boolean(expr.op());
     expr.type()=bool_typet();
   }
-  else if(expr.id() == ID_sva_sequence_first_match)
-  {
-    throw errort().with_location(expr.source_location())
-      << "no support for 'first_match'";
-  }
-  else if(expr.id() == ID_sva_sequence_repetition_plus)
-  {
-    throw errort().with_location(expr.source_location())
-      << "currently no support for [+]";
-  }
-  else if(expr.id() == ID_sva_sequence_repetition_star)
-  {
-    throw errort().with_location(expr.source_location())
-      << "currently no support for [*]";
-  }
   else if(expr.id() == ID_verilog_explicit_cast)
   {
     // SystemVerilog has got type'(expr). This is an explicit
@@ -2959,20 +2947,24 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr)
 
     return std::move(expr);
   }
-  else if(expr.id() == ID_sva_sequence_intersect)
-  {
-    throw errort().with_location(expr.source_location())
-      << "no support for 'intersect'";
-  }
-  else if(expr.id() == ID_sva_sequence_throughout)
-  {
-    throw errort().with_location(expr.source_location())
-      << "no support for 'throughout'";
-  }
-  else if(expr.id() == ID_sva_sequence_within)
+  else if(
+    expr.id() == ID_sva_sequence_intersect ||
+    expr.id() == ID_sva_sequence_throughout ||
+    expr.id() == ID_sva_sequence_within ||
+    expr.id() == ID_sva_sequence_non_consecutive_repetition ||
+    expr.id() == ID_sva_sequence_consecutive_repetition ||
+    expr.id() == ID_sva_sequence_goto_repetition)
   {
-    throw errort().with_location(expr.source_location())
-      << "no support for 'within'";
+    auto &binary_expr = to_binary_expr(expr);
+
+    convert_expr(binary_expr.lhs());
+    make_boolean(binary_expr.lhs());
+    convert_expr(binary_expr.rhs());
+    make_boolean(binary_expr.rhs());
+
+    expr.type() = bool_typet();
+
+    return std::move(expr);
   }
   else if(expr.id()==ID_hierarchical_identifier)
   {
@@ -3026,21 +3018,6 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr)
     expr.type() = bool_typet();
     return std::move(expr);
   }
-  else if(expr.id() == ID_sva_sequence_non_consecutive_repetition)
-  {
-    throw errort().with_location(expr.source_location())
-      << "currently no support for [=]";
-  }
-  else if(expr.id() == ID_sva_sequence_consecutive_repetition)
-  {
-    throw errort().with_location(expr.source_location())
-      << "currently no support for [*]";
-  }
-  else if(expr.id() == ID_sva_sequence_goto_repetition)
-  {
-    throw errort().with_location(expr.source_location())
-      << "currently no support for [->]";
-  }
   else
   {
     // type is guessed for now