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

regression/verilog/SVA/sva_and1.desc

@@ -1,7 +1,7 @@
 CORE
 sva_and1.sv
 
-^\[main\.p0\] always \(1 and 1\): PROVED$
+^\[main\.p0\] always \(1 and 1\): PROVED up to bound 5$
 ^\[main\.p1\] always \(1 and 0\): REFUTED$
 ^\[main\.p2\] always \(1 and 32'b0000000000000000000000000000000x\): REFUTED$
 ^EXIT=10$

src/ebmc/completeness_threshold.cpp

@@ -68,10 +68,18 @@ bool has_low_completeness_threshold(const exprt &expr)
     expr.id() == ID_sva_implicit_strong || expr.id() == ID_sva_implicit_weak)
   {
     auto &sequence = to_sva_sequence_property_expr_base(expr).sequence();
-    if(!is_SVA_sequence_operator(sequence))
-      return true;
-    else
-      return false;
+    return has_low_completeness_threshold(sequence);
+  }
+  else if(expr.id() == ID_sva_boolean)
+  {
+    return true;
+  }
+  else if(expr.id() == ID_sva_or || expr.id() == ID_sva_and)
+  {
+    for(auto &op : expr.operands())
+      if(!has_low_completeness_threshold(op))
+        return false;
+    return true;
   }
   else if(expr.id() == ID_sva_sequence_property)
   {

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/nnf.cpp

@@ -149,6 +149,24 @@ std::optional<exprt> negate_property_node(const exprt &expr)
     return sva_non_overlapped_implication_exprt{
       followed_by.antecedent(), not_b};
   }
+  else if(expr.id() == ID_sva_overlapped_implication)
+  {
+    // 1800 2017 16.12.9
+    // !(a |-> b)   --->   a #-# !b
+    auto &implication = to_sva_implication_base_expr(expr);
+    auto not_b = not_exprt{implication.consequent()};
+    return sva_followed_by_exprt{
+      implication.antecedent(), ID_sva_overlapped_followed_by, not_b};
+  }
+  else if(expr.id() == ID_sva_non_overlapped_implication)
+  {
+    // 1800 2017 16.12.9
+    // !(a |=> b)   --->   a #=# !b
+    auto &implication = to_sva_implication_base_expr(expr);
+    auto not_b = not_exprt{implication.consequent()};
+    return sva_followed_by_exprt{
+      implication.antecedent(), ID_sva_nonoverlapped_followed_by, not_b};
+  }
   else
     return {};
 }

src/temporal-logic/normalize_property.cpp

@@ -23,12 +23,26 @@ 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()))
+  // a|=>b is the 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);
+}
+
+exprt normalize_pre_sva_overlapped_implication(
+  sva_overlapped_implication_exprt expr)
+{
+  // a|->b is the same as a->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();
+    return implies_exprt{lhs_cond, expr.rhs()};
   }
   else
     return std::move(expr);
@@ -42,6 +56,11 @@ exprt normalize_property_rec(exprt expr)
     expr = normalize_pre_sva_non_overlapped_implication(
       to_sva_non_overlapped_implication_expr(expr));
   }
+  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_nexttime)
   {
     auto one = natural_typet{}.one_expr();

src/temporal-logic/normalize_property.h

@@ -13,15 +13,14 @@ Author: Daniel Kroening, [email protected]
 
 /// This applies the following rewrites:
 ///
-/// cover(φ) --> G¬φ
-///
 /// -----Propositional-----
 /// ¬(a ∨ b) --> ¬a ∧ ¬b
 /// ¬(a ∧ b) --> ¬a ∨ ¬b
 /// (a -> b) --> ¬a ∨ b
 ///
 /// -----SVA-----
-/// sva_non_overlapped_implication --> ¬a ∨ always[1:1] b   if a is not an SVA sequence
+/// a|=>b --> ¬a ∨ always[1:1] b   if a is not an SVA sequence
+/// a|->b --> a⇒b                  if a is not an SVA sequence
 /// sva_nexttime φ --> sva_always[1:1] φ
 /// sva_nexttime[i] φ --> sva_always[i:i] φ
 /// sva_s_nexttime φ --> sva_always[1:1] φ

src/temporal-logic/sva_to_ltl.cpp

@@ -42,10 +42,10 @@ 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}};
+    return {{to_sva_boolean_expr(sequence).op(), 1}};
   }
   else if(sequence.id() == ID_sva_sequence_concatenation)
   {

src/temporal-logic/trivial_sva.cpp

@@ -12,12 +12,10 @@ Author: Daniel Kroening, [email protected]
 
 #include "temporal_logic.h"
 
-static std::optional<exprt> is_state_formula(const exprt &expr)
+static std::optional<exprt> is_state_predicate(const exprt &expr)
 {
-  if(expr.id() == ID_typecast && expr.type().id() == ID_verilog_sva_sequence)
-    return to_typecast_expr(expr).op();
-  else if(expr.type().id() == ID_bool)
-    return expr;
+  if(expr.id() == ID_sva_boolean)
+    return to_sva_boolean_expr(expr).op();
   else
     return {};
 }
@@ -30,8 +28,8 @@ exprt trivial_sva(exprt expr)
     // Same as regular implication if lhs and rhs are not sequences.
     auto &sva_implication = to_sva_overlapped_implication_expr(expr);
 
-    auto lhs = is_state_formula(sva_implication.lhs());
-    auto rhs = is_state_formula(sva_implication.rhs());
+    auto lhs = is_state_predicate(sva_implication.lhs());
+    auto rhs = is_state_predicate(sva_implication.rhs());
 
     if(lhs.has_value() && rhs.has_value())
       expr = implies_exprt{*lhs, *rhs};
@@ -51,22 +49,22 @@ exprt trivial_sva(exprt expr)
     auto &sva_and = to_sva_and_expr(expr);
 
     // Same as a ∧ b if the expression is not a sequence.
-    auto lhs = is_state_formula(sva_and.lhs());
-    auto rhs = is_state_formula(sva_and.rhs());
+    auto lhs = is_state_predicate(sva_and.lhs());
+    auto rhs = is_state_predicate(sva_and.rhs());
 
     if(lhs.has_value() && rhs.has_value())
-      expr = and_exprt{*lhs, *rhs};
+      expr = sva_boolean_exprt{and_exprt{*lhs, *rhs}, expr.type()};
   }
   else if(expr.id() == ID_sva_or)
   {
     auto &sva_or = to_sva_or_expr(expr);
 
     // Same as a ∨ b if the expression is not a sequence.
-    auto lhs = is_state_formula(sva_or.lhs());
-    auto rhs = is_state_formula(sva_or.rhs());
+    auto lhs = is_state_predicate(sva_or.lhs());
+    auto rhs = is_state_predicate(sva_or.rhs());
 
     if(lhs.has_value() && rhs.has_value())
-      expr = or_exprt{*lhs, *rhs};
+      expr = sva_boolean_exprt{or_exprt{*lhs, *rhs}, expr.type()};
   }
   else if(expr.id() == ID_sva_not)
   {
@@ -113,9 +111,10 @@ exprt trivial_sva(exprt expr)
   {
     // We simplify sequences to boolean expressions, and hence can drop
     // the sva_sequence_property converter
-    auto &op = to_sva_sequence_property_expr_base(expr).sequence();
-    if(op.type().id() == ID_bool)
-      return op;
+    auto &sequence = to_sva_sequence_property_expr_base(expr).sequence();
+    auto pred_opt = is_state_predicate(sequence);
+    if(pred_opt.has_value())
+      return *pred_opt;
   }
 
   return expr;

src/trans-word-level/sequence.cpp

@@ -454,10 +454,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

@@ -1815,6 +1815,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);