introduce sva_boolean_exprt

IEEE 1800-2017 16.6 Boolean expressions introduces rules on how to convert
Boolean expressions into SVA sequences or properties.  This introduces an
expression for this conversion.

Author: kroening

src/hw_cbmc_irep_ids.h

@@ -45,6 +45,7 @@ IREP_ID_ONE(smv_EBG)
 IREP_ID_ONE(smv_ABG)
 IREP_ID_ONE(smv_ABU)
 IREP_ID_ONE(smv_EBU)
+IREP_ID_ONE(sva_boolean)
 IREP_ID_ONE(sva_accept_on)
 IREP_ID_ONE(sva_reject_on)
 IREP_ID_ONE(sva_sync_accept_on)

src/temporal-logic/normalize_property.cpp

@@ -23,12 +23,13 @@ Author: Daniel Kroening, [email protected]
 exprt normalize_pre_sva_non_overlapped_implication(
   sva_non_overlapped_implication_exprt expr)
 {
-  // Same as a->always[1:1] b if lhs is not a sequence.
-  if(!is_SVA_sequence_operator(expr.lhs()))
+  // Same as a->always[1:1] b if lhs is not a proper sequence.
+  if(expr.lhs().id() == ID_sva_boolean)
   {
+    const auto &lhs_cond = to_sva_boolean_expr(expr.lhs()).op();
     auto one = natural_typet{}.one_expr();
     return or_exprt{
-      not_exprt{expr.lhs()}, sva_ranged_always_exprt{one, one, expr.rhs()}};
+      not_exprt{lhs_cond}, sva_ranged_always_exprt{one, one, expr.rhs()}};
   }
   else
     return std::move(expr);

src/temporal-logic/temporal_logic.cpp

@@ -105,9 +105,9 @@ bool is_SVA_sequence_operator(const exprt &expr)
   // ID_sva_non_overlapped_implication and ID_sva_overlapped_implication
   // are property expressions, not sequence expressions.
   // Note that ID_sva_not does not yield a sequence expression.
-  return id == ID_sva_and || id == ID_sva_or || id == ID_sva_cycle_delay ||
-         id == ID_sva_cycle_delay_plus || id == ID_sva_cycle_delay_star ||
-         id == ID_sva_sequence_concatenation ||
+  return id == ID_sva_boolean || id == ID_sva_and || id == ID_sva_or ||
+         id == ID_sva_cycle_delay || id == ID_sva_cycle_delay_plus ||
+         id == ID_sva_cycle_delay_star || 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_goto_repetition ||
@@ -120,7 +120,9 @@ bool is_SVA_sequence_operator(const exprt &expr)
 bool is_SVA_operator(const exprt &expr)
 {
   auto id = expr.id();
-  return is_SVA_sequence_operator(expr) || id == ID_sva_disable_iff ||
+  return is_SVA_sequence_operator(expr) || id == ID_sva_implies ||
+         id == ID_sva_iff || id == ID_sva_not || id == ID_sva_case ||
+         id == ID_sva_if || id == ID_sva_disable_iff ||
          id == ID_sva_accept_on || id == ID_sva_reject_on ||
          id == ID_sva_sync_accept_on || id == ID_sva_sync_reject_on ||
          id == ID_sva_always || id == ID_sva_s_always ||
@@ -245,10 +247,11 @@ struct ltl_sequence_matcht
 
 std::vector<ltl_sequence_matcht> LTL_sequence_matches(const exprt &sequence)
 {
-  if(!is_SVA_sequence_operator(sequence))
+  if(sequence.id() == ID_sva_boolean)
   {
     // atomic proposition
-    return {{sequence, 1}};
+    auto &p = to_sva_boolean_expr(sequence).op();
+    return {{p, 1}};
   }
   else if(sequence.id() == ID_sva_sequence_concatenation)
   {

src/trans-word-level/sequence.cpp

@@ -411,10 +411,19 @@ sequence_matchest instantiate_sequence(
 
     return result;
   }
-  else
+  else if(expr.id() == ID_sva_boolean)
   {
-    // not a sequence, evaluate as state predicate
-    auto instantiated = instantiate_property(expr, t, no_timeframes);
+    // a state predicate
+    auto &predicate = to_sva_boolean_expr(expr).op();
+    auto instantiated = instantiate_property(predicate, t, no_timeframes);
     return {{instantiated.first, instantiated.second}};
   }
+  else
+  {
+    DATA_CHECK_WITH_DIAGNOSTICS(
+      validation_modet::INVARIANT,
+      false,
+      "unexpected sequence expression",
+      expr.pretty());
+  }
 }

src/verilog/expr2verilog.cpp

@@ -1810,6 +1810,12 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src)
     return convert_rec(to_sva_sequence_property_expr_base(src).sequence());
   }
 
+  else if(src.id() == ID_sva_boolean)
+  {
+    // These are invisible
+    return convert_rec(to_sva_boolean_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

@@ -13,6 +13,29 @@ Author: Daniel Kroening, [email protected]
 
 #include "verilog_types.h"
 
+/// 1800-2017 16.6 Boolean expressions
+/// Conversion of a Boolean expression into a sequence or property
+class sva_boolean_exprt : public unary_exprt
+{
+public:
+  sva_boolean_exprt(exprt condition, typet __type)
+    : unary_exprt(ID_sva_boolean, std::move(condition), std::move(__type))
+  {
+  }
+};
+
+static inline const sva_boolean_exprt &to_sva_boolean_expr(const exprt &expr)
+{
+  sva_boolean_exprt::check(expr, validation_modet::INVARIANT);
+  return static_cast<const sva_boolean_exprt &>(expr);
+}
+
+static inline sva_boolean_exprt &to_sva_boolean_expr(exprt &expr)
+{
+  sva_boolean_exprt::check(expr, validation_modet::INVARIANT);
+  return static_cast<sva_boolean_exprt &>(expr);
+}
+
 /// accept_on, reject_on, sync_accept_on, sync_reject_on, disable_iff
 class sva_abort_exprt : public binary_predicate_exprt
 {

src/verilog/verilog_typecheck_sva.cpp

@@ -35,8 +35,9 @@ void verilog_typecheck_exprt::require_sva_sequence(exprt &expr)
     }
     else
     {
-      // state formula, can cast to sequence
+      // state formula, can convert to sequence
       make_boolean(expr);
+      expr = sva_boolean_exprt{std::move(expr), verilog_sva_sequence_typet{}};
     }
   }
   else
@@ -86,10 +87,8 @@ exprt verilog_typecheck_exprt::convert_unary_sva(unary_exprt expr)
     return std::move(expr);
   }
   else if(
-    expr.id() == ID_sva_cycle_delay_plus ||         // ##[+]
-    expr.id() == ID_sva_cycle_delay_star ||         // ##[*]
-    expr.id() == ID_sva_sequence_repetition_plus || // x[+]
-    expr.id() == ID_sva_sequence_repetition_star)   // x[*}
+    expr.id() == ID_sva_cycle_delay_plus || // ##[+]
+    expr.id() == ID_sva_cycle_delay_star)   // ##[*]
   {
     // These take a sequence as argument.
     // For some, the grammar allows properties to implement and/or over
@@ -99,6 +98,16 @@ exprt verilog_typecheck_exprt::convert_unary_sva(unary_exprt expr)
     expr.type() = verilog_sva_sequence_typet{};
     return std::move(expr);
   }
+  else if(
+    expr.id() == ID_sva_sequence_repetition_plus || // x[+]
+    expr.id() == ID_sva_sequence_repetition_star)   // x[*]
+  {
+    // These take a Boolean as argument, and yield a sequence.
+    convert_expr(expr.op());
+    make_boolean(expr.op());
+    expr.type() = verilog_sva_sequence_typet{};
+    return std::move(expr);
+  }
   else if(expr.id() == ID_sva_weak || expr.id() == ID_sva_strong)
   {
     convert_sva(expr.op());
@@ -109,7 +118,11 @@ exprt verilog_typecheck_exprt::convert_unary_sva(unary_exprt expr)
   else
   {
     // not SVA
-    return convert_expr_rec(std::move(expr));
+    DATA_CHECK_WITH_DIAGNOSTICS(
+      validation_modet::INVARIANT,
+      false,
+      "unexpected unary SVA expression",
+      expr.pretty());
   }
 }
 
@@ -123,14 +136,12 @@ exprt verilog_typecheck_exprt::convert_binary_sva(binary_exprt expr)
     // These yield sequences when both operands are sequences, and
     // properties otherwise.
     if(
-      (expr.lhs().type().id() == ID_verilog_sva_sequence ||
-       !has_temporal_operator(expr.lhs())) &&
-      (expr.rhs().type().id() == ID_verilog_sva_sequence ||
-       !has_temporal_operator(expr.rhs())))
+      expr.lhs().type().id() == ID_verilog_sva_sequence &&
+      expr.rhs().type().id() == ID_verilog_sva_sequence)
     {
-      expr.type() = verilog_sva_sequence_typet{};
       require_sva_sequence(expr.lhs());
       require_sva_sequence(expr.rhs());
+      expr.type() = verilog_sva_sequence_typet{};
     }
     else
     {
@@ -294,8 +305,12 @@ exprt verilog_typecheck_exprt::convert_binary_sva(binary_exprt expr)
   }
   else
   {
-    // not SVA
-    return convert_expr_rec(std::move(expr));
+    // unexpected SVA expression
+    DATA_CHECK_WITH_DIAGNOSTICS(
+      validation_modet::INVARIANT,
+      false,
+      "unexpected binary SVA expression",
+      expr.pretty());
   }
 }
 
@@ -409,22 +424,38 @@ exprt verilog_typecheck_exprt::convert_ternary_sva(ternary_exprt expr)
   else
   {
     // not SVA
-    return convert_expr_rec(std::move(expr));
+    DATA_CHECK_WITH_DIAGNOSTICS(
+      validation_modet::INVARIANT,
+      false,
+      "unexpected ternary SVA expression",
+      expr.pretty());
   }
 }
 
 exprt verilog_typecheck_exprt::convert_sva_rec(exprt expr)
 {
-  switch(expr.operands().size())
-  {
-  case 1:
-    return convert_unary_sva(to_unary_expr(expr));
-  case 2:
-    return convert_binary_sva(to_binary_expr(expr));
-  case 3:
-    return convert_ternary_sva(to_ternary_expr(expr));
-  default:
-    return convert_expr_rec(expr);
+  if(is_SVA_operator(expr))
+  {
+    switch(expr.operands().size())
+    {
+    case 1:
+      return convert_unary_sva(to_unary_expr(expr));
+    case 2:
+      return convert_binary_sva(to_binary_expr(expr));
+    case 3:
+      return convert_ternary_sva(to_ternary_expr(expr));
+    default:
+      DATA_CHECK_WITH_DIAGNOSTICS(
+        validation_modet::INVARIANT,
+        false,
+        "unexpected SVA expression",
+        expr.pretty());
+    }
+  }
+  else
+  {
+    // not SVA, but an expression that gets sampled.
+    return convert_expr_rec(std::move(expr));
   }
 }