Merge pull request #1028 from diffblue/sequence_first_match2

SVA: `first_match`

Author: kroening

CHANGELOG

@@ -3,6 +3,7 @@
 * SystemVerilog: typedefs from package scopes
 * SystemVerilog: assignment patterns with keys for structs
 * SystemVerilog: unbased unsigned literals '0, '1, 'x, 'z
+* SystemVerilog: first_match
 * Verilog: 'dx, 'dz
 * SMV: LTL V operator, xnor operator
 * SMV: word types and operators

regression/verilog/SVA/sequence_first_match1.desc

@@ -1,8 +1,9 @@
 CORE
 sequence_first_match1.sv
 --bound 5
-^\[.*\] first_match\(main\.x == 0\): FAILURE: property not supported by BMC engine$
-^EXIT=10$
+^\[.*\] first_match\(main\.x == 0\): PROVED up to bound 5$
+^\[.*\] first_match\(main\.x == 0, main\.x\+\+\): PROVED up to bound 5$
+^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring

regression/verilog/SVA/sequence_first_match2.desc

@@ -0,0 +1,12 @@
+CORE
+sequence_first_match2.sv
+--bound 5
+^\[.*\] \(##1 1\) or \(\(##2 1\) \|-> main.x == 1\): PROVED up to bound 5$
+^\[.*\] first_match\(\(##1 1\) or \(##2 1\)\) \|-> main\.x == 1: PROVED up to bound 5$
+^\[.*\] 1 or \(\(##1 1\) \|-> main\.x == 0\): PROVED up to bound 5$
+^\[.*\] first_match\(1 or \(##1 1\)\) \|-> main\.x == 0: PROVED up to bound 5$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/SVA/sequence_first_match2.sv

@@ -0,0 +1,23 @@
+module main(input clk);
+
+  reg [31:0] x = 0;
+
+  always @(posedge clk)
+    x<=x+1;
+
+  // Starting from a particular state,
+  // first_match yields the sequence that _ends_ first.
+
+  // fails
+  initial p0: assert property ((##1 1) or (##2 1) |-> x==1);
+
+  // passes
+  initial p1: assert property (first_match((##1 1) or (##2 1)) |-> x==1);
+
+  // fails
+  initial p2: assert property (1 or ##1 1 |-> x==0);
+
+  // passes
+  initial p3: assert property (first_match(1 or ##1 1) |-> x==0);
+
+endmodule

src/trans-word-level/property.cpp

@@ -111,10 +111,6 @@ 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_within is not supported yet
   if(has_subexpr(expr, ID_sva_sequence_within))
     return false;

src/trans-word-level/sequence.cpp

@@ -158,7 +158,36 @@ std::vector<std::pair<mp_integer, exprt>> instantiate_sequence(
   }
   else if(expr.id() == ID_sva_sequence_first_match)
   {
-    PRECONDITION(false);
+    auto &first_match = to_sva_sequence_first_match_expr(expr);
+
+    const auto lhs_match_points =
+      instantiate_sequence(first_match.lhs(), t, no_timeframes);
+
+    // the match of seq with the earliest ending clock tick is a
+    // match of first_match (seq)
+    std::optional<mp_integer> earliest;
+
+    for(auto &match : lhs_match_points)
+    {
+      if(!earliest.has_value() || earliest.value() > match.first)
+        earliest = match.first;
+    }
+
+    if(!earliest.has_value())
+      return {}; // no match
+
+    std::vector<std::pair<mp_integer, exprt>> result;
+
+    for(auto &match : lhs_match_points)
+    {
+      // Earliest?
+      if(match.first == earliest.value())
+      {
+        result.push_back(match);
+      }
+    }
+
+    return result;
   }
   else if(expr.id() == ID_sva_sequence_throughout)
   {

src/verilog/expr2verilog.cpp

@@ -215,6 +215,36 @@ expr2verilogt::resultt expr2verilogt::convert_sva_sequence_concatenation(
 
 /*******************************************************************\
 
+Function: expr2verilogt::convert_sva_sequence_first_match
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+expr2verilogt::resultt expr2verilogt::convert_sva_sequence_first_match(
+  const sva_sequence_first_match_exprt &src)
+{
+  std::string dest = "first_match(";
+
+  dest += convert_rec(src.lhs()).s;
+
+  if(src.rhs().is_not_nil())
+  {
+    dest += ", ";
+    dest += convert_rec(src.rhs()).s;
+  }
+
+  dest += ')';
+
+  return {verilog_precedencet::MAX, dest};
+}
+
+/*******************************************************************\
+
 Function: expr2verilogt::convert_binary
 
   Inputs:
@@ -1782,7 +1812,8 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src)
     // not sure about precedence
 
   else if(src.id() == ID_sva_sequence_first_match)
-    return convert_function("first_match", src);
+    return convert_sva_sequence_first_match(
+      to_sva_sequence_first_match_expr(src));
 
   else if(src.id() == ID_sva_sequence_intersect)
     return precedence = verilog_precedencet::MIN,
@@ -1956,6 +1987,9 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src)
   else if(src.id() == ID_verilog_value_range)
     return convert_value_range(to_verilog_value_range_expr(src));
 
+  else if(src.id() == ID_postincrement)
+    return convert_sva_unary(to_unary_expr(src), "++");
+
   else if(
     src.id() == ID_nand || src.id() == ID_nor || src.id() == ID_xnor ||
     src.id() == ID_xor)

src/verilog/expr2verilog_class.h

@@ -17,6 +17,7 @@ class sva_case_exprt;
 class sva_if_exprt;
 class sva_ranged_predicate_exprt;
 class sva_sequence_consecutive_repetition_exprt;
+class sva_sequence_first_match_exprt;
 
 // Precedences (higher means binds more strongly).
 // Follows Table 11-2 in IEEE 1800-2017.
@@ -160,6 +161,9 @@ class expr2verilogt
   resultt
   convert_sva_sequence_concatenation(const binary_exprt &, verilog_precedencet);
 
+  resultt
+  convert_sva_sequence_first_match(const sva_sequence_first_match_exprt &);
+
   resultt convert_function_call(const class function_call_exprt &);
 
   resultt convert_non_indexed_part_select(

src/verilog/parser.y

@@ -2621,7 +2621,7 @@ sequence_expr_proper:
 	| sequence_expr "or" sequence_expr
 		{ init($$, ID_sva_or); mto($$, $1); mto($$, $3); }
         | "first_match" '(' sequence_expr ')'
-                { init($$, ID_sva_sequence_first_match); mto($$, $3); }
+                { init($$, ID_sva_sequence_first_match); mto($$, $3); stack_expr($$).add_to_operands(nil_exprt{}); }
         | "first_match" '(' sequence_expr ',' sequence_match_item_brace ')'
                 { init($$, ID_sva_sequence_first_match); mto($$, $3); mto($$, $5); }
         | expression_or_dist "throughout" sequence_expr

src/verilog/sva_expr.h

@@ -1332,4 +1332,38 @@ to_sva_sequence_throughout_expr(exprt &expr)
   return static_cast<sva_sequence_throughout_exprt &>(expr);
 }
 
+class sva_sequence_first_match_exprt : public binary_exprt
+{
+public:
+  // the second operand is optional
+  explicit sva_sequence_first_match_exprt(exprt op)
+    : binary_exprt(std::move(op), ID_sva_sequence_first_match, nil_exprt{})
+  {
+  }
+
+  sva_sequence_first_match_exprt(exprt op, exprt action)
+    : binary_exprt(
+        std::move(op),
+        ID_sva_sequence_first_match,
+        std::move(action))
+  {
+  }
+};
+
+static inline const sva_sequence_first_match_exprt &
+to_sva_sequence_first_match_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_sva_sequence_first_match);
+  sva_sequence_first_match_exprt::check(expr, validation_modet::INVARIANT);
+  return static_cast<const sva_sequence_first_match_exprt &>(expr);
+}
+
+static inline sva_sequence_first_match_exprt &
+to_sva_sequence_first_match_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_sva_sequence_first_match);
+  sva_sequence_first_match_exprt::check(expr, validation_modet::INVARIANT);
+  return static_cast<sva_sequence_first_match_exprt &>(expr);
+}
+
 #endif