Merge pull request #300 from diffblue/verilog-let

Verilog: let

regression/verilog/let/let1.desc

@@ -0,0 +1,7 @@
+CORE
+let1.sv
+--bound 0
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/verilog/let/let1.sv

@@ -0,0 +1,20 @@
+// The "let construct" was introduced by SystemVerilog 1800-2009.
+
+module main;
+
+  let some_let = 8'd123;
+  p0: assert property (some_let == 123 && $bits(some_let) == 8);
+
+  // The standard doesn't say, but we allow these to be elaboration-time
+  // constants.
+  parameter some_parameter = some_let;
+
+  p1: assert property (some_parameter == 123 && $bits(some_parameter) == 8);
+
+  // May depend on state.
+  wire some_wire;
+  let some_let_eq_wire = some_wire;
+
+  p2: assert property (some_let_eq_wire == some_wire);
+
+endmodule

regression/verilog/let/let_ports1.desc

@@ -0,0 +1,8 @@
+CORE
+let_ports1.sv
+--bound 0
+^file .* line 5: let ports not supported yet$
+^EXIT=2$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/verilog/let/let_ports1.sv

@@ -0,0 +1,8 @@
+// The "let construct" was introduced by SystemVerilog 1800-2009.
+
+module main;
+
+  let some_let_with_port(x) = x + 1;
+  p0: assert property (some_let_with_port(1) == 2);
+
+endmodule

src/hw_cbmc_irep_ids.h

@@ -114,6 +114,8 @@ IREP_ID_ONE(trireg)
 IREP_ID_ONE(local_parameter_decl)
 IREP_ID_ONE(parameter_decl)
 IREP_ID_ONE(set_genvars)
+IREP_ID_ONE(verilog_let)
+IREP_ID_ONE(verilog_untyped)
 IREP_ID_ONE(verilog_genvar)
 IREP_ID_ONE(verilog_shortreal)
 IREP_ID_ONE(verilog_real)

src/verilog/parser.y

@@ -1057,6 +1057,11 @@ package_or_generate_item_declaration:
 	| class_declaration
 	| local_parameter_declaration ';'
 	| parameter_declaration ';'
+	  /* The following rule is not in the standard.
+	     However, Section 11.12 explicitly states
+	     that let constructs may be declared in a
+	     module/interface/program/checker etc. */
+	| let_declaration
         ;
 
 // System Verilog standard 1800-2017
@@ -1897,6 +1902,7 @@ block_item_declaration:
 	  attribute_instance_brace data_declaration { $$=$2; }
 	| attribute_instance_brace local_parameter_declaration ';' { $$=$2; }
 	| attribute_instance_brace parameter_declaration ';' { $$=$2; }
+	| attribute_instance_brace let_declaration { $$=$2; }
 	;
 
 // System Verilog standard 1800-2017
@@ -2014,6 +2020,59 @@ expression_or_dist:
 	  expression
 	;
 
+// System Verilog standard 1800-2017
+// A.2.12 Let declarations
+
+let_declaration:
+	  TOK_LET let_identifier let_port_list_paren_opt '=' expression ';'
+		{
+		  init($$, ID_verilog_let);
+		  // These have one declarator exactly.
+		  stack_expr($2).id(ID_declarator);
+		  addswap($2, ID_type, $3);
+		  addswap($2, ID_value, $5);
+		  mto($$, $2);
+		}
+	;
+
+let_identifier: identifier;
+
+let_port_list_paren_opt:
+	  /* Optional */
+		{ init($$, ID_nil); }
+	| '(' let_port_list_opt ')'
+		{ $$ = $2; }
+	;
+
+let_port_list_opt:
+	  /* Optional */
+		{ init($$, ID_nil); }
+	| let_port_list
+	;
+
+let_port_list:
+	  let_port_item
+		{ init($$); mts($$, $1); }
+	| let_port_list ',' let_port_item
+		{ $$ = $1; mts($$, $3); }
+	;
+
+let_port_item:
+	  attribute_instance_brace let_formal_type formal_port_identifier
+	  variable_dimension_brace let_port_initializer_opt
+	;
+
+let_port_initializer_opt:
+	  /* Optional */
+	| '=' expression
+	;
+
+let_formal_type:
+	  data_type_or_implicit
+	| TOK_UNTYPED
+		{ init($$, ID_verilog_untyped); }
+	;
+
 // System Verilog standard 1800-2017
 // A.3.1 Primitive instantiation and instances
 
@@ -3236,6 +3295,8 @@ class_identifier: TOK_NON_TYPE_IDENTIFIER;
 
 constraint_identifier: TOK_NON_TYPE_IDENTIFIER;
 
+formal_port_identifier: identifier;
+
 genvar_identifier: identifier;
 
 hierarchical_parameter_identifier: hierarchical_identifier

src/verilog/verilog_elaborate.cpp

@@ -592,6 +592,39 @@ void verilog_typecheckt::collect_symbols(const verilog_declt &decl)
   }
 }
 
+#include <iostream>
+
+void verilog_typecheckt::collect_symbols(const verilog_lett &let)
+{
+  // These have one declarator.
+  auto &declarator = let.declarator();
+
+  // We don't currently do let ports
+  if(declarator.type().is_not_nil())
+  {
+    throw errort().with_location(let.source_location())
+      << "let ports not supported yet";
+  }
+
+  const irep_idt &base_name = declarator.base_name();
+  irep_idt identifier = hierarchical_identifier(base_name);
+
+  // The range type is always derived from the type of the
+  // value expression.
+  auto type = to_be_elaborated_typet(derive_from_value_typet());
+
+  // add the symbol
+  symbolt new_symbol(identifier, type, mode);
+
+  new_symbol.module = module_identifier;
+  new_symbol.is_macro = true;
+  new_symbol.value = declarator.value();
+  new_symbol.base_name = base_name;
+  new_symbol.pretty_name = strip_verilog_prefix(new_symbol.name);
+
+  add_symbol(std::move(new_symbol));
+}
+
 void verilog_typecheckt::collect_symbols(const verilog_statementt &statement)
 {
   if(statement.id() == ID_assert || statement.id() == ID_assume)
@@ -729,6 +762,10 @@ void verilog_typecheckt::collect_symbols(
   {
     collect_symbols(to_verilog_set_genvars(module_item).module_item());
   }
+  else if(module_item.id() == ID_verilog_let)
+  {
+    collect_symbols(to_verilog_let(module_item));
+  }
   else
     DATA_INVARIANT(false, "unexpected module item: " + module_item.id_string());
 }

src/verilog/verilog_expr.h

@@ -512,6 +512,32 @@ to_verilog_local_parameter_decl(irept &irep)
   return static_cast<verilog_local_parameter_declt &>(irep);
 }
 
+class verilog_lett : public verilog_module_itemt
+{
+public:
+  // These have a single declarator.
+  using declaratort = verilog_parameter_declt::declaratort;
+
+  const declaratort &declarator() const
+  {
+    return static_cast<const declaratort &>(op0());
+  }
+};
+
+inline const verilog_lett &to_verilog_let(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_verilog_let);
+  validate_operands(expr, 1, "verilog_let must have 1 operand");
+  return static_cast<const verilog_lett &>(expr);
+}
+
+inline verilog_lett &to_verilog_let(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_verilog_let);
+  validate_operands(expr, 1, "verilog_let must have 1 operand");
+  return static_cast<verilog_lett &>(expr);
+}
+
 class verilog_inst_baset : public verilog_module_itemt
 {
 public:

src/verilog/verilog_interfaces.cpp

@@ -274,6 +274,10 @@ void verilog_typecheckt::interface_module_item(
   {
     // does not yield symbol
   }
+  else if(module_item.id() == ID_verilog_let)
+  {
+    // already done during constant elaboration
+  }
   else
   {
     DATA_INVARIANT(false, "unexpected module item: " + module_item.id_string());

src/verilog/verilog_synthesis.cpp

@@ -2635,6 +2635,10 @@ void verilog_synthesist::synth_module_item(
   {
     // ignore for now
   }
+  else if(module_item.id() == ID_verilog_let)
+  {
+    // done already
+  }
   else
   {
     throw errort().with_location(module_item.source_location())

src/verilog/verilog_typecheck.cpp

@@ -1551,10 +1551,14 @@ void verilog_typecheckt::convert_module_item(
     module_item.swap(tmp);
     convert_module_item(module_item);
   }
+  else if(module_item.id() == ID_verilog_let)
+  {
+    // done already
+  }
   else
   {
     throw errort().with_location(module_item.source_location())
-      << "unexpected module item:" << module_item.id();
+      << "unexpected module item: " << module_item.id();
   }
 }
 

src/verilog/verilog_typecheck.h

@@ -87,6 +87,7 @@ class verilog_typecheckt:
   void collect_symbols(const verilog_module_sourcet &);
   void collect_symbols(const verilog_module_itemt &);
   void collect_symbols(const verilog_declt &);
+  void collect_symbols(const verilog_lett &);
   void collect_symbols(const verilog_statementt &);
   void
   collect_symbols(const typet &, const verilog_parameter_declt::declaratort &);