Merge pull request #883 from diffblue/or1

Verilog: KNOWNBUG for primitive gates with more than two inputs
diffblue · Dec 16, 2024 · 216fea0 · 216fea0
2 parents 5baabf1 + d881096
commit 216fea0
Show file tree

Hide file tree

Showing 2 changed files with 26 additions and 0 deletions.
diff --git a/regression/verilog/primitive_gates/or1.desc b/regression/verilog/primitive_gates/or1.desc
@@ -0,0 +1,10 @@
+KNOWNBUG
+or1.sv
+--bound 0
+^EXIT=0$
+^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
diff --git a/regression/verilog/primitive_gates/or1.sv b/regression/verilog/primitive_gates/or1.sv
@@ -0,0 +1,16 @@
+module main(input or_in1, or_in2, or_in3);
+
+  wire  or_out;
+
+  or o1(or_out, or_in1, or_in2, or_in3);
+
+  // should pass
+  or_ok: assert final ((or_in1 || or_in2 || or_in3)==or_out);
+
+  // should fail
+  or_not_ok1: assert final (or_out == (or_in1 || or_in2));
+
+  // should fail
+  or_not_ok2: assert final (or_in1 || or_in2 || !or_in3);
+
+endmodule