Merge pull request #885 from diffblue/fix-or1

Verilog: fix for multi-ary binary primitive gates

Author: kroening

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

regression/verilog/primitive_gates/nand1.desc

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

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

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
+--

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

regression/verilog/primitive_gates/nor1.desc

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

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

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
+--

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

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

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

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)
     {