Merge pull request #1041 from diffblue/verilog_sva_sequence

Verilog: type for SVA sequences

Author: tautschnig

regression/verilog/SVA/sequence_implication2.desc

@@ -1,7 +1,7 @@
 CORE
 sequence_implication2.sv
 --module main
-^file .* line 4: sequence required$
+^file .* line 4: sequence required, but got property$
 ^EXIT=2$
 ^SIGNAL=0$
 --

regression/verilog/SVA/sequence_repetition6.desc

@@ -1,7 +1,7 @@
 CORE
 sequence_repetition6.sv
 
-^file .* line 4: sequence required$
+^file .* line 4: sequence required, but got property$
 ^EXIT=2$
 ^SIGNAL=0$
 --

src/hw_cbmc_irep_ids.h

@@ -136,6 +136,7 @@ IREP_ID_ONE(verilog_null)
 IREP_ID_ONE(verilog_event)
 IREP_ID_ONE(verilog_event_trigger)
 IREP_ID_ONE(verilog_string)
+IREP_ID_ONE(verilog_sva_sequence)
 IREP_ID_ONE(reg)
 IREP_ID_ONE(macromodule)
 IREP_ID_ONE(output_register)

src/temporal-logic/normalize_property.cpp

@@ -97,14 +97,6 @@ exprt normalize_property_rec(exprt expr)
   {
     expr = sva_s_eventually_exprt{to_sva_cycle_delay_star_expr(expr).op()};
   }
-  else if(expr.id() == ID_sva_strong)
-  {
-    expr = to_sva_strong_expr(expr).op();
-  }
-  else if(expr.id() == ID_sva_weak)
-  {
-    expr = to_sva_weak_expr(expr).op();
-  }
 
   // normalize the operands
   for(auto &op : expr.operands())

src/temporal-logic/trivial_sva.cpp

@@ -12,19 +12,29 @@ Author: Daniel Kroening, [email protected]
 
 #include "temporal_logic.h"
 
+static std::optional<exprt> is_state_formula(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;
+  else
+    return {};
+}
+
 exprt trivial_sva(exprt expr)
 {
   // pre-traversal
   if(expr.id() == ID_sva_overlapped_implication)
   {
     // Same as regular implication if lhs and rhs are not sequences.
     auto &sva_implication = to_sva_overlapped_implication_expr(expr);
-    if(
-      !is_SVA_sequence_operator(sva_implication.lhs()) &&
-      !is_SVA_sequence_operator(sva_implication.rhs()))
-    {
-      expr = implies_exprt{sva_implication.lhs(), sva_implication.rhs()};
-    }
+
+    auto lhs = is_state_formula(sva_implication.lhs());
+    auto rhs = is_state_formula(sva_implication.rhs());
+
+    if(lhs.has_value() && rhs.has_value())
+      expr = implies_exprt{*lhs, *rhs};
   }
   else if(expr.id() == ID_sva_iff)
   {
@@ -38,21 +48,25 @@ exprt trivial_sva(exprt expr)
   }
   else if(expr.id() == ID_sva_and)
   {
-    // Same as a ∧ b if lhs and rhs are not sequences.
     auto &sva_and = to_sva_and_expr(expr);
-    if(
-      !is_SVA_sequence_operator(sva_and.lhs()) &&
-      !is_SVA_sequence_operator(sva_and.rhs()))
-      expr = and_exprt{sva_and.lhs(), sva_and.rhs()};
+
+    // 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());
+
+    if(lhs.has_value() && rhs.has_value())
+      expr = and_exprt{*lhs, *rhs};
   }
   else if(expr.id() == ID_sva_or)
   {
-    // Same as a ∧ b if lhs or rhs are not sequences.
     auto &sva_or = to_sva_or_expr(expr);
-    if(
-      !is_SVA_sequence_operator(sva_or.lhs()) &&
-      !is_SVA_sequence_operator(sva_or.rhs()))
-      expr = or_exprt{sva_or.lhs(), sva_or.rhs()};
+
+    // 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());
+
+    if(lhs.has_value() && rhs.has_value())
+      expr = or_exprt{*lhs, *rhs};
   }
   else if(expr.id() == ID_sva_not)
   {
@@ -93,6 +107,14 @@ exprt trivial_sva(exprt expr)
     op = trivial_sva(op);
 
   // post-traversal
+  if(expr.id() == ID_typecast)
+  {
+    // 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)
+      return op;
+  }
 
   return expr;
 }

src/trans-word-level/instantiate_word_level.cpp

@@ -119,11 +119,15 @@ wl_instantiatet::instantiate_rec(exprt expr, const mp_integer &t) const
   {
     return {t, timeframe_symbol(t, to_symbol_expr(std::move(expr)))};
   }
-  else if(is_SVA_sequence_operator(expr))
+  else if(
+    expr.id() == ID_typecast && expr.type().id() == ID_bool &&
+    to_typecast_expr(expr).op().type().id() == ID_verilog_sva_sequence)
   {
+    auto &sequence = to_typecast_expr(expr).op();
+
     // sequence expressions -- these may have multiple potential
     // match points, and evaluate to true if any of them matches
-    const auto matches = instantiate_sequence(expr, t, no_timeframes);
+    const auto matches = instantiate_sequence(sequence, t, no_timeframes);
     exprt::operandst disjuncts;
     disjuncts.reserve(matches.size());
     mp_integer max = t;

src/trans-word-level/property.cpp

@@ -645,6 +645,26 @@ static obligationst property_obligations_rec(
     }
     return obligationst{t, disjunction(disjuncts)};
   }
+  else if(
+    property_expr.id() == ID_sva_strong || property_expr.id() == ID_sva_weak)
+  {
+    auto &sequence = to_unary_expr(property_expr).op();
+
+    // sequence expressions -- these may have multiple potential
+    // match points, and evaluate to true if any of them matches
+    const 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
   {
     return obligationst{

src/verilog/expr2verilog.cpp

@@ -531,8 +531,16 @@ expr2verilogt::resultt expr2verilogt::convert_sva_unary(
   const unary_exprt &src)
 {
   auto op = convert_rec(src.op());
-  if(op.p == verilog_precedencet::MIN && src.op().operands().size() >= 2)
+
+  auto op_skip_typecast =
+    src.op().id() == ID_typecast ? to_typecast_expr(src.op()).op() : src.op();
+
+  if(
+    op.p == verilog_precedencet::MIN && op_skip_typecast.operands().size() >= 2)
+  {
     op.s = "(" + op.s + ")";
+  }
+
   return {verilog_precedencet::MIN, name + " " + op.s};
 }
 

src/verilog/sva_expr.cpp

@@ -41,7 +41,8 @@ exprt sva_case_exprt::lowering() const
 
 exprt sva_sequence_consecutive_repetition_exprt::lower() const
 {
-  PRECONDITION(op().type().id() == ID_bool);
+  PRECONDITION(
+    op().type().id() == ID_bool || op().type().id() == ID_verilog_sva_sequence);
 
   if(to().is_nil())
   {

src/verilog/sva_expr.h

@@ -11,6 +11,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/std_expr.h>
 
+#include "verilog_types.h"
+
 /// accept_on, reject_on, sync_accept_on, sync_reject_on, disable_iff
 class sva_abort_exprt : public binary_predicate_exprt
 {
@@ -1240,7 +1242,7 @@ class sva_sequence_consecutive_repetition_exprt : public ternary_exprt
         std::move(__op),
         std::move(__repetitions),
         nil_exprt{},
-        bool_typet{}}
+        verilog_sva_sequence_typet{}}
   {
   }
 
@@ -1253,7 +1255,7 @@ class sva_sequence_consecutive_repetition_exprt : public ternary_exprt
         std::move(__op),
         std::move(__from),
         std::move(__to),
-        bool_typet{}}
+        verilog_sva_sequence_typet{}}
   {
   }
 

src/verilog/verilog_typecheck.cpp

@@ -1051,7 +1051,7 @@ void verilog_typecheckt::convert_assert_assume_cover(
   exprt &cond = module_item.condition();
 
   convert_sva(cond);
-  make_boolean(cond);
+  require_sva_property(cond);
 
   // We create a symbol for the property.
   // The 'value' of the symbol is set by synthesis.
@@ -1116,7 +1116,7 @@ void verilog_typecheckt::convert_assert_assume_cover(
   exprt &cond = statement.condition();
 
   convert_sva(cond);
-  make_boolean(cond);
+  require_sva_property(cond);
 
   // We create a symbol for the property.
   // The 'value' is set by synthesis.
@@ -1819,11 +1819,11 @@ void verilog_typecheckt::convert_sequence_declaration(
   auto base_name = declaration.base_name();
   auto full_identifier = hierarchical_identifier(base_name);
 
-  convert_sva(declaration.sequence());
+  auto &sequence = declaration.sequence();
+  convert_sva(sequence);
+  require_sva_sequence(sequence);
 
-  auto type = bool_typet{};
-  type.set(ID_C_verilog_type, ID_verilog_sequence_declaration);
-  symbolt symbol{full_identifier, type, mode};
+  symbolt symbol{full_identifier, sequence.type(), mode};
 
   symbol.module = module_identifier;
   symbol.base_name = base_name;