SVA: default sequence semantics

SVA sequences can have weak or strong semantics.  1800-2017 16.12.2 Sequence
property requires that sequences in properties that are not explicitly
marked as strong or weak are interpreted as weak when used in assert
property or assume property, and strong otherwise.

The Verilog type checker now emits corresponding expressions
sva_implict_weak and sva_implicit_strong for uses of SVA sequences in
properties.

Author: kroening

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);
+  }
+}