Merge pull request #1071 from diffblue/sva-default-sequence-semantics

SVA: default sequence semantics

Author: tautschnig

src/hw_cbmc_irep_ids.h

@@ -49,6 +49,8 @@ IREP_ID_ONE(sva_accept_on)
 IREP_ID_ONE(sva_reject_on)
 IREP_ID_ONE(sva_sync_accept_on)
 IREP_ID_ONE(sva_sync_reject_on)
+IREP_ID_ONE(sva_implicit_strong)
+IREP_ID_ONE(sva_implicit_weak)
 IREP_ID_ONE(sva_strong)
 IREP_ID_ONE(sva_weak)
 IREP_ID_ONE(sva_if)

src/temporal-logic/trivial_sva.cpp

@@ -107,11 +107,13 @@ exprt trivial_sva(exprt expr)
     op = trivial_sva(op);
 
   // post-traversal
-  if(expr.id() == ID_sva_sequence_property)
+  if(
+    expr.id() == ID_sva_weak || expr.id() == ID_sva_strong ||
+    expr.id() == ID_sva_implicit_weak || expr.id() == ID_sva_implicit_strong)
   {
     // We simplify sequences to boolean expressions, and hence can drop
     // the sva_sequence_property converter
-    auto &op = to_sva_sequence_property_expr(expr).sequence();
+    auto &op = to_sva_sequence_property_expr_base(expr).sequence();
     if(op.type().id() == ID_bool)
       return op;
   }

src/trans-word-level/property.cpp

@@ -527,10 +527,24 @@ static obligationst property_obligations_rec(
       return property_obligations_rec(
         op_negated_opt.value(), current, no_timeframes);
     }
-    else if(is_SVA_sequence_operator(op))
+    else if(
+      op.id() == ID_sva_strong || op.id() == ID_sva_weak ||
+      op.id() == ID_sva_implicit_strong || op.id() == ID_sva_implicit_weak)
     {
-      return obligationst{
-        instantiate_property(property_expr, current, no_timeframes)};
+      // The sequence must not match.
+      auto &sequence = to_sva_sequence_property_expr_base(op).sequence();
+
+      const auto matches =
+        instantiate_sequence(sequence, current, no_timeframes);
+
+      obligationst obligations;
+
+      for(auto &match : matches)
+      {
+        obligations.add(match.end_time, not_exprt{match.condition});
+      }
+
+      return obligations;
     }
     else if(is_temporal_operator(op))
     {
@@ -647,7 +661,8 @@ static obligationst property_obligations_rec(
   }
   else if(
     property_expr.id() == ID_sva_strong || property_expr.id() == ID_sva_weak ||
-    property_expr.id() == ID_sva_sequence_property)
+    property_expr.id() == ID_sva_implicit_strong ||
+    property_expr.id() == ID_sva_implicit_weak)
   {
     auto &sequence =
       to_sva_sequence_property_expr_base(property_expr).sequence();
@@ -667,6 +682,11 @@ static obligationst property_obligations_rec(
 
     return obligationst{max, disjunction(disjuncts)};
   }
+  else if(property_expr.id() == ID_sva_sequence_property)
+  {
+    // Should have been turned into sva_implict_weak or sva_implict_strong in the type checker.
+    PRECONDITION(false);
+  }
   else
   {
     return obligationst{

src/verilog/expr2verilog.cpp

@@ -536,9 +536,14 @@ expr2verilogt::resultt expr2verilogt::convert_sva_unary(
 
   if(op.id() == ID_typecast)
     op_operands = to_typecast_expr(op).op().operands().size();
-  else if(src.op().id() == ID_sva_sequence_property)
+  else if(
+    src.op().id() == ID_sva_sequence_property ||
+    src.op().id() == ID_sva_implicit_weak ||
+    src.op().id() == ID_sva_implicit_strong)
+  {
     op_operands =
-      to_sva_sequence_property_expr(op).sequence().operands().size();
+      to_sva_sequence_property_expr_base(op).sequence().operands().size();
+  }
   else
     op_operands = op.operands().size();
 
@@ -1816,8 +1821,12 @@ 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).sequence());
+  else if(
+    src.id() == ID_sva_sequence_property ||
+    src.id() == ID_sva_implicit_strong || src.id() == ID_sva_implicit_weak)
+  {
+    return convert_rec(to_sva_sequence_property_expr_base(src).sequence());
+  }
 
   else if(src.id()==ID_sva_sequence_concatenation)
     return convert_sva_sequence_concatenation(

src/verilog/sva_expr.h

@@ -1143,7 +1143,7 @@ to_sva_sequence_property_expr_base(const exprt &expr)
 }
 
 inline sva_sequence_property_expr_baset &
-to_sva_sequence_property_base_expr(exprt &expr)
+to_sva_sequence_property_expr_base(exprt &expr)
 {
   sva_sequence_property_expr_baset::check(expr);
   return static_cast<sva_sequence_property_expr_baset &>(expr);
@@ -1152,45 +1152,47 @@ to_sva_sequence_property_base_expr(exprt &expr)
 class sva_strong_exprt : public sva_sequence_property_expr_baset
 {
 public:
-  sva_strong_exprt(exprt __op)
-    : sva_sequence_property_expr_baset(ID_sva_strong, std::move(__op))
+  sva_strong_exprt(irep_idt __id, exprt __op)
+    : sva_sequence_property_expr_baset(__id, std::move(__op))
   {
   }
 };
 
 inline const sva_strong_exprt &to_sva_strong_expr(const exprt &expr)
 {
-  PRECONDITION(expr.id() == ID_sva_strong);
+  PRECONDITION(
+    expr.id() == ID_sva_strong || expr.id() == ID_sva_implicit_strong);
   sva_strong_exprt::check(expr);
   return static_cast<const sva_strong_exprt &>(expr);
 }
 
 inline sva_strong_exprt &to_sva_strong_expr(exprt &expr)
 {
-  PRECONDITION(expr.id() == ID_sva_strong);
+  PRECONDITION(
+    expr.id() == ID_sva_strong || expr.id() == ID_sva_implicit_strong);
   sva_strong_exprt::check(expr);
   return static_cast<sva_strong_exprt &>(expr);
 }
 
 class sva_weak_exprt : public sva_sequence_property_expr_baset
 {
 public:
-  sva_weak_exprt(exprt __op)
-    : sva_sequence_property_expr_baset(ID_sva_weak, std::move(__op))
+  sva_weak_exprt(irep_idt __id, exprt __op)
+    : sva_sequence_property_expr_baset(__id, std::move(__op))
   {
   }
 };
 
 inline const sva_weak_exprt &to_sva_weak_expr(const exprt &expr)
 {
-  PRECONDITION(expr.id() == ID_sva_weak);
+  PRECONDITION(expr.id() == ID_sva_weak || expr.id() == ID_sva_implicit_weak);
   sva_weak_exprt::check(expr);
   return static_cast<const sva_weak_exprt &>(expr);
 }
 
 inline sva_weak_exprt &to_sva_weak_expr(exprt &expr)
 {
-  PRECONDITION(expr.id() == ID_sva_weak);
+  PRECONDITION(expr.id() == ID_sva_weak || expr.id() == ID_sva_implicit_weak);
   sva_weak_exprt::check(expr);
   return static_cast<sva_weak_exprt &>(expr);
 }
@@ -1584,4 +1586,11 @@ to_sva_sequence_property_expr(exprt &expr)
   return static_cast<sva_sequence_property_exprt &>(expr);
 }
 
+/// SVA sequences can be interpreted as weak or strong
+enum class sva_sequence_semanticst
+{
+  WEAK,
+  STRONG
+};
+
 #endif

src/verilog/verilog_typecheck.cpp

@@ -1060,6 +1060,12 @@ void verilog_typecheckt::convert_assert_assume_cover(
   convert_sva(cond);
   require_sva_property(cond);
 
+  // 1800-2017 16.12.2 Sequence property
+  if(module_item.id() == ID_verilog_cover_property)
+    set_default_sequence_semantics(cond, sva_sequence_semanticst::STRONG);
+  else
+    set_default_sequence_semantics(cond, sva_sequence_semanticst::WEAK);
+
   // We create a symbol for the property.
   // The 'value' of the symbol is set by synthesis.
   const irep_idt &identifier = module_item.identifier();
@@ -1125,6 +1131,12 @@ void verilog_typecheckt::convert_assert_assume_cover(
   convert_sva(cond);
   require_sva_property(cond);
 
+  // 1800-2017 16.12.2 Sequence property
+  if(statement.id() == ID_verilog_cover_property)
+    set_default_sequence_semantics(cond, sva_sequence_semanticst::STRONG);
+  else
+    set_default_sequence_semantics(cond, sva_sequence_semanticst::WEAK);
+
   // We create a symbol for the property.
   // The 'value' is set by synthesis.
   const irep_idt &identifier = statement.identifier();

src/verilog/verilog_typecheck_expr.h

@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/namespace.h>
 #include <util/std_expr.h>
 
+#include "sva_expr.h"
 #include "verilog_typecheck_base.h"
 
 #include <stack>
@@ -207,6 +208,8 @@ class verilog_typecheck_exprt:public verilog_typecheck_baset
   [[nodiscard]] exprt convert_binary_sva(binary_exprt);
   [[nodiscard]] exprt convert_ternary_sva(ternary_exprt);
 
+  static void set_default_sequence_semantics(exprt &, sva_sequence_semanticst);
+
   // system functions
   exprt bits(const exprt &);
   std::optional<mp_integer> bits_rec(const typet &) const;

src/verilog/verilog_typecheck_sva.cpp

@@ -430,3 +430,35 @@ exprt verilog_typecheck_exprt::convert_sva_rec(exprt expr)
     return convert_expr_rec(expr);
   }
 }
+
+// 1800-2017 16.12.2 Sequence property
+// Sequences are by default _weak_ when used in assert property
+// or assume property, and are _strong_ when used in cover property.
+// This flips when below the SVA not operator.
+void verilog_typecheck_exprt::set_default_sequence_semantics(
+  exprt &expr,
+  sva_sequence_semanticst semantics)
+{
+  if(expr.id() == ID_sva_sequence_property)
+  {
+    // apply
+    if(semantics == sva_sequence_semanticst::WEAK)
+      expr.id(ID_sva_implicit_weak);
+    else
+      expr.id(ID_sva_implicit_strong);
+  }
+  else if(expr.id() == ID_sva_not)
+  {
+    // flip
+    semantics = semantics == sva_sequence_semanticst::WEAK
+                  ? sva_sequence_semanticst::STRONG
+                  : sva_sequence_semanticst::WEAK;
+
+    set_default_sequence_semantics(to_sva_not_expr(expr).op(), semantics);
+  }
+  else
+  {
+    for(auto &op : expr.operands())
+      set_default_sequence_semantics(op, semantics);
+  }
+}