We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent b6deb2e commit a331144Copy full SHA for a331144
regression/verilog/primitive_gates/or1.desc
@@ -0,0 +1,10 @@
1
+KNOWNBUG
2
+or1.sv
3
+--bound 0
4
+^EXIT=0$
5
+^SIGNAL=0$
6
+--
7
+^warning: ignoring
8
9
+This is a small version of a misencoding of the Verilog primitive gates
10
+reported as https://github.com/diffblue/hw-cbmc/issues/880
regression/verilog/primitive_gates/or1.sv
@@ -0,0 +1,13 @@
+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
11
+ or_not_ok: assert final (or_out == (or_in1 || or_in2));
12
13
+endmodule
0 commit comments