Verilog: implement xnor gates

regression/verilog/primitive_gates/xnor1.desc

@@ -0,0 +1,11 @@
+CORE broken-smt-backend
+xnor1.sv
+--bound 0
+^\[main\.xnor_ok\] always !\(xor\(xor\(main\.xnor_in1, main\.xnor_in2\), main\.xnor_in3\)\) == main\.xnor_out: PROVED up to bound 0$
+^\[main\.xnor_fail\] always main\.xnor_in1 == main\.xnor_in2 == main\.xnor_in3 == main\.xnor_out: REFUTED$
+^\[main\.xnor_is_reduction_xnor\] always ~\^\{ main\.xnor_in1, main\.xnor_in2, main\.xnor_in3 \} == main\.xnor_out: PROVED up to bound 0$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/primitive_gates/xnor1.sv

@@ -0,0 +1,61 @@
+module main(output xnor_out, input xnor_in1, xnor_in2, xnor_in3);
+
+  // An 'xnor' with three inputs.
+  // 1800-2017 28.4 says that these "shall have a natural extension".
+  xnor x1(xnor_out, xnor_in1, xnor_in2, xnor_in3);
+
+  // should pass
+  `ifndef __ICARUS__
+  xnor_ok: assert final (!(xnor_in1 ^ xnor_in2 ^ xnor_in3)==xnor_out);
+  `endif
+
+  // should fail -- not the same as using a chain of binary xnors
+  `ifndef __ICARUS__
+  xnor_fail: assert final ((xnor_in1 ~^ xnor_in2 ~^ xnor_in3)==xnor_out);
+  `endif
+
+  // should pass -- xnor is the same as reduction xnor
+  `ifndef __ICARUS__
+  xnor_is_reduction_xnor: assert final (~^{xnor_in1, xnor_in2, xnor_in3}==xnor_out);
+  `endif
+
+endmodule
+
+// To check simulator behavior
+module xnor_tb;
+
+  wire xnor_out;
+  reg xnor_in1, xnor_in2, xnor_in3;
+
+  main m(xnor_out, xnor_in1, xnor_in2, xnor_in3);
+
+  task print;
+    begin
+      $display("input: ", xnor_in1, xnor_in2, xnor_in3);
+      $display("  xnor gate:      ", xnor_out);
+      $display("  reduction-xnor: ", ~^{xnor_in1, xnor_in2, xnor_in3});
+      $display("  !reduction-xor: ", !(^{xnor_in1, xnor_in2, xnor_in3}));
+      $display("  !xor:           ", !(xnor_in1 ^ xnor_in2 ^ xnor_in3));
+      $display("  binary xnors:   ", xnor_in1 ~^ xnor_in2 ~^ xnor_in3);
+    end
+  endtask
+
+  initial begin
+    {xnor_in1, xnor_in2, xnor_in3} = 'b000;
+    #1;
+    print();
+    {xnor_in1, xnor_in2, xnor_in3} = 'b100;
+    #1;
+    print();
+    {xnor_in1, xnor_in2, xnor_in3} = 'b110;
+    #1;
+    print();
+    {xnor_in1, xnor_in2, xnor_in3} = 'b111;
+    #1;
+    print();
+    {xnor_in1, xnor_in2, xnor_in3} = 'b101;
+    #1;
+    print();
+  end
+
+endmodule

regression/verilog/primitive_gates/xnor2.desc

@@ -0,0 +1,10 @@
+CORE broken-smt-backend
+xnor2.sv
+--bound 0
+^\[main\.xnor_ok\] always !main\.xnor_in1 == main\.xnor_out: PROVED up to bound 0$
+^\[main\.xnor_is_reduction_xnor\] always ~\^\{ main\.xnor_in1 \} == main\.xnor_out: PROVED up to bound 0$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/primitive_gates/xnor2.sv

@@ -0,0 +1,45 @@
+module main(output xnor_out, input xnor_in1);
+
+  // An 'xnor' with just one input.  These negate.
+  xnor x1(xnor_out, xnor_in1);
+
+  // should pass
+  `ifndef __ICARUS__
+  xnor_ok: assert final (!xnor_in1==xnor_out);
+  `endif
+
+  // should pass -- xnor is the same as reduction xnor
+  `ifndef __ICARUS__
+  xnor_is_reduction_xnor: assert final (~^{xnor_in1}==xnor_out);
+  `endif
+
+endmodule
+
+// To check simulator behavior
+module xnor_tb;
+
+  wire xnor_out;
+  reg xnor_in1;
+
+  main m(xnor_out, xnor_in1);
+
+  task print;
+    begin
+      $display("input: ", xnor_in1);
+      $display("  xnor gate:      ", xnor_out);
+      $display("  reduction-xnor: ", ~^{xnor_in1});
+      $display("  !reduction-xor: ", !(^{xnor_in1}));
+      $display("  !:              ", !xnor_in1);
+    end
+  endtask
+
+  initial begin
+    {xnor_in1} = 'b0;
+    #1;
+    print();
+    {xnor_in1} = 'b1;
+    #1;
+    print();
+  end
+
+endmodule

regression/verilog/primitive_gates/xnor3.desc

@@ -0,0 +1,9 @@
+CORE broken-smt-backend
+xnor3.sv
+--bound 0
+^\[main\.xnor_ok\] always main\.xnor_in1 ~\^ main\.xnor_in2 == main\.xnor_out: PROVED up to bound 0$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/primitive_gates/xnor3.sv

@@ -0,0 +1,11 @@
+module main(output [31:0] xnor_out, input [31:0] xnor_in1, xnor_in2);
+
+  // An 'xnor' with two inputs, 32 bits each.
+  xnor x1[31:0](xnor_out, xnor_in1, xnor_in2);
+
+  // should pass
+  `ifndef __ICARUS__
+  xnor_ok: assert final (xnor_in1 ~^ xnor_in2==xnor_out);
+  `endif
+
+endmodule

src/verilog/parser.y

@@ -2724,7 +2724,7 @@ n_input_gatetype:
 	| TOK_NAND     { init($$, ID_nand); }
         | TOK_NOR      { init($$, ID_nor); }
         | TOK_OR       { init($$, ID_or); }
-	| TOK_XNOR     { init($$, ID_nor); }
+	| TOK_XNOR     { init($$, ID_xnor); }
         | TOK_XOR      { init($$, ID_xor); }
 	;
 

src/verilog/verilog_synthesis.cpp

@@ -1516,12 +1516,9 @@ void verilog_synthesist::synth_module_instance_builtin(
       assert(trans.operands().size()==3);
       trans.invar().add_to_operands(std::move(constraint));
     }
-    else if(module==ID_and ||
-            module==ID_nand ||
-            module==ID_or ||
-            module==ID_nor ||
-            module==ID_xor ||
-            module==ID_xnor)
+    else if(
+      module == ID_and || module == ID_nand || module == ID_or ||
+      module == ID_nor || module == ID_xor)
     {
       // 1800-2017 28.4 and, nand, nor, or, xor, and xnor gates
       DATA_INVARIANT(
@@ -1549,6 +1546,41 @@ void verilog_synthesist::synth_module_instance_builtin(
       equal_exprt constraint{output, op};
       trans.invar().add_to_operands(std::move(constraint));
     }
+    else if(module == ID_xnor)
+    {
+      // Our solver does not have ID_xnor, hence use the negation of ID_xor
+      // ID_bitxor.
+      // With one operand, or with more than three operands, the result is
+      // ambiguous. The semantics of bitxnor do not match when using one
+      // or more than two operands.
+      DATA_INVARIANT(
+        instance.connections().size() >= 2,
+        "binary primitive gates should have at least two connections");
+
+      // One output, one or more inputs.
+      auto &connections = instance.connections();
+      auto &output = connections[0];
+
+      exprt::operandst operands;
+
+      // iterate over the module inputs
+      for(std::size_t i = 1; i < connections.size(); i++)
+      {
+        operands.push_back(connections[i]);
+      }
+
+      exprt op;
+
+      if(instance.type().id() == ID_bool)
+        op = not_exprt{
+          multi_ary_exprt{ID_xor, std::move(operands), instance.type()}};
+      else
+        op = bitnot_exprt{
+          multi_ary_exprt{ID_bitxor, std::move(operands), instance.type()}};
+
+      equal_exprt constraint{output, std::move(op)};
+      trans.invar().add_to_operands(std::move(constraint));
+    }
     else if(module==ID_buf)
     {
       assert(instance.connections().size() >= 2);