Merge pull request #420 from diffblue/verilog-final

Verilog: parse the `final` construct

Author: tautschnig

regression/verilog/final-procedures/final1.desc

@@ -0,0 +1,7 @@
+CORE
+final1.sv
+
+^no properties$
+^EXIT=10$
+^SIGNAL=0$
+--

regression/verilog/final-procedures/final1.sv

@@ -0,0 +1,6 @@
+module main;
+
+  // no synthesis semantics at all
+  final $display("Final time: %d", $time);
+
+endmodule

src/hw_cbmc_irep_ids.h

@@ -68,6 +68,7 @@ IREP_ID_ONE(continuous_assign)
 IREP_ID_ONE(wait)
 IREP_ID_ONE(always)
 IREP_ID_ONE(named_port_connection)
+IREP_ID_ONE(verilog_final)
 IREP_ID_ONE(initial)
 IREP_ID_ONE(verilog_label_statement)
 IREP_ID_ONE(disable)

src/verilog/parser.y

@@ -861,6 +861,7 @@ module_common_item:
         | bind_directive
 	| continuous_assign
 	| initial_construct
+	| final_construct
 	| always_construct
 	| loop_generate_construct
 	| conditional_generate_construct
@@ -2511,6 +2512,10 @@ always_keyword:
 	| TOK_ALWAYS_FF    { init($$, ID_always); }
 	;
 
+final_construct: TOK_FINAL function_statement
+		{ init($$, ID_verilog_final); mto($$, $2); }
+	;
+
 blocking_assignment:
 	  variable_lvalue '=' delay_or_event_control expression
 		{ init($$, ID_blocking_assign); mto($$, $1); mto($$, $4); }
@@ -2696,6 +2701,9 @@ statement_item:
 	| procedural_assertion_statement
 	;
 
+function_statement: statement
+	;
+
 system_task_name: TOK_SYSIDENT
                 { new_symbol($$, $1); }
         ;

src/verilog/verilog_elaborate.cpp

@@ -764,6 +764,9 @@ void verilog_typecheckt::collect_symbols(
   {
     collect_symbols(to_verilog_set_genvars(module_item).module_item());
   }
+  else if(module_item.id() == ID_verilog_final)
+  {
+  }
   else if(module_item.id() == ID_verilog_let)
   {
     collect_symbols(to_verilog_let(module_item));

src/verilog/verilog_interfaces.cpp

@@ -270,6 +270,9 @@ void verilog_typecheckt::interface_module_item(
   {
     // does not yield symbol
   }
+  else if(module_item.id() == ID_verilog_final)
+  {
+  }
   else if(module_item.id() == ID_verilog_let)
   {
     // already done during constant elaboration

src/verilog/verilog_synthesis.cpp

@@ -2625,6 +2625,10 @@ void verilog_synthesist::synth_module_item(
   {
     // ignore for now
   }
+  else if(module_item.id() == ID_verilog_final)
+  {
+    // no synthesis semantics
+  }
   else if(module_item.id() == ID_verilog_let)
   {
     // done already

src/verilog/verilog_typecheck.cpp

@@ -1625,6 +1625,9 @@ void verilog_typecheckt::convert_module_item(
     module_item.swap(tmp);
     convert_module_item(module_item);
   }
+  else if(module_item.id() == ID_verilog_final)
+  {
+  }
   else if(module_item.id() == ID_verilog_let)
   {
     // done already