Skip to content

Commit 268e27e

Browse files
tautschnigtautschnig
authored
Merge pull request #886 from diffblue/xnor1
Verilog: implement xnor gates
2 parents 003138b + 13d7d6a commit 268e27e

File tree

8 files changed

+186
-7
lines changed

8 files changed

+186
-7
lines changed

‎regression/verilog/primitive_gates/xnor1.desc

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE broken-smt-backend
2+
xnor1.sv
3+
--bound 0
4+
^\[main\.xnor_ok\] always !\(xor\(xor\(main\.xnor_in1, main\.xnor_in2\), main\.xnor_in3\)\) == main\.xnor_out: PROVED up to bound 0$
5+
^\[main\.xnor_fail\] always main\.xnor_in1 == main\.xnor_in2 == main\.xnor_in3 == main\.xnor_out: REFUTED$
6+
^\[main\.xnor_is_reduction_xnor\] always ~\^\{ main\.xnor_in1, main\.xnor_in2, main\.xnor_in3 \} == main\.xnor_out: PROVED up to bound 0$
7+
^EXIT=10$
8+
^SIGNAL=0$
9+
--
10+
^warning: ignoring
11+
--

‎regression/verilog/primitive_gates/xnor1.sv

Lines changed: 61 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,61 @@
1+
module main(output xnor_out, input xnor_in1, xnor_in2, xnor_in3);
2+
3+
// An 'xnor' with three inputs.
4+
// 1800-2017 28.4 says that these "shall have a natural extension".
5+
xnor x1(xnor_out, xnor_in1, xnor_in2, xnor_in3);
6+
7+
// should pass
8+
`ifndef __ICARUS__
9+
xnor_ok: assert final (!(xnor_in1 ^ xnor_in2 ^ xnor_in3)==xnor_out);
10+
`endif
11+
12+
// should fail -- not the same as using a chain of binary xnors
13+
`ifndef __ICARUS__
14+
xnor_fail: assert final ((xnor_in1 ~^ xnor_in2 ~^ xnor_in3)==xnor_out);
15+
`endif
16+
17+
// should pass -- xnor is the same as reduction xnor
18+
`ifndef __ICARUS__
19+
xnor_is_reduction_xnor: assert final (~^{xnor_in1, xnor_in2, xnor_in3}==xnor_out);
20+
`endif
21+
22+
endmodule
23+
24+
// To check simulator behavior
25+
module xnor_tb;
26+
27+
wire xnor_out;
28+
reg xnor_in1, xnor_in2, xnor_in3;
29+
30+
main m(xnor_out, xnor_in1, xnor_in2, xnor_in3);
31+
32+
task print;
33+
begin
34+
$display("input: ", xnor_in1, xnor_in2, xnor_in3);
35+
$display(" xnor gate: ", xnor_out);
36+
$display(" reduction-xnor: ", ~^{xnor_in1, xnor_in2, xnor_in3});
37+
$display(" !reduction-xor: ", !(^{xnor_in1, xnor_in2, xnor_in3}));
38+
$display(" !xor: ", !(xnor_in1 ^ xnor_in2 ^ xnor_in3));
39+
$display(" binary xnors: ", xnor_in1 ~^ xnor_in2 ~^ xnor_in3);
40+
end
41+
endtask
42+
43+
initial begin
44+
{xnor_in1, xnor_in2, xnor_in3} = 'b000;
45+
#1;
46+
print();
47+
{xnor_in1, xnor_in2, xnor_in3} = 'b100;
48+
#1;
49+
print();
50+
{xnor_in1, xnor_in2, xnor_in3} = 'b110;
51+
#1;
52+
print();
53+
{xnor_in1, xnor_in2, xnor_in3} = 'b111;
54+
#1;
55+
print();
56+
{xnor_in1, xnor_in2, xnor_in3} = 'b101;
57+
#1;
58+
print();
59+
end
60+
61+
endmodule

‎regression/verilog/primitive_gates/xnor2.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE broken-smt-backend
2+
xnor2.sv
3+
--bound 0
4+
^\[main\.xnor_ok\] always !main\.xnor_in1 == main\.xnor_out: PROVED up to bound 0$
5+
^\[main\.xnor_is_reduction_xnor\] always ~\^\{ main\.xnor_in1 \} == main\.xnor_out: PROVED up to bound 0$
6+
^EXIT=0$
7+
^SIGNAL=0$
8+
--
9+
^warning: ignoring
10+
--

‎regression/verilog/primitive_gates/xnor2.sv

Lines changed: 45 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,45 @@
1+
module main(output xnor_out, input xnor_in1);
2+
3+
// An 'xnor' with just one input. These negate.
4+
xnor x1(xnor_out, xnor_in1);
5+
6+
// should pass
7+
`ifndef __ICARUS__
8+
xnor_ok: assert final (!xnor_in1==xnor_out);
9+
`endif
10+
11+
// should pass -- xnor is the same as reduction xnor
12+
`ifndef __ICARUS__
13+
xnor_is_reduction_xnor: assert final (~^{xnor_in1}==xnor_out);
14+
`endif
15+
16+
endmodule
17+
18+
// To check simulator behavior
19+
module xnor_tb;
20+
21+
wire xnor_out;
22+
reg xnor_in1;
23+
24+
main m(xnor_out, xnor_in1);
25+
26+
task print;
27+
begin
28+
$display("input: ", xnor_in1);
29+
$display(" xnor gate: ", xnor_out);
30+
$display(" reduction-xnor: ", ~^{xnor_in1});
31+
$display(" !reduction-xor: ", !(^{xnor_in1}));
32+
$display(" !: ", !xnor_in1);
33+
end
34+
endtask
35+
36+
initial begin
37+
{xnor_in1} = 'b0;
38+
#1;
39+
print();
40+
{xnor_in1} = 'b1;
41+
#1;
42+
print();
43+
end
44+
45+
endmodule

‎regression/verilog/primitive_gates/xnor3.desc

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE broken-smt-backend
2+
xnor3.sv
3+
--bound 0
4+
^\[main\.xnor_ok\] always main\.xnor_in1 ~\^ main\.xnor_in2 == main\.xnor_out: PROVED up to bound 0$
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
--
8+
^warning: ignoring
9+
--

‎regression/verilog/primitive_gates/xnor3.sv

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
module main(output [31:0] xnor_out, input [31:0] xnor_in1, xnor_in2);
2+
3+
// An 'xnor' with two inputs, 32 bits each.
4+
xnor x1[31:0](xnor_out, xnor_in1, xnor_in2);
5+
6+
// should pass
7+
`ifndef __ICARUS__
8+
xnor_ok: assert final (xnor_in1 ~^ xnor_in2==xnor_out);
9+
`endif
10+
11+
endmodule

‎src/verilog/parser.y

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2724,7 +2724,7 @@ n_input_gatetype:
27242724
| TOK_NAND { init($$, ID_nand); }
27252725
| TOK_NOR { init($$, ID_nor); }
27262726
| TOK_OR { init($$, ID_or); }
2727-
| TOK_XNOR { init($$, ID_nor); }
2727+
| TOK_XNOR { init($$, ID_xnor); }
27282728
| TOK_XOR { init($$, ID_xor); }
27292729
;
27302730

‎src/verilog/verilog_synthesis.cpp

Lines changed: 38 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1516,12 +1516,9 @@ void verilog_synthesist::synth_module_instance_builtin(
15161516
assert(trans.operands().size()==3);
15171517
trans.invar().add_to_operands(std::move(constraint));
15181518
}
1519-
else if(module==ID_and ||
1520-
module==ID_nand ||
1521-
module==ID_or ||
1522-
module==ID_nor ||
1523-
module==ID_xor ||
1524-
module==ID_xnor)
1519+
else if(
1520+
module == ID_and || module == ID_nand || module == ID_or ||
1521+
module == ID_nor || module == ID_xor)
15251522
{
15261523
// 1800-2017 28.4 and, nand, nor, or, xor, and xnor gates
15271524
DATA_INVARIANT(
@@ -1549,6 +1546,41 @@ void verilog_synthesist::synth_module_instance_builtin(
15491546
equal_exprt constraint{output, op};
15501547
trans.invar().add_to_operands(std::move(constraint));
15511548
}
1549+
else if(module == ID_xnor)
1550+
{
1551+
// Our solver does not have ID_xnor, hence use the negation of ID_xor
1552+
// ID_bitxor.
1553+
// With one operand, or with more than three operands, the result is
1554+
// ambiguous. The semantics of bitxnor do not match when using one
1555+
// or more than two operands.
1556+
DATA_INVARIANT(
1557+
instance.connections().size() >= 2,
1558+
"binary primitive gates should have at least two connections");
1559+
1560+
// One output, one or more inputs.
1561+
auto &connections = instance.connections();
1562+
auto &output = connections[0];
1563+
1564+
exprt::operandst operands;
1565+
1566+
// iterate over the module inputs
1567+
for(std::size_t i = 1; i < connections.size(); i++)
1568+
{
1569+
operands.push_back(connections[i]);
1570+
}
1571+
1572+
exprt op;
1573+
1574+
if(instance.type().id() == ID_bool)
1575+
op = not_exprt{
1576+
multi_ary_exprt{ID_xor, std::move(operands), instance.type()}};
1577+
else
1578+
op = bitnot_exprt{
1579+
multi_ary_exprt{ID_bitxor, std::move(operands), instance.type()}};
1580+
1581+
equal_exprt constraint{output, std::move(op)};
1582+
trans.invar().add_to_operands(std::move(constraint));
1583+
}
15521584
else if(module==ID_buf)
15531585
{
15541586
assert(instance.connections().size() >= 2);

0 commit comments

Comments
 (0)