do not add constraints for assignments to function-local variables

Assignments to function-local variables are now treated as cycle-local, and
hence neither require invariants nor next-state constraints.

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

@@ -111,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:
@@ -182,7 +208,10 @@ exprt verilog_synthesist::expand_function_call(const 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++)
   {
@@ -195,13 +224,16 @@ exprt verilog_synthesist::expand_function_call(const 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));
 
-  return return_symbol.symbol_expr();
+  // get the current value
+  auto result = synth_expr(return_symbol.symbol_expr(), symbol_statet::CURRENT);
+
+  return result;
 }
 
 /*******************************************************************\
@@ -358,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);
+    }
   }
 
   {
@@ -2760,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)
     {
@@ -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;
 };