diff --git a/CHANGELOG b/CHANGELOG index 3c310d306..05f28e602 100644 --- a/CHANGELOG +++ b/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 diff --git a/lib/cbmc b/lib/cbmc index 857c88e7e..fc4f7ca71 160000 --- a/lib/cbmc +++ b/lib/cbmc @@ -1 +1 @@ -Subproject commit 857c88e7e982a05b22301b49fee03d27895ed58d +Subproject commit fc4f7ca71ddcbd290cea0d9ac58b6cc6f6b79cb0 diff --git a/regression/verilog/primitive_gates/nand4.desc b/regression/verilog/primitive_gates/nand4.desc new file mode 100644 index 000000000..e2d2646f9 --- /dev/null +++ b/regression/verilog/primitive_gates/nand4.desc @@ -0,0 +1,8 @@ +CORE broken-smt-backend +nand4.sv +--bound 0 +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/verilog/primitive_gates/nand4.sv b/regression/verilog/primitive_gates/nand4.sv new file mode 100644 index 000000000..9b7bfdd24 --- /dev/null +++ b/regression/verilog/primitive_gates/nand4.sv @@ -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 diff --git a/regression/verilog/primitive_gates/nor4.desc b/regression/verilog/primitive_gates/nor4.desc new file mode 100644 index 000000000..5ae5809ee --- /dev/null +++ b/regression/verilog/primitive_gates/nor4.desc @@ -0,0 +1,8 @@ +CORE broken-smt-backend +nor4.sv +--bound 0 +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/verilog/primitive_gates/nor4.sv b/regression/verilog/primitive_gates/nor4.sv new file mode 100644 index 000000000..48eb3d462 --- /dev/null +++ b/regression/verilog/primitive_gates/nor4.sv @@ -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 diff --git a/regression/verilog/primitive_gates/xnor4.desc b/regression/verilog/primitive_gates/xnor4.desc new file mode 100644 index 000000000..e249c0f18 --- /dev/null +++ b/regression/verilog/primitive_gates/xnor4.desc @@ -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 +-- diff --git a/regression/verilog/primitive_gates/xnor4.sv b/regression/verilog/primitive_gates/xnor4.sv new file mode 100644 index 000000000..28bd06547 --- /dev/null +++ b/regression/verilog/primitive_gates/xnor4.sv @@ -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 diff --git a/src/verilog/verilog_synthesis.cpp b/src/verilog/verilog_synthesis.cpp index 646efcb4d..6956a1d4f 100644 --- a/src/verilog/verilog_synthesis.cpp +++ b/src/verilog/verilog_synthesis.cpp @@ -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);