From 13d7d6a71040b995853625c890abd5e578c1da70 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 16 Dec 2024 10:45:50 -0800 Subject: [PATCH] Verilog: implement xnor gates Our backend solver does not support xnor. On Booleans, implement via a lowering to not(xor(...)). On bit-vectors, use the bit-wise negation of bitxor. --- regression/verilog/primitive_gates/xnor1.desc | 11 ++++ regression/verilog/primitive_gates/xnor1.sv | 61 +++++++++++++++++++ regression/verilog/primitive_gates/xnor2.desc | 10 +++ regression/verilog/primitive_gates/xnor2.sv | 45 ++++++++++++++ regression/verilog/primitive_gates/xnor3.desc | 9 +++ regression/verilog/primitive_gates/xnor3.sv | 11 ++++ src/verilog/parser.y | 2 +- src/verilog/verilog_synthesis.cpp | 44 +++++++++++-- 8 files changed, 186 insertions(+), 7 deletions(-) create mode 100644 regression/verilog/primitive_gates/xnor1.desc create mode 100644 regression/verilog/primitive_gates/xnor1.sv create mode 100644 regression/verilog/primitive_gates/xnor2.desc create mode 100644 regression/verilog/primitive_gates/xnor2.sv create mode 100644 regression/verilog/primitive_gates/xnor3.desc create mode 100644 regression/verilog/primitive_gates/xnor3.sv diff --git a/regression/verilog/primitive_gates/xnor1.desc b/regression/verilog/primitive_gates/xnor1.desc new file mode 100644 index 00000000..5157b0fc --- /dev/null +++ b/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 +-- diff --git a/regression/verilog/primitive_gates/xnor1.sv b/regression/verilog/primitive_gates/xnor1.sv new file mode 100644 index 00000000..99215c4c --- /dev/null +++ b/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 diff --git a/regression/verilog/primitive_gates/xnor2.desc b/regression/verilog/primitive_gates/xnor2.desc new file mode 100644 index 00000000..2ef667e2 --- /dev/null +++ b/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 +-- diff --git a/regression/verilog/primitive_gates/xnor2.sv b/regression/verilog/primitive_gates/xnor2.sv new file mode 100644 index 00000000..c6b1e445 --- /dev/null +++ b/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 diff --git a/regression/verilog/primitive_gates/xnor3.desc b/regression/verilog/primitive_gates/xnor3.desc new file mode 100644 index 00000000..c0221a59 --- /dev/null +++ b/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 +-- diff --git a/regression/verilog/primitive_gates/xnor3.sv b/regression/verilog/primitive_gates/xnor3.sv new file mode 100644 index 00000000..e3e315f2 --- /dev/null +++ b/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 diff --git a/src/verilog/parser.y b/src/verilog/parser.y index 21666b37..fbd33040 100644 --- a/src/verilog/parser.y +++ b/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); } ; diff --git a/src/verilog/verilog_synthesis.cpp b/src/verilog/verilog_synthesis.cpp index d7f28058..94d1c6b9 100644 --- a/src/verilog/verilog_synthesis.cpp +++ b/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);