Veriog: synthesis of primitive not gates

For a primitive not gate with input i and output o, this now generates the constraint

  i = !o

as opposed to

  !i = o

While logically equivalent, the new constraint is easier to read, and
enables the generation of netlists that are more compact.

Author: kroening

regression/verilog/primitive_gates/not1.desc

@@ -0,0 +1,7 @@
+CORE
+not1.sv
+--bound 0
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/verilog/primitive_gates/not1.sv

@@ -0,0 +1,11 @@
+module main(input not_in);
+
+  wire not_out1, not_out2;
+
+  not not_gate(not_out1, not_out2, not_in);
+
+  // should pass
+  not_out1_ok: assert final (not_out1 == !not_in);
+  not_out2_ok: assert final (not_out2 == !not_in);
+
+endmodule

src/verilog/verilog_synthesis.cpp

@@ -1586,17 +1586,21 @@ void verilog_synthesist::synth_module_instance_builtin(
     {
       assert(instance.connections().size() >= 2);
 
-      for(unsigned i = 0; i < instance.connections().size() - 1; i++)
-      {
-        exprt op(ID_not, instance.type());
-        op.add_to_operands(instance.connections()[i]);
+      // May have multiple outputs. The input is the last connection.
+      auto &input = instance.connections().back();
+      exprt rhs;
 
-        if(instance.type().id()!=ID_bool)
-          op.id("bit"+op.id_string());
+      if(input.type().id() == ID_bool)
+        rhs = not_exprt{input};
+      else
+        rhs = bitnot_exprt{input};
 
-        equal_exprt constraint{op, instance.connections().back()};
+      rhs.add_source_location() = module_item.source_location();
 
-        assert(trans.operands().size()==3);
+      for(std::size_t i = 0; i < instance.connections().size() - 1; i++)
+      {
+        auto &lhs = instance.connections()[i];
+        auto constraint = equal_exprt{lhs, rhs};
         trans.invar().add_to_operands(std::move(constraint));
       }
     }