SVA: sequence property expressions

SVA Sequences can be used as properties, in one of three ways:

1. weak(s)

2. strong(s)

3. s

The third form is interpreted as strong when used in a cover statement, and
as weak in assert/assume. The SVA not operator flips this around.

This adds a new expression, sva_sequence_property_exprt, to denote this
conversion.

Author: kroening

regression/verilog/SVA/sequence2.desc

@@ -2,7 +2,7 @@ CORE
 sequence2.sv
 --bound 10 --numbered-trace
 ^\[main\.p0] ##\[0:\$\] main\.x == 10: REFUTED$
-^Counterexample with 7 states:$
+^Counterexample with \d+ states:$
 ^main\.x@0 = 0$
 ^main\.x@1 = 1$
 ^main\.x@2 = 2$

src/hw_cbmc_irep_ids.h

@@ -63,6 +63,7 @@ IREP_ID_ONE(sva_sequence_first_match)
 IREP_ID_ONE(sva_sequence_goto_repetition)
 IREP_ID_ONE(sva_sequence_intersect)
 IREP_ID_ONE(sva_sequence_non_consecutive_repetition)
+IREP_ID_ONE(sva_sequence_property)
 IREP_ID_ONE(sva_sequence_repetition_star)
 IREP_ID_ONE(sva_sequence_repetition_plus)
 IREP_ID_ONE(sva_sequence_throughout)

src/temporal-logic/trivial_sva.cpp

@@ -107,12 +107,12 @@ exprt trivial_sva(exprt expr)
     op = trivial_sva(op);
 
   // post-traversal
-  if(expr.id() == ID_typecast)
+  if(expr.id() == ID_sva_sequence_property)
   {
-    // We typecast sequences to bool, and hence can drop
-    // casts from bool to bool
-    auto &op = to_typecast_expr(expr).op();
-    if(expr.type().id() == ID_bool && op.type().id() == ID_bool)
+    // We simplify sequences to boolean expressions, and hence can drop
+    // the sva_sequence_property converter
+    auto &op = to_sva_sequence_property_expr(expr).op();
+    if(op.type().id() == ID_bool)
       return op;
   }
 

src/trans-word-level/instantiate_word_level.cpp

@@ -140,6 +140,24 @@ wl_instantiatet::instantiate_rec(exprt expr, const mp_integer &t) const
 
     return {max, disjunction(disjuncts)};
   }
+  else if(expr.id() == ID_sva_sequence_property)
+  {
+    // sequence expressions -- these may have multiple potential
+    // match points, and evaluate to true if any of them matches
+    auto &sequence = to_sva_sequence_property_expr(expr);
+    const auto matches = instantiate_sequence(sequence, t, no_timeframes);
+    exprt::operandst disjuncts;
+    disjuncts.reserve(matches.size());
+    mp_integer max = t;
+
+    for(auto &match : matches)
+    {
+      disjuncts.push_back(match.condition);
+      max = std::max(max, match.end_time);
+    }
+
+    return {max, disjunction(disjuncts)};
+  }
   else if(expr.id() == ID_verilog_past)
   {
     auto &verilog_past = to_verilog_past_expr(expr);

src/trans-word-level/property.cpp

@@ -507,6 +507,25 @@ static obligationst property_obligations_rec(
       std::max(obligations_true.first, obligations_false.first),
       if_exprt{cond, obligations_true.second, obligations_false.second}};
   }
+  else if(property_expr.id() == ID_sva_sequence_property)
+  {
+    // Sequences can be used as property, and evaluate to true
+    // when there is at least one match.
+    auto &sequence = to_sva_sequence_property_expr(property_expr).op();
+    auto matches = instantiate_sequence(sequence, current, no_timeframes);
+
+    exprt::operandst disjuncts;
+    disjuncts.reserve(matches.size());
+    mp_integer max = current;
+
+    for(auto &match : matches)
+    {
+      disjuncts.push_back(match.condition);
+      max = std::max(max, match.end_time);
+    }
+
+    return obligationst{max, disjunction(disjuncts)};
+  }
   else if(
     property_expr.id() == ID_typecast &&
     to_typecast_expr(property_expr).op().type().id() == ID_bool)

src/verilog/expr2verilog.cpp

@@ -530,18 +530,25 @@ expr2verilogt::resultt expr2verilogt::convert_sva_unary(
   const std::string &name,
   const unary_exprt &src)
 {
-  auto op = convert_rec(src.op());
+  auto &op = src.op();
+
+  std::size_t op_operands = 0;
+
+  if(op.id() == ID_typecast)
+    op_operands = to_typecast_expr(op).op().operands().size();
+  else if(src.op().id() == ID_sva_sequence_property)
+    op_operands = to_sva_sequence_property_expr(op).op().operands().size();
+  else
+    op_operands = op.operands().size();
 
-  auto op_skip_typecast =
-    src.op().id() == ID_typecast ? to_typecast_expr(src.op()).op() : src.op();
+  auto op_rec = convert_rec(op);
 
-  if(
-    op.p == verilog_precedencet::MIN && op_skip_typecast.operands().size() >= 2)
+  if(op_rec.p == verilog_precedencet::MIN && op_operands >= 2)
   {
-    op.s = "(" + op.s + ")";
+    op_rec.s = "(" + op_rec.s + ")";
   }
 
-  return {verilog_precedencet::MIN, name + " " + op.s};
+  return {verilog_precedencet::MIN, name + " " + op_rec.s};
 }
 
 /*******************************************************************\
@@ -1808,6 +1815,9 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src)
   else if(src.id() == ID_sva_weak)
     return convert_function("weak", src);
 
+  else if(src.id() == ID_sva_sequence_property)
+    return convert_rec(to_sva_sequence_property_expr(src).op());
+
   else if(src.id()==ID_sva_sequence_concatenation)
     return convert_sva_sequence_concatenation(
       to_binary_expr(src), precedence = verilog_precedencet::MIN);

src/verilog/sva_expr.h

@@ -1515,4 +1515,31 @@ to_sva_sequence_first_match_expr(exprt &expr)
   return static_cast<sva_sequence_first_match_exprt &>(expr);
 }
 
+/// 1800-2017 16.12.2 Sequence property
+/// Equivalent to weak(...) or strong(...) depending on context.
+class sva_sequence_property_exprt : public unary_predicate_exprt
+{
+public:
+  explicit sva_sequence_property_exprt(exprt op)
+    : unary_predicate_exprt(ID_sva_sequence_property, std::move(op))
+  {
+  }
+};
+
+static inline const sva_sequence_property_exprt &
+to_sva_sequence_property_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_sva_sequence_property);
+  sva_sequence_property_exprt::check(expr, validation_modet::INVARIANT);
+  return static_cast<const sva_sequence_property_exprt &>(expr);
+}
+
+static inline sva_sequence_property_exprt &
+to_sva_sequence_property_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_sva_sequence_property);
+  sva_sequence_property_exprt::check(expr, validation_modet::INVARIANT);
+  return static_cast<sva_sequence_property_exprt &>(expr);
+}
+
 #endif

src/verilog/verilog_typecheck.cpp

@@ -1785,7 +1785,7 @@ void verilog_typecheckt::convert_property_declaration(
   auto full_identifier = hierarchical_identifier(base_name);
 
   convert_sva(declaration.cond());
-  make_boolean(declaration.cond());
+  require_sva_property(declaration.cond());
 
   auto type = bool_typet{};
   type.set(ID_C_verilog_type, ID_verilog_property_declaration);

src/verilog/verilog_typecheck_sva.cpp

@@ -52,8 +52,11 @@ void verilog_typecheck_exprt::require_sva_property(exprt &expr)
 
   if(type.id() == ID_verilog_sva_sequence)
   {
-    // cast to boolean
-    make_boolean(expr);
+    // 1800 2017 16.12.2 Sequence property
+    // These yield an implicit weak(...) or strong(...), but we
+    // only know which one once the sequence is used in an assert/assume
+    // or cover.
+    expr = sva_sequence_property_exprt{std::move(expr)};
   }
   else if(
     type.id() == ID_bool || type.id() == ID_unsignedbv ||