Skip to content

Commit d881096

Browse files
committed
Verilog: KNOWNBUG for primitive gates with more than two inputs
This replicates issue #880.
1 parent b6deb2e commit d881096

File tree

2 files changed

+26
-0
lines changed

2 files changed

+26
-0
lines changed
Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -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
Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
module main(input or_in1, or_in2, or_in3);
2+
3+
wire or_out;
4+
5+
or o1(or_out, or_in1, or_in2, or_in3);
6+
7+
// should pass
8+
or_ok: assert final ((or_in1 || or_in2 || or_in3)==or_out);
9+
10+
// should fail
11+
or_not_ok1: assert final (or_out == (or_in1 || or_in2));
12+
13+
// should fail
14+
or_not_ok2: assert final (or_in1 || or_in2 || !or_in3);
15+
16+
endmodule

0 commit comments

Comments
 (0)