Merge pull request #895 from diffblue/xnor-fix

bump CBMC dependency

Author: tautschnig

CHANGELOG

@@ -3,6 +3,7 @@
 * Verilog: bugfix for $onehot0
 * Verilog: fix for primitive gates with more than two inputs
 * Verilog: Support $past when using AIG-based engines
+* Verilog: fix for nor/nand/xnor primitive gates
 
 # EBMC 5.4
 

lib/cbmc

@@ -0,0 +1,8 @@
+CORE broken-smt-backend
+nand4.sv
+--bound 0
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/primitive_gates/nand4.desc

@@ -0,0 +1,15 @@
+module main(output [31:0] nand_out, input [31:0] nand_in1, nand_in2, nand_in3);
+
+  // An 'nand' with three inputs over 32 bits.
+  nand x1[31:0] (nand_out, nand_in1, nand_in2, nand_in3);
+
+  // should pass
+  nand_x1_ok: assert final (~(nand_in1 & nand_in2 & nand_in3)==nand_out);
+
+  // An 'nand' with one input over 32 bits.
+  nand x2[31:0] (nand_out, nand_in1);
+
+  // should pass
+  nand_x2_ok: assert final (~nand_in1==nand_out);
+
+endmodule

regression/verilog/primitive_gates/nand4.sv

@@ -0,0 +1,8 @@
+CORE broken-smt-backend
+nor4.sv
+--bound 0
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/primitive_gates/nor4.desc

@@ -0,0 +1,15 @@
+module main(output [31:0] nor_out, input [31:0] nor_in1, nor_in2, nor_in3);
+
+  // An 'nor' with three inputs over 32 bits.
+  nor x1[31:0] (nor_out, nor_in1, nor_in2, nor_in3);
+
+  // should pass
+  nor_x1_ok: assert final (~(nor_in1 | nor_in2 | nor_in3)==nor_out);
+
+  // An 'nor' with one input over 32 bits.
+  nor x2[31:0] (nor_out, nor_in1);
+
+  // should pass
+  nor_x2_ok: assert final (~nor_in1==nor_out);
+
+endmodule

regression/verilog/primitive_gates/nor4.sv

@@ -0,0 +1,10 @@
+CORE broken-smt-backend
+xnor4.sv
+--bound 0
+^\[main\.xnor_x1_ok\] always ~\(main\.xnor_in1 \^ main\.xnor_in2 \^ main.xnor_in3\) == main.xnor_out: PROVED up to bound 0$
+^\[main\.xnor_x2_ok\] always ~main\.xnor_in1 == main.xnor_out: PROVED up to bound 0$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/primitive_gates/xnor4.desc

@@ -0,0 +1,15 @@
+module main(output [31:0] xnor_out, input [31:0] xnor_in1, xnor_in2, xnor_in3);
+
+  // An 'xnor' with three inputs over 32 bits.
+  xnor x1[31:0] (xnor_out, xnor_in1, xnor_in2, xnor_in3);
+
+  // should pass
+  xnor_x1_ok: assert final (~(xnor_in1 ^ xnor_in2 ^ xnor_in3)==xnor_out);
+
+  // An 'xnor' with one input over 32 bits.
+  xnor x2[31:0] (xnor_out, xnor_in1);
+
+  // should pass
+  xnor_x2_ok: assert final (~xnor_in1==xnor_out);
+
+endmodule

regression/verilog/primitive_gates/xnor4.sv

@@ -1518,7 +1518,7 @@ void verilog_synthesist::synth_module_instance_builtin(
     }
     else if(
       module == ID_and || module == ID_nand || module == ID_or ||
-      module == ID_nor || module == ID_xor)
+      module == ID_nor || module == ID_xor || module == ID_xnor)
     {
       // 1800-2017 28.4 and, nand, nor, or, xor, and xnor gates
       DATA_INVARIANT(
@@ -1541,44 +1541,11 @@ void verilog_synthesist::synth_module_instance_builtin(
         operands.push_back(connections[i]);
       }
 
-      exprt op{id, instance.type(), std::move(operands)};
+      auto op = exprt{id, instance.type(), std::move(operands)};
 
       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{xor_exprt{std::move(operands)}};
-      else
-        op = bitnot_exprt{bitxor_exprt{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);