Verilog: fix synthesis for continuous assignments to state variables

SystemVerilog allows continous assignments to variables.  These are now
added to the assignments data structure.

Fixes issue #635.

Author: kroening

regression/verilog/synthesis/continuous_assignment_to_variable_systemverilog2.desc

@@ -1,9 +1,8 @@
-KNOWNBUG
+CORE
 continuous_assignment_to_variable_systemverilog2.sv
 --bound 1
 ^\[main\.cover1\] cover 1: PROVED$
 ^EXIT=0$
 ^SIGNAL=0$
 --
 --
-This creates inconsistent constraints, which yields UNSAT.

src/verilog/verilog_synthesis.cpp

@@ -2389,23 +2389,40 @@ void verilog_synthesist::synth_force_rec(
   }
 
   // get symbol
-
   const symbolt &symbol=assignment_symbol(lhs);
 
+  // turn into combinational assignment
   assignmentt &assignment=assignments[symbol.name];
 
   if(assignment.type==event_guardt::NONE)
+  {
     assignment.type=event_guardt::COMBINATIONAL;
-  else if(assignment.type!=event_guardt::COMBINATIONAL)
+  }
+  else if(assignment.type == event_guardt::CLOCK)
   {
     throw errort().with_location(lhs.source_location())
-      << "variable is clocked";
+      << "variable " << symbol.display_name() << " is clocked";
+  }
+  else if(assignment.type == event_guardt::COMBINATIONAL)
+  {
+    // leave as is
   }
+  else
+    DATA_INVARIANT(false, "unexpected assignment type");
 
-  auto rhs_synth = synth_expr(rhs, symbol_statet::CURRENT);  
+  auto rhs_synth = synth_expr(rhs, symbol_statet::CURRENT);
 
-  equal_exprt equality(lhs, rhs_synth);
-  invars.push_back(equality);
+  // If it's a variable, synth_assignments will
+  // generate the constraint.
+  if(symbol.is_state_var)
+  {
+    assignment.next.value = rhs_synth;
+  }
+  else
+  {
+    equal_exprt equality(lhs, rhs_synth);
+    invars.push_back(equality);
+  }
 }
 
 /*******************************************************************\
@@ -3642,7 +3659,7 @@ void verilog_synthesist::synth_assignments(transt &trans)
       }
     }
   }
-  
+
   for(const auto & it : new_wires)
   {
     symbolt &symbol=symbol_table_lookup(it);
@@ -3725,7 +3742,7 @@ exprt verilog_synthesist::current_value(
     {
       return symbol_expr(symbol, CURRENT);
     }
-    else
+    else if(construct == constructt::INITIAL)
     {
       // Initial state computation, i.e., this is a value _before_ the
       // initial state  -- make it non-deterministic
@@ -3734,6 +3751,10 @@ exprt verilog_synthesist::current_value(
       result.set("initial_value", true);
       return result;
     }
+    else
+    {
+      DATA_INVARIANT(false, "unexpected assignment construct");
+    }
   }
 }