Verilog: separate synthesis for LHS expressions

The left-hand side of assignments requires special-case synthesis; the
symbol to be assigned must not be replaced by its value, but any array
indices must be.

Author: kroening

src/verilog/verilog_synthesis.cpp

@@ -405,6 +405,56 @@ exprt verilog_synthesist::synth_expr(exprt expr, symbol_statet symbol_state)
 
 /*******************************************************************\
 
+Function: verilog_synthesist::synth_lhs_expr
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+exprt verilog_synthesist::synth_lhs_expr(exprt expr)
+{
+  if(expr.id() == ID_symbol)
+  {
+    return expr; // leave as is
+  }
+  else if(expr.id() == ID_concatenation)
+  {
+    for(auto &op : expr.operands())
+      op = synth_lhs_expr(op);
+
+    return expr;
+  }
+  else if(expr.id() == ID_verilog_non_indexed_part_select)
+  {
+    auto &part_select = to_verilog_non_indexed_part_select_expr(expr);
+    part_select.src() = synth_lhs_expr(part_select.src());
+    // The indices are expected to be constants.
+    return expr;
+  }
+  else if(
+    expr.id() == ID_verilog_indexed_part_select_plus ||
+    expr.id() == ID_verilog_indexed_part_select_minus)
+  {
+    auto &part_select = to_verilog_indexed_part_select_plus_or_minus_expr(expr);
+    part_select.src() = synth_lhs_expr(part_select.src());
+    // The index need not be a constant, and is _not_ an lhs.
+    part_select.index() =
+      synth_expr(part_select.index(), symbol_statet::CURRENT);
+    return expr;
+  }
+  else
+  {
+    DATA_INVARIANT_WITH_DIAGNOSTICS(
+      false, "unexpected lhs during synthesis", to_string(expr));
+  }
+}
+
+/*******************************************************************\
+
 Function: verilog_synthesist::value_mapt::guarded_expr
 
   Inputs:
@@ -2283,9 +2333,10 @@ void verilog_synthesist::synth_assign(const verilog_assignt &statement)
       << "unexpected assignment statement";
   }
 
-  const exprt &lhs = statement.lhs();
-  exprt rhs = statement.rhs();
+  exprt lhs = statement.lhs();
+  lhs = synth_lhs_expr(lhs);
 
+  exprt rhs = statement.rhs();
   rhs = synth_expr(rhs, symbol_statet::CURRENT);
 
   irep_idt compound_id = irep_idt{};

src/verilog/verilog_synthesis_class.h

@@ -177,7 +177,10 @@ class verilog_synthesist:
 
     exprt guarded_expr(exprt) const;
   };
-   
+
+  // expressions
+  [[nodiscard]] exprt synth_lhs_expr(exprt expr);
+
   exprt current_value(
     const value_mapt::mapt &map,
     const symbolt &symbol,