Verilog: generate property description prior to expression synthesis

regression/verilog/SVA/immediate1.desc

@@ -1,7 +1,7 @@
 CORE
 immediate1.sv
 --bound 20
-^\[main\.assert\.1\] always \(main\.x == 11 \|-> main\.x & 1\): PROVED up to bound 20$
+^\[main\.assert\.1\] always main\.x & 1: PROVED up to bound 20$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/SVA/immediate2.desc

@@ -1,7 +1,7 @@
 CORE broken-smt-backend
 immediate2.sv
 --bound 0
-^\[main\.assert\.1\] assume always \(main\.index >= 10 |-> 0\): ASSUMED$
+^\[main\.assume\.1\] assume always 0: ASSUMED$
 ^\[main\.assert\.2\] always main\.index < 10: PROVED up to bound 0$
 ^\[main\.assert\.3\] always 0: REFUTED$
 ^EXIT=10$

regression/verilog/SVA/initial2.desc

@@ -1,7 +1,7 @@
 CORE
 initial2.sv
 --module main --bound 1
-^\[main\.assert\.1\] 1 == 1: PROVED up to bound 1
+^\[main\.assert\.1\] main\.counter == 1: PROVED up to bound 1
 ^\[main\.assert\.2\] main\.counter == 2: PROVED up to bound 1
 ^EXIT=0$
 ^SIGNAL=0$

regression/verilog/SVA/named_property1.desc

@@ -1,7 +1,7 @@
 CORE
 named_property1.sv
 --bound 0
-^\[main\.assert\.1\] always main\.x == 10: PROVED up to bound 0$
+^\[main\.assert\.1\] always main\.x_is_ten: PROVED up to bound 0$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/SVA/unbounded1.desc

@@ -1,7 +1,7 @@
 CORE
 unbounded1.sv
 --module main --bound 1
-^\[main\.assert\.1\] always \(main\.a ##\[0:\$\] main.b\): REFUTED$
+^\[main\.assert\.1\] always \(main\.a ##\[0:main\.upper\] main.b\): REFUTED$
 ^EXIT=10$
 ^SIGNAL=0$
 --

regression/verilog/enums/enum4.desc

@@ -3,5 +3,5 @@ enum4.sv
 --bound 0
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main\.p1\] always main.A == main.A: PROVED up to bound 0$
+^\[main\.p1\] always main\.A == 1: PROVED up to bound 0$
 --

regression/verilog/enums/enum_base_type1.desc

@@ -3,5 +3,5 @@ enum_base_type1.sv
 --bound 0
 ^EXIT=0$
 ^SIGNAL=0$
-^\[.*\] always 8 == 8: PROVED up to bound 0$
+^\[.*\] always \$bits\(main\.A\) == 8: PROVED up to bound 0$
 --

regression/verilog/enums/enum_base_type2.desc

@@ -3,5 +3,5 @@ enum_base_type2.sv
 --bound 0
 ^EXIT=0$
 ^SIGNAL=0$
-^\[.*\] always 8 == 8: PROVED up to bound 0$
+^\[.*\] always \$bits\(main\.A\) == main\.p: PROVED up to bound 0$
 --

regression/verilog/expressions/concatenation2.desc

@@ -3,7 +3,7 @@ concatenation2.v
 --bound 0
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main\.property\.pA\] always -1 == -1: PROVED up to bound 0$
-^\[main\.property\.pB\] always 15 == 15: PROVED up to bound 0$
+^\[main\.property\.pA\] always main\.A == -1: PROVED up to bound 0$
+^\[main\.property\.pB\] always main\.B == 15: PROVED up to bound 0$
 --
 ^warning: ignoring

regression/verilog/expressions/static_cast1.desc

@@ -3,6 +3,6 @@ static_cast1.sv
 --module main --bound 0
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main\.p0\] always 255 == 255: PROVED up to bound 0$
+^\[main\.p0\] always 'hFFFF == 255: PROVED up to bound 0$
 --
 ^warning: ignoring

regression/verilog/modules/type_parameters1.desc

@@ -1,8 +1,8 @@
 CORE
 type_parameters1.sv
 --bound 0
-^\[main\.p1\] always 1 == 1: PROVED up to bound 0$
-^\[main\.p2\] always 32 == 32: PROVED up to bound 0$
+^\[main\.p1\] always \$bits\(main\.T1\) == 1: PROVED up to bound 0$
+^\[main\.p2\] always \$bits\(main\.T2\) == 32: PROVED up to bound 0$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/structs/structs1.desc

@@ -1,7 +1,7 @@
 CORE
 structs1.sv
 --bound 0
-^\[main\.p0\] always 9 == 9: PROVED up to bound 0$
+^\[main\.p0\] always \$bits\(main\.s\) == 9: PROVED up to bound 0$
 ^\[main\.p1\] always main\.s\.field1 == 1: PROVED up to bound 0$
 ^\[main\.p2\] always main\.s\.field2 == 0: PROVED up to bound 0$
 ^\[main\.p3\] always main\.s\.field3 == 115: PROVED up to bound 0$

regression/verilog/system-functions/array_functions1.desc

@@ -1,21 +1,21 @@
 CORE
 array_functions1.sv
 --module main --bound 0
-^\[main\.pP0\] always 32 == 32 && 1 == 1: PROVED up to bound 0$
-^\[main\.pP1\] always 0 == 0 && 31 == 31: PROVED up to bound 0$
-^\[main\.pP2\] always 1 == 1 && 32 == 32: PROVED up to bound 0$
-^\[main\.pP3\] always 0 == 0 && 31 == 31: PROVED up to bound 0$
-^\[main\.pP4\] always 1 == 1: PROVED up to bound 0$
-^\[main\.pP5\] always -1 == -1: PROVED up to bound 0$
-^\[main\.pU0\] always 32 == 32 && 1 == 1: PROVED up to bound 0$
-^\[main\.pU1\] always 0 == 0 && 31 == 31: PROVED up to bound 0$
-^\[main\.pU2\] always 31 == 31 && 0 == 0: PROVED up to bound 0$
-^\[main\.pU3\] always 1 == 1 && 32 == 32: PROVED up to bound 0$
-^\[main\.pU4\] always 0 == 0 && 31 == 31: PROVED up to bound 0$
-^\[main\.pU5\] always 0 == 0 && 31 == 31: PROVED up to bound 0$
-^\[main\.pU6\] always 1 == 1: PROVED up to bound 0$
-^\[main\.pU7\] always -1 == -1: PROVED up to bound 0$
-^\[main\.pU8\] always 1 == 1: PROVED up to bound 0$
+^\[main\.pP0\] always \$left\(main\.packed1\) == 32 && \$right\(main\.packed1\) == 1: PROVED up to bound 0$
+^\[main\.pP1\] always \$left\(main\.packed2\) == 0 && \$right\(main\.packed2\) == 31: PROVED up to bound 0$
+^\[main\.pP2\] always \$low\(main\.packed1\) == 1 && \$high\(main\.packed1\) == 32: PROVED up to bound 0$
+^\[main\.pP3\] always \$low\(main\.packed2\) == 0 && \$high\(main\.packed2\) == 31: PROVED up to bound 0$
+^\[main\.pP4\] always \$increment\(main\.packed1\) == 1: PROVED up to bound 0$
+^\[main\.pP5\] always \$increment\(main\.packed2\) == -1: PROVED up to bound 0$
+^\[main\.pU0\] always \$left\(main\.unpacked1\) == 32 && \$right\(main\.unpacked1\) == 1: PROVED up to bound 0$
+^\[main\.pU1\] always \$left\(main\.unpacked2\) == 0 && \$right\(main\.unpacked2\) == 31: PROVED up to bound 0$
+^\[main\.pU2\] always \$left\(main\.unpacked3\) == 31 && \$right\(main\.unpacked3\) == 0: PROVED up to bound 0$
+^\[main\.pU3\] always \$low\(main\.unpacked1\) == 1 && \$high\(main\.unpacked1\) == 32: PROVED up to bound 0$
+^\[main\.pU4\] always \$low\(main\.unpacked2\) == 0 && \$high\(main\.unpacked2\) == 31: PROVED up to bound 0$
+^\[main\.pU5\] always \$low\(main\.unpacked3\) == 0 && \$high\(main\.unpacked3\) == 31: PROVED up to bound 0$
+^\[main\.pU6\] always \$increment\(main\.unpacked1\) == 1: PROVED up to bound 0$
+^\[main\.pU7\] always \$increment\(main\.unpacked2\) == -1: PROVED up to bound 0$
+^\[main\.pU8\] always \$increment\(main\.unpacked3\) == 1: PROVED up to bound 0$
 ^EXIT=0$
 ^SIGNAL=0$
 --

src/verilog/expr2verilog.cpp

@@ -647,6 +647,81 @@ std::string expr2verilogt::convert_index(
 
 /*******************************************************************\
 
+Function: expr2verilogt::convert_non_indexed_part_select
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+std::string expr2verilogt::convert_non_indexed_part_select(
+  const verilog_non_indexed_part_select_exprt &src,
+  verilog_precedencet precedence)
+{
+  verilog_precedencet p;
+  std::string op = convert(src.src(), p);
+
+  std::string dest;
+  if(precedence > p)
+    dest += '(';
+  dest += op;
+  if(precedence > p)
+    dest += ')';
+
+  dest += '[';
+  dest += convert(src.msb());
+  dest += ':';
+  dest += convert(src.lsb());
+  dest += ']';
+
+  return dest;
+}
+
+/*******************************************************************\
+
+Function: expr2verilogt::convert_indexed_part_select
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+std::string expr2verilogt::convert_indexed_part_select(
+  const verilog_indexed_part_select_plus_or_minus_exprt &src,
+  verilog_precedencet precedence)
+{
+  verilog_precedencet p;
+  std::string op = convert(src.src(), p);
+
+  std::string dest;
+  if(precedence > p)
+    dest += '(';
+  dest += op;
+  if(precedence > p)
+    dest += ')';
+
+  dest += '[';
+  dest += convert(src.index());
+
+  if(src.id() == ID_verilog_indexed_part_select_plus)
+    dest += '+';
+  else
+    dest += '-';
+
+  dest += convert(src.width());
+  dest += ']';
+
+  return dest;
+}
+
+/*******************************************************************\
+
 Function: expr2verilogt::convert_extractbit
 
   Inputs:
@@ -842,6 +917,26 @@ std::string expr2verilogt::convert_next_symbol(
 
 /*******************************************************************\
 
+Function: expr2verilogt::convert_hierarchical_identifier
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+std::string expr2verilogt::convert_hierarchical_identifier(
+  const hierarchical_identifier_exprt &src,
+  verilog_precedencet &precedence)
+{
+  precedence = verilog_precedencet::MAX;
+  return convert(src.module()) + '.' + src.item().get_string(ID_base_name);
+}
+
+/*******************************************************************\
+
 Function: expr2verilogt::convert_constant
 
   Inputs:
@@ -1048,6 +1143,20 @@ expr2verilogt::convert(const exprt &src, verilog_precedencet &precedence)
     return convert_index(
       to_index_expr(src), precedence = verilog_precedencet::MEMBER);
 
+  else if(
+    src.id() == ID_verilog_indexed_part_select_plus ||
+    src.id() == ID_verilog_indexed_part_select_minus)
+  {
+    return convert_indexed_part_select(
+      to_verilog_indexed_part_select_plus_or_minus_expr(src),
+      precedence = verilog_precedencet::MEMBER);
+  }
+
+  else if(src.id() == ID_verilog_non_indexed_part_select)
+    return convert_non_indexed_part_select(
+      to_verilog_non_indexed_part_select_expr(src),
+      precedence = verilog_precedencet::MEMBER);
+
   else if(src.id()==ID_extractbit)
     return convert_extractbit(
       to_extractbit_expr(src), precedence = verilog_precedencet::MEMBER);
@@ -1195,6 +1304,10 @@ expr2verilogt::convert(const exprt &src, verilog_precedencet &precedence)
   else if(src.id()==ID_next_symbol)
     return convert_next_symbol(src, precedence);
 
+  else if(src.id() == ID_hierarchical_identifier)
+    return convert_hierarchical_identifier(
+      to_hierarchical_identifier_expr(src), precedence);
+
   else if(src.id()==ID_constant)
     return convert_constant(to_constant_expr(src), precedence);
 

src/verilog/expr2verilog_class.h

@@ -86,6 +86,10 @@ class expr2verilogt
 
   virtual std::string convert_symbol(const exprt &src, verilog_precedencet &);
 
+  std::string convert_hierarchical_identifier(
+    const class hierarchical_identifier_exprt &,
+    verilog_precedencet &precedence);
+
   virtual std::string
   convert_nondet_symbol(const exprt &src, verilog_precedencet &);
 
@@ -135,6 +139,14 @@ class expr2verilogt
 
   virtual std::string convert_function_call(const class function_call_exprt &);
 
+  std::string convert_non_indexed_part_select(
+    const class verilog_non_indexed_part_select_exprt &,
+    verilog_precedencet precedence);
+
+  std::string convert_indexed_part_select(
+    const class verilog_indexed_part_select_plus_or_minus_exprt &,
+    verilog_precedencet precedence);
+
 protected:
   const namespacet &ns;
 };

src/verilog/verilog_synthesis.cpp

@@ -2271,6 +2271,39 @@ void verilog_synthesist::synth_assert_assume_cover(
   // but this is to be checked.
   // Arguments to procedural concurrent assertions are complex
   // (1800-2017 16.14.6.1)
+  {
+    exprt cond_for_comment = statement.condition();
+
+    // Are we in an initial or always block?
+    if(construct != constructt::INITIAL)
+    {
+      // one of the 'always' variants -- assertions and assumptions have an implicit 'always'
+      if(
+        statement.id() != ID_verilog_cover_property &&
+        statement.id() != ID_verilog_immediate_cover)
+      {
+        if(cond_for_comment.id() != ID_sva_always)
+          cond_for_comment = sva_always_exprt(cond_for_comment);
+      }
+    }
+
+    // mark 'assume' and 'cover' properties as such
+    if(
+      statement.id() == ID_verilog_assume_property ||
+      statement.id() == ID_verilog_immediate_assume ||
+      statement.id() == ID_verilog_smv_assume)
+    {
+      cond_for_comment = sva_assume_exprt(cond_for_comment);
+    }
+    else if(statement.id() == ID_verilog_cover_property)
+    {
+      // 'cover' properties are existential
+      cond_for_comment = sva_cover_exprt(cond_for_comment);
+    }
+
+    symbol.location.set_comment(to_string(cond_for_comment));
+  }
+
   exprt cond;
 
   // Are we in an initial or always block?
@@ -2323,8 +2356,6 @@ void verilog_synthesist::synth_assert_assume_cover(
     cond = sva_cover_exprt(cond);
   }
 
-  symbol.location.set_comment(to_string(cond));
-
   symbol.value = std::move(cond);
 }
 
@@ -2347,6 +2378,27 @@ void verilog_synthesist::synth_assert_assume_cover(
   const irep_idt &identifier = module_item.identifier();
   symbolt &symbol=symbol_table_lookup(identifier);
 
+  {
+    exprt cond_for_comment = module_item.condition();
+
+    if(
+      module_item.id() == ID_verilog_assert_property ||
+      module_item.id() == ID_verilog_assume_property)
+    {
+      // Concurrent assertions and assumptions come with an implicit 'always'
+      // (1800-2017 Sec 16.12.11).
+      if(cond_for_comment.id() != ID_sva_always)
+        cond_for_comment = sva_always_exprt{cond_for_comment};
+    }
+    else if(module_item.id() == ID_verilog_cover_property)
+    {
+      // 'cover' requirements are existential.
+      cond_for_comment = sva_cover_exprt{cond_for_comment};
+    }
+
+    symbol.location.set_comment(to_string(cond_for_comment));
+  }
+
   construct=constructt::OTHER;
 
   auto cond = synth_expr(module_item.condition(), symbol_statet::SYMBOL);
@@ -2376,8 +2428,6 @@ void verilog_synthesist::synth_assert_assume_cover(
   else
     PRECONDITION(false);
 
-  symbol.location.set_comment(to_string(cond));
-
   symbol.value = std::move(cond);
 }