From 63b7c5cc261cb3848c63c26c476e25627635c989 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 23 Oct 2025 10:48:00 -0700 Subject: [PATCH] netlist: fix further extractbits off-by-one errors This fixes a further extracbits off-by-one error in the netlist generator. --- CHANGELOG | 1 + regression/ebmc/smv-netlist/verilog3.desc | 5 +++++ regression/ebmc/smv-netlist/verilog3.sv | 5 +++++ src/trans-netlist/trans_to_netlist.cpp | 5 ++++- 4 files changed, 15 insertions(+), 1 deletion(-) create mode 100644 regression/ebmc/smv-netlist/verilog3.desc create mode 100644 regression/ebmc/smv-netlist/verilog3.sv diff --git a/CHANGELOG b/CHANGELOG index 659ff0bea..de26baf5b 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -1,5 +1,6 @@ # EBMC 5.8 +* AIG/netlist engine: fix for conversion of extract bits operator * Verilog: semantic fix for output register ports * SystemVerilog: cover sequence * SystemVerilog: labeled immediate assert/assume/cover statements diff --git a/regression/ebmc/smv-netlist/verilog3.desc b/regression/ebmc/smv-netlist/verilog3.desc new file mode 100644 index 000000000..37a0b22e7 --- /dev/null +++ b/regression/ebmc/smv-netlist/verilog3.desc @@ -0,0 +1,5 @@ +CORE +verilog3.sv +--smv-netlist +^EXIT=0$ +^SIGNAL=0$ diff --git a/regression/ebmc/smv-netlist/verilog3.sv b/regression/ebmc/smv-netlist/verilog3.sv new file mode 100644 index 000000000..514292ca5 --- /dev/null +++ b/regression/ebmc/smv-netlist/verilog3.sv @@ -0,0 +1,5 @@ +module main; + wire [7:0] some_wire; + wire [31:0] something_else; + assign something_else = some_wire[7:1]; +endmodule diff --git a/src/trans-netlist/trans_to_netlist.cpp b/src/trans-netlist/trans_to_netlist.cpp index 7f04cc306..cea043f47 100644 --- a/src/trans-netlist/trans_to_netlist.cpp +++ b/src/trans-netlist/trans_to_netlist.cpp @@ -594,7 +594,10 @@ void convert_trans_to_netlistt::convert_lhs_rec( if(!to_integer_non_constant(to_extractbits_expr(expr).index(), new_from)) { boolbv_widtht boolbv_width(ns); - mp_integer new_to = new_from + boolbv_width(expr.type()); + const auto width = boolbv_width(expr.type()); + DATA_INVARIANT( + width != 0, "trans_to_netlist got extractbits with zero-width operand"); + mp_integer new_to = new_from + width - 1; from = new_from.to_ulong(); to = new_to.to_ulong();