Skip to content

Commit 1b31efb

Browse files
authored
Merge pull request #890 from diffblue/bump-cbmc-onehot0
bump CBMC dependency
2 parents 3d95eaa + 63cea6d commit 1b31efb

File tree

4 files changed

+8
-6
lines changed

4 files changed

+8
-6
lines changed

CHANGELOG

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
# EBMC 5.5
22

3+
* Verilog: bugfix for $onehot0
34
* Verilog: fix for primitive gates with more than two inputs
45

56
# EBMC 5.4

regression/verilog/SVA/system_verilog_assertion3.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
CORE broken-smt-backend
1+
CORE
22
system_verilog_assertion3.sv
3-
--module main --bound 1
3+
--module main --bound 0
44
^EXIT=0$
55
^SIGNAL=0$
66
--

regression/verilog/SVA/system_verilog_assertion3.sv

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,9 @@ module main();
33
assert final ($onehot('b0001000));
44
assert final (!$onehot('b0101000));
55
assert final (!$onehot('b00000));
6-
assert final ($onehot0('b00000));
7-
assert final ($onehot0('b000100));
8-
assert final (!$onehot0('b010100));
6+
assert final (!$onehot0(6'b00000));
7+
assert final (!$onehot0(6'b000100));
8+
assert final (!$onehot0(6'b010100));
9+
assert final ($onehot0(6'b111101));
910

1011
endmodule

0 commit comments

Comments
 (0)