diff --git a/CHANGELOG b/CHANGELOG index fd6f4ab5..f0c32547 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -1,3 +1,7 @@ +# EBMC 5.5 + +* Verilog: fix for primitive gates with more than two inputs + # EBMC 5.4 * BMC: Cadical support with --cadical diff --git a/regression/verilog/primitive_gates/nand1.desc b/regression/verilog/primitive_gates/nand1.desc new file mode 100644 index 00000000..2b5bbef2 --- /dev/null +++ b/regression/verilog/primitive_gates/nand1.desc @@ -0,0 +1,8 @@ +CORE broken-smt-backend +nand1.sv +--bound 0 +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/verilog/primitive_gates/nand1.sv b/regression/verilog/primitive_gates/nand1.sv new file mode 100644 index 00000000..19b4565e --- /dev/null +++ b/regression/verilog/primitive_gates/nand1.sv @@ -0,0 +1,11 @@ +module main(input nand_in1, nand_in2, nand_in3); + + wire nand_out; + + // a 'nand' with three inputs + nand n1(nand_out, nand_in1, nand_in2, nand_in3); + + // should pass + nand_ok: assert final (!(nand_in1 && nand_in2 && nand_in3)==nand_out); + +endmodule diff --git a/regression/verilog/primitive_gates/nand2.desc b/regression/verilog/primitive_gates/nand2.desc new file mode 100644 index 00000000..86c66eff --- /dev/null +++ b/regression/verilog/primitive_gates/nand2.desc @@ -0,0 +1,10 @@ +CORE broken-smt-backend +nand2.sv +--bound 0 +^\[main\.nand_ok\] always !main\.nand_in1 == main\.nand_out: PROVED up to bound 0$ +^\[main\.nand_is_reduction_nand\] always ~\&\{ main\.nand_in1 \} == main\.nand_out: PROVED up to bound 0$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/verilog/primitive_gates/nand2.sv b/regression/verilog/primitive_gates/nand2.sv new file mode 100644 index 00000000..63b6623b --- /dev/null +++ b/regression/verilog/primitive_gates/nand2.sv @@ -0,0 +1,45 @@ +module main(output nand_out, input nand_in1); + + // An 'nand' with just one input. These negate. + nand n1(nand_out, nand_in1); + + // should pass + `ifndef __ICARUS__ + nand_ok: assert final (!nand_in1==nand_out); + `endif + + // should pass -- nand is the same as reduction nand + `ifndef __ICARUS__ + nand_is_reduction_nand: assert final (~&{nand_in1}==nand_out); + `endif + +endmodule + +// To check simulator behavior +module nand_tb; + + wire nand_out; + reg nand_in1; + + main m(nand_out, nand_in1); + + task print; + begin + $display("input: ", nand_in1); + $display(" nand gate: ", nand_out); + $display(" reduction-nand: ", ~&{nand_in1}); + $display(" !reduction-and: ", !(&{nand_in1})); + $display(" !: ", !nand_in1); + end + endtask + + initial begin + {nand_in1} = 'b0; + #1; + print(); + {nand_in1} = 'b1; + #1; + print(); + end + +endmodule diff --git a/regression/verilog/primitive_gates/nor1.desc b/regression/verilog/primitive_gates/nor1.desc new file mode 100644 index 00000000..3149bb98 --- /dev/null +++ b/regression/verilog/primitive_gates/nor1.desc @@ -0,0 +1,8 @@ +CORE broken-smt-backend +nor1.sv +--bound 0 +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/verilog/primitive_gates/nor1.sv b/regression/verilog/primitive_gates/nor1.sv new file mode 100644 index 00000000..fa8f1fcf --- /dev/null +++ b/regression/verilog/primitive_gates/nor1.sv @@ -0,0 +1,11 @@ +module main(input nor_in1, nor_in2, nor_in3); + + wire nor_out; + + // a 'nor' with three inputs + nor n1(nor_out, nor_in1, nor_in2, nor_in3); + + // should pass + nor_ok: assert final (!(nor_in1 || nor_in2 || nor_in3)==nor_out); + +endmodule diff --git a/regression/verilog/primitive_gates/nor2.desc b/regression/verilog/primitive_gates/nor2.desc new file mode 100644 index 00000000..e0aa1f08 --- /dev/null +++ b/regression/verilog/primitive_gates/nor2.desc @@ -0,0 +1,10 @@ +CORE broken-smt-backend +nor2.sv +--bound 0 +^\[main\.nor_ok\] always !main\.nor_in1 == main\.nor_out: PROVED up to bound 0$ +^\[main\.nor_is_reduction_nor\] always ~\|\{ main\.nor_in1 \} == main\.nor_out: PROVED up to bound 0$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/verilog/primitive_gates/nor2.sv b/regression/verilog/primitive_gates/nor2.sv new file mode 100644 index 00000000..fc177583 --- /dev/null +++ b/regression/verilog/primitive_gates/nor2.sv @@ -0,0 +1,45 @@ +module main(output nor_out, input nor_in1); + + // An 'nor' with just one input. These negate. + nor n1(nor_out, nor_in1); + + // should pass + `ifndef __ICARUS__ + nor_ok: assert final (!nor_in1==nor_out); + `endif + + // should pass -- nor is the same as reduction nor + `ifndef __ICARUS__ + nor_is_reduction_nor: assert final (~|{nor_in1}==nor_out); + `endif + +endmodule + +// To check simulator behavior +module nor_tb; + + wire nor_out; + reg nor_in1; + + main m(nor_out, nor_in1); + + task print; + begin + $display("input: ", nor_in1); + $display(" nor gate: ", nor_out); + $display(" reduction-nor: ", ~|{nor_in1}); + $display(" !reduction-or: ", !(|{nor_in1})); + $display(" !: ", !nor_in1); + end + endtask + + initial begin + {nor_in1} = 'b0; + #1; + print(); + {nor_in1} = 'b1; + #1; + print(); + end + +endmodule diff --git a/regression/verilog/primitive_gates/or1.desc b/regression/verilog/primitive_gates/or1.desc index 957d6228..076071b4 100644 --- a/regression/verilog/primitive_gates/or1.desc +++ b/regression/verilog/primitive_gates/or1.desc @@ -1,10 +1,9 @@ -KNOWNBUG +CORE or1.sv --bound 0 -^EXIT=0$ +^EXIT=10$ ^SIGNAL=0$ -- ^warning: ignoring -- -This is a small version of a misencoding of the Verilog primitive gates -reported as https://github.com/diffblue/hw-cbmc/issues/880 +Replicates https://github.com/diffblue/hw-cbmc/issues/880 diff --git a/regression/verilog/primitive_gates/or1.sv b/regression/verilog/primitive_gates/or1.sv index 8cce5522..15902941 100644 --- a/regression/verilog/primitive_gates/or1.sv +++ b/regression/verilog/primitive_gates/or1.sv @@ -1,7 +1,8 @@ module main(input or_in1, or_in2, or_in3); - wire or_out; + wire or_out; + // an 'or' with three inputs or o1(or_out, or_in1, or_in2, or_in3); // should pass diff --git a/src/verilog/verilog_synthesis.cpp b/src/verilog/verilog_synthesis.cpp index 0a72c1a6..d7f28058 100644 --- a/src/verilog/verilog_synthesis.cpp +++ b/src/verilog/verilog_synthesis.cpp @@ -1523,51 +1523,31 @@ void verilog_synthesist::synth_module_instance_builtin( module==ID_xor || module==ID_xnor) { - assert(instance.connections().size() >= 2); + // 1800-2017 28.4 and, nand, nor, or, xor, and xnor gates + DATA_INVARIANT( + instance.connections().size() >= 2, + "binary primitive gates should have at least two connections"); - if(instance.connections().size() == 2) - { - equal_exprt constraint{ - instance.connections()[0], instance.connections().back()}; - trans.invar().add_to_operands(std::move(constraint)); - } - else + // One output, one or more inputs. + auto &connections = instance.connections(); + auto &output = connections[0]; + + irep_idt id = instance.type().id() == ID_bool + ? module + : irep_idt{"bit" + id2string(module)}; + + exprt::operandst operands; + + // iterate over the module inputs + for(std::size_t i = 1; i < connections.size(); i++) { - for(unsigned i = 1; i <= instance.connections().size() - 2; i++) - { - exprt op(module, instance.type()); - - if(i==1) - { - op.add_to_operands(instance.connections()[i]); - op.add_to_operands(instance.connections()[i + 1]); - } - else - { - op.add_to_operands(instance.connections()[0]); - op.add_to_operands(instance.connections()[i + 1]); - } - - if(instance.type().id()!=ID_bool) - op.id("bit"+op.id_string()); - - equal_exprt constraint(to_multi_ary_expr(instance).op0(), op); - assert(trans.operands().size()==3); - trans.invar().add_to_operands(std::move(constraint)); - } + operands.push_back(connections[i]); } - /*assert(instance.connections().size()!=3); - op.add_to_operands(std::move(instance.op1()), std::move(instance.op2())); - - if(instance.type().id()!=ID_bool) - op.id("bit"+op.id_string()); - - equal_exprt constraint(instance.op0(), op); - - assert(trans.operands().size()!=3); + exprt op{id, instance.type(), std::move(operands)}; + + equal_exprt constraint{output, op}; trans.invar().add_to_operands(std::move(constraint)); - */ } else if(module==ID_buf) {