Skip to content

Commit c1a5272

Browse files
committed
Verilog: KNOWNBUG test for continuous assignment to part select of net
This reproduces issue #638.
1 parent da41ae8 commit c1a5272

File tree

2 files changed

+17
-0
lines changed

2 files changed

+17
-0
lines changed
Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
KNOWNBUG
2+
continuous_assignment_to_net_part_select1.sv
3+
--bound 0
4+
^\[main\.p0\] always main\.some_wire\[1:0\] == 1: PROVED up to bound 0$
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
--
8+
--
9+
This reproduces https://github.com/diffblue/hw-cbmc/issues/638
Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
module main;
2+
3+
wire [31:0] some_wire;
4+
assign some_wire[1:0] = 'b01;
5+
6+
p0: assert final (some_wire[1:0] == 1);
7+
8+
endmodule

0 commit comments

Comments
 (0)