From 63cea6d077fe403eba7118ead6d442cff22f61dd Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 19 Dec 2024 11:17:22 -0800 Subject: [PATCH] bump CBMC dependency The bump of the CBMC dependency fixes $onehot0. --- CHANGELOG | 1 + lib/cbmc | 2 +- regression/verilog/SVA/system_verilog_assertion3.desc | 4 ++-- regression/verilog/SVA/system_verilog_assertion3.sv | 7 ++++--- 4 files changed, 8 insertions(+), 6 deletions(-) diff --git a/CHANGELOG b/CHANGELOG index f0c325476..485ac6513 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -1,5 +1,6 @@ # EBMC 5.5 +* Verilog: bugfix for $onehot0 * Verilog: fix for primitive gates with more than two inputs # EBMC 5.4 diff --git a/lib/cbmc b/lib/cbmc index fb2847509..857c88e7e 160000 --- a/lib/cbmc +++ b/lib/cbmc @@ -1 +1 @@ -Subproject commit fb284750934f5830501990d54c1d8118c7af0d3d +Subproject commit 857c88e7e982a05b22301b49fee03d27895ed58d diff --git a/regression/verilog/SVA/system_verilog_assertion3.desc b/regression/verilog/SVA/system_verilog_assertion3.desc index f86fc8b84..38ce84e04 100644 --- a/regression/verilog/SVA/system_verilog_assertion3.desc +++ b/regression/verilog/SVA/system_verilog_assertion3.desc @@ -1,6 +1,6 @@ -CORE broken-smt-backend +CORE system_verilog_assertion3.sv ---module main --bound 1 +--module main --bound 0 ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/SVA/system_verilog_assertion3.sv b/regression/verilog/SVA/system_verilog_assertion3.sv index 528f64709..daa704b92 100644 --- a/regression/verilog/SVA/system_verilog_assertion3.sv +++ b/regression/verilog/SVA/system_verilog_assertion3.sv @@ -3,8 +3,9 @@ module main(); assert final ($onehot('b0001000)); assert final (!$onehot('b0101000)); assert final (!$onehot('b00000)); - assert final ($onehot0('b00000)); - assert final ($onehot0('b000100)); - assert final (!$onehot0('b010100)); + assert final (!$onehot0(6'b00000)); + assert final (!$onehot0(6'b000100)); + assert final (!$onehot0(6'b010100)); + assert final ($onehot0(6'b111101)); endmodule