Fix for sequences in named properties

Sequences that are in named properties now get the proper weak/strong
semantics.  This is achieved by moving the code that assigns the implicit
weak/strong semantics from the type checker to the synthesis pass, where
named properties are already expanded.

Author: kroening

regression/verilog/property/named_property4.desc

@@ -1,9 +1,8 @@
-KNOWNBUG
+CORE
 named_property4.sv
 
 ^EXIT=10$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-This triggers an internal error.

src/verilog/verilog_synthesis.cpp

@@ -130,6 +130,38 @@ exprt verilog_synthesist::synth_expr_rec(exprt expr, symbol_statet symbol_state)
   UNREACHABLE;
 }
 
+// 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_synthesist::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);
+  }
+}
+
 /*******************************************************************\
 
 Function: verilog_synthesist::synthesis_constant
@@ -2326,6 +2358,12 @@ void verilog_synthesist::synth_assert_assume_cover(
     cond = sva_cover_exprt(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);
+
   symbol.value = std::move(cond);
 }
 
@@ -2401,6 +2439,12 @@ void verilog_synthesist::synth_assert_assume_cover(
   else
     PRECONDITION(false);
 
+  // 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);
+
   symbol.value = std::move(cond);
 }
 

src/verilog/verilog_synthesis_class.h

@@ -15,6 +15,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/std_expr.h>
 #include <util/string_hash.h>
 
+#include "sva_expr.h"
 #include "verilog_expr.h"
 #include "verilog_symbol_table.h"
 #include "verilog_typecheck_base.h"
@@ -235,6 +236,8 @@ class verilog_synthesist:
     const membert &member,
     assignmentt::datat &data);
 
+  static void set_default_sequence_semantics(exprt &, sva_sequence_semanticst);
+
   // module items
   virtual void convert_module_items(symbolt &);
   void synth_module_item(const verilog_module_itemt &, transt &);

src/verilog/verilog_typecheck.cpp

@@ -1060,12 +1060,6 @@ 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();
@@ -1131,12 +1125,6 @@ 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

@@ -209,8 +209,6 @@ class verilog_typecheck_exprt:public verilog_typecheck_baset
   [[nodiscard]] exprt convert_ternary_sva(ternary_exprt);
   [[nodiscard]] exprt convert_other_sva(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

@@ -480,35 +480,3 @@ exprt verilog_typecheck_exprt::convert_sva_rec(exprt expr)
     return convert_other_sva(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);
-  }
-}