Merge pull request #579 from diffblue/named_property1

SystemVerilog: named properties

Author: kroening

regression/verilog/SVA/named_property1.desc

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

regression/verilog/SVA/named_property1.sv

@@ -0,0 +1,11 @@
+module main;
+
+  wire [31:0] x = 10;
+
+  property x_is_ten;
+    x == 10
+  endproperty : x_is_ten
+
+  assert property (x_is_ten);
+
+endmodule

src/hw_cbmc_irep_ids.h

@@ -60,6 +60,7 @@ IREP_ID_ONE(verilog_non_indexed_part_select)
 IREP_ID_ONE(verilog_indexed_part_select_plus)
 IREP_ID_ONE(verilog_indexed_part_select_minus)
 IREP_ID_ONE(verilog_past)
+IREP_ID_ONE(verilog_property_declaration)
 IREP_ID_ONE(chandle)
 IREP_ID_ONE(event)
 IREP_ID_ONE(reg)

src/verilog/parser.y

@@ -2039,9 +2039,42 @@ assertion_item_declaration:
 	;
 
 property_declaration:
-          TOK_PROPERTY property_identifier TOK_ENDPROPERTY
+          TOK_PROPERTY property_identifier property_port_list_paren_opt ';'
+          property_spec
+          TOK_ENDPROPERTY property_identifier_opt
+		{ init($$, ID_verilog_property_declaration);
+		  stack_expr($$).set(ID_base_name, stack_expr($2).id());
+		  mto($$, $5); }
         ;
 
+property_identifier_opt:
+	  /* optional */
+	| TOK_COLON property_identifier
+	;
+
+property_port_list_paren_opt:
+	  /* optional */
+	| '(' property_port_list_opt ')'
+	;
+
+property_port_list_opt:
+	  /* optional */
+	| property_port_list
+	;
+
+property_port_list:
+	  property_port_item
+	| property_port_list_opt ',' property_port_item
+	;
+
+property_port_item:
+	  attribute_instance_brace property_formal_type formal_port_identifier variable_dimension_brace
+	;
+
+property_formal_type:
+	  TOK_PROPERTY
+	;
+
 property_spec:
 	  TOK_DISABLE TOK_IFF '(' expression ')' property_expr
 		{ $$=$6; }

src/verilog/verilog_elaborate.cpp

@@ -113,6 +113,11 @@ void verilog_typecheckt::collect_symbols(
   }
 }
 
+void verilog_typecheckt::collect_symbols(
+  const verilog_property_declarationt &declaration)
+{
+}
+
 void verilog_typecheckt::collect_symbols(const typet &type)
 {
   // These types are not yet converted.
@@ -800,6 +805,10 @@ void verilog_typecheckt::collect_symbols(
   else if(module_item.id() == ID_verilog_covergroup)
   {
   }
+  else if(module_item.id() == ID_verilog_property_declaration)
+  {
+    collect_symbols(to_verilog_property_declaration(module_item));
+  }
   else
     DATA_INVARIANT(false, "unexpected module item: " + module_item.id_string());
 }

src/verilog/verilog_expr.h

@@ -2123,4 +2123,37 @@ to_verilog_indexed_part_select_plus_or_minus_expr(exprt &expr)
   return static_cast<verilog_indexed_part_select_plus_or_minus_exprt &>(expr);
 }
 
+class verilog_property_declarationt : public verilog_module_itemt
+{
+public:
+  const irep_idt &base_name() const
+  {
+    return get(ID_base_name);
+  }
+
+  const exprt &cond() const
+  {
+    return op0();
+  }
+
+  exprt &cond()
+  {
+    return op0();
+  }
+};
+
+inline const verilog_property_declarationt &
+to_verilog_property_declaration(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_verilog_property_declaration);
+  return static_cast<const verilog_property_declarationt &>(expr);
+}
+
+inline verilog_property_declarationt &
+to_verilog_property_declaration(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_verilog_property_declaration);
+  return static_cast<verilog_property_declarationt &>(expr);
+}
+
 #endif

src/verilog/verilog_interfaces.cpp

@@ -299,6 +299,9 @@ void verilog_typecheckt::interface_module_item(
   else if(module_item.id() == ID_verilog_covergroup)
   {
   }
+  else if(module_item.id() == ID_verilog_property_declaration)
+  {
+  }
   else
   {
     DATA_INVARIANT(false, "unexpected module item: " + module_item.id_string());

src/verilog/verilog_synthesis.cpp

@@ -3231,6 +3231,9 @@ void verilog_synthesist::synth_module_item(
   else if(module_item.id() == ID_verilog_covergroup)
   {
   }
+  else if(module_item.id() == ID_verilog_property_declaration)
+  {
+  }
   else
   {
     throw errort().with_location(module_item.source_location())

src/verilog/verilog_typecheck.cpp

@@ -1639,6 +1639,10 @@ void verilog_typecheckt::convert_module_item(
   else if(module_item.id() == ID_verilog_covergroup)
   {
   }
+  else if(module_item.id() == ID_verilog_property_declaration)
+  {
+    convert_property_declaration(to_verilog_property_declaration(module_item));
+  }
   else
   {
     throw errort().with_location(module_item.source_location())
@@ -1648,6 +1652,41 @@ void verilog_typecheckt::convert_module_item(
 
 /*******************************************************************\
 
+Function: verilog_typecheckt::convert_property_declaration
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void verilog_typecheckt::convert_property_declaration(
+  verilog_property_declarationt &declaration)
+{
+  auto base_name = declaration.base_name();
+  auto full_identifier = hierarchical_identifier(base_name);
+
+  convert_expr(declaration.cond());
+  make_boolean(declaration.cond());
+
+  auto type = bool_typet{};
+  type.set(ID_C_verilog_type, ID_verilog_property_declaration);
+  symbolt symbol{full_identifier, type, mode};
+
+  symbol.module = module_identifier;
+  symbol.base_name = base_name;
+  symbol.pretty_name = strip_verilog_prefix(symbol.name);
+  symbol.is_macro = true;
+  symbol.value = declaration.cond();
+  symbol.location = declaration.source_location();
+
+  add_symbol(std::move(symbol));
+}
+
+/*******************************************************************\
+
 Function: verilog_typecheckt::convert_statements
 
   Inputs:

src/verilog/verilog_typecheck.h

@@ -92,6 +92,7 @@ class verilog_typecheckt:
   void collect_symbols(const verilog_declt &);
   void collect_symbols(const verilog_lett &);
   void collect_symbols(const verilog_statementt &);
+  void collect_symbols(const verilog_property_declarationt &);
   void
   collect_symbols(const typet &, const verilog_parameter_declt::declaratort &);
   void collect_port_symbols(const verilog_declt &);
@@ -171,6 +172,7 @@ class verilog_typecheckt:
   void convert_assignments(exprt &trans);
   void convert_module_item(class verilog_module_itemt &);
   void convert_parameter_override(const class verilog_parameter_overridet &);
+  void convert_property_declaration(class verilog_property_declarationt &);
 
   void integer_expr(exprt &expr);