Merge pull request #315 from diffblue/fix-functioncall5

do not add constraints for assignments to function-local variables

Author: kroening

regression/verilog/functioncall/functioncall5.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 functioncall5.v
 --module main --bound 0
 ^EXIT=0$

regression/verilog/functioncall/functioncall5.v

@@ -17,7 +17,9 @@ module main(input clk);
 
   reg my_reg;
 
-  always @(posedge clk)
+  always @(posedge clk) begin
     my_reg = isUpper(my_wire1);
+    assert (my_reg == my_wire2);
+  end
 
 endmodule

regression/verilog/functioncall/functioncall7.desc

@@ -0,0 +1,8 @@
+CORE
+functioncall7.v
+--module main --bound 0
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/functioncall/functioncall7.v

@@ -0,0 +1,18 @@
+module main(input clk);
+
+  function negate;
+  input in;
+  begin
+      negate = ~in;
+  end
+  endfunction
+
+  // same function used twice
+
+  wire my_wire0 = negate(0);
+  wire my_wire1 = negate(1);
+
+  always assert p0: (my_wire0 == 1);
+  always assert p1: (my_wire1 == 0);
+
+endmodule

src/verilog/verilog_synthesis.cpp

@@ -76,8 +76,7 @@ exprt verilog_synthesist::synth_expr(exprt expr, symbol_statet symbol_state)
   }
   else if(expr.id()==ID_function_call)
   {
-    expand_function_call(to_function_call_expr(expr));
-    return expr;
+    return expand_function_call(to_function_call_expr(expr));
   }
   else if(expr.id()==ID_hierarchical_identifier)
   {
@@ -112,6 +111,32 @@ exprt verilog_synthesist::synth_expr(exprt expr, symbol_statet symbol_state)
 
 /*******************************************************************\
 
+Function: verilog_synthesist::function_locality
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void verilog_synthesist::function_locality(const symbolt &function_symbol)
+{
+  // Find all local symbols of the function, mark their
+  // assignments as local.
+  auto prefix = id2string(function_symbol.name) + '.';
+  for(auto &symbol : symbol_table.symbols)
+  {
+    if(irep_idt(symbol.first).starts_with(prefix))
+    {
+      assignments[symbol.first].is_cycle_local = true;
+    }
+  }
+}
+
+/*******************************************************************\
+
 Function: verilog_synthesist::expand_function_call
 
   Inputs:
@@ -122,7 +147,7 @@ Function: verilog_synthesist::expand_function_call
 
 \*******************************************************************/
 
-void verilog_synthesist::expand_function_call(function_call_exprt &call)
+exprt verilog_synthesist::expand_function_call(const function_call_exprt &call)
 {
   // Is it a 'system function call'?
   if(call.is_system_function_call())
@@ -138,8 +163,7 @@ void verilog_synthesist::expand_function_call(function_call_exprt &call)
       throw 0;
     }
 
-    call.swap(result);
-    return;
+    return result;
   }
 
   // check some restrictions
@@ -184,7 +208,10 @@ void verilog_synthesist::expand_function_call(function_call_exprt &call)
     error() << "wrong number of arguments" << eom;
     throw 0;
   }
-  
+
+  // preserve locality of function-local variables
+  function_locality(symbol);
+
   // do assignments to function parameters
   for(unsigned i=0; i<parameters.size(); i++)
   {
@@ -197,15 +224,16 @@ void verilog_synthesist::expand_function_call(function_call_exprt &call)
   }
 
   synth_statement(to_verilog_statement(symbol.value));
-  
+
   // replace function call by return value symbol
   const symbolt &return_symbol=
     ns.lookup(id2string(symbol.name)+"."+
               id2string(symbol.base_name));
 
-  exprt return_value=return_symbol.symbol_expr();
+  // get the current value
+  auto result = synth_expr(return_symbol.symbol_expr(), symbol_statet::CURRENT);
 
-  call.swap(return_value);
+  return result;
 }
 
 /*******************************************************************\
@@ -362,22 +390,27 @@ void verilog_synthesist::assignment_rec(
 
     assignmentt &assignment=assignments[symbol.name];
 
-    if(assignment.type==event_guardt::NONE)
-      assignment.type=new_type;
-    else if(assignment.type!=new_type)
+    if(assignment.is_cycle_local)
     {
-      error().source_location=lhs.source_location();
-      error() << "conflicting assignment types for `"
-              << symbol.base_name
-              << "' (new: "
-              << as_string(new_type) << ", old: "
-              << as_string(assignment.type) << ")" << eom;
-      throw 0;      
     }
-    
-    membert member;
-    assignment_member_rec(lhs, member,
-      (construct==constructt::INITIAL)?assignment.init:assignment.next);
+    else
+    {
+      if(assignment.type == event_guardt::NONE)
+        assignment.type = new_type;
+      else if(assignment.type != new_type)
+      {
+        throw errort().with_location(lhs.source_location())
+          << "conflicting assignment types for `" << symbol.base_name
+          << "' (new: " << as_string(new_type)
+          << ", old: " << as_string(assignment.type) << ")";
+      }
+
+      membert member;
+      assignment_member_rec(
+        lhs,
+        member,
+        (construct == constructt::INITIAL) ? assignment.init : assignment.next);
+    }
   }
 
   {
@@ -2764,6 +2797,9 @@ void verilog_synthesist::synth_assignments(transt &trans)
     {
       assignmentt &assignment=assignments[symbol.name];
 
+      if(assignment.is_cycle_local)
+        continue; // ignore
+
       if(assignment.type==event_guardt::COMBINATIONAL)
       {
         warning().source_location = symbol.location;

src/verilog/verilog_synthesis_class.h

@@ -111,6 +111,7 @@ class verilog_synthesist:
 
     // only relevant for 'next'
     event_guardt type;
+    bool is_cycle_local = false;
 
     assignmentt():type(event_guardt::NONE)
     {
@@ -277,8 +278,8 @@ class verilog_synthesist:
     class hierarchical_identifier_exprt &expr,
     symbol_statet symbol_state);
 
-  void expand_function_call(class function_call_exprt &call);
-  
+  exprt expand_function_call(const class function_call_exprt &call);
+
   typedef std::map<irep_idt, exprt> replace_mapt;
 
   void instantiate_ports(
@@ -299,7 +300,11 @@ class verilog_synthesist:
     transt &);
 
   void replace_by_wire(exprt &expr, const symbolt &base);
-  
+
+  // Mark the local variables of a function or task
+  // as cycle local.
+  void function_locality(const symbolt &);
+
   unsigned temporary_counter;
 };