From 767623b4fdc7b5df46896fffa37416415c4a3db3 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Wed, 22 Oct 2025 13:24:53 -0700 Subject: [PATCH 1/2] KNOWNBUG test for smv-to-netlist --- regression/ebmc/smv-netlist/verilog2.desc | 8 ++++++++ regression/ebmc/smv-netlist/verilog2.sv | 4 ++++ 2 files changed, 12 insertions(+) create mode 100644 regression/ebmc/smv-netlist/verilog2.desc create mode 100644 regression/ebmc/smv-netlist/verilog2.sv diff --git a/regression/ebmc/smv-netlist/verilog2.desc b/regression/ebmc/smv-netlist/verilog2.desc new file mode 100644 index 000000000..d2ce100d3 --- /dev/null +++ b/regression/ebmc/smv-netlist/verilog2.desc @@ -0,0 +1,8 @@ +KNOWNBUG +verilog2.sv +--smv-netlist +^EXIT=0$ +^SIGNAL=0$ +-- +-- +This throws an error. diff --git a/regression/ebmc/smv-netlist/verilog2.sv b/regression/ebmc/smv-netlist/verilog2.sv new file mode 100644 index 000000000..f4c7425cd --- /dev/null +++ b/regression/ebmc/smv-netlist/verilog2.sv @@ -0,0 +1,4 @@ +module main; + wire [7:0] some_wire; + assign some_wire[7:0] = 0; +endmodule From 26ef9a0b3fddbb1e4ed7258f1b9916aa67e97dae Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Wed, 22 Oct 2025 14:01:28 -0700 Subject: [PATCH 2/2] netlist: fix off-by-one bug This fixes an off-by-one error in the netlist conversion. --- regression/ebmc/smv-netlist/verilog2.desc | 3 +-- src/trans-netlist/trans_to_netlist.cpp | 9 ++++++--- 2 files changed, 7 insertions(+), 5 deletions(-) diff --git a/regression/ebmc/smv-netlist/verilog2.desc b/regression/ebmc/smv-netlist/verilog2.desc index d2ce100d3..04061ef65 100644 --- a/regression/ebmc/smv-netlist/verilog2.desc +++ b/regression/ebmc/smv-netlist/verilog2.desc @@ -1,8 +1,7 @@ -KNOWNBUG +CORE verilog2.sv --smv-netlist ^EXIT=0$ ^SIGNAL=0$ -- -- -This throws an error. diff --git a/src/trans-netlist/trans_to_netlist.cpp b/src/trans-netlist/trans_to_netlist.cpp index 44948e7d7..863d74a36 100644 --- a/src/trans-netlist/trans_to_netlist.cpp +++ b/src/trans-netlist/trans_to_netlist.cpp @@ -720,7 +720,7 @@ void convert_trans_to_netlistt::add_equality_rec( bv_varidt bv_varid; bv_varid.id=lhs.get(ID_identifier); - + for(bv_varid.bit_nr=lhs_from; bv_varid.bit_nr!=(lhs_to+1); bv_varid.bit_nr++) @@ -767,9 +767,12 @@ void convert_trans_to_netlistt::add_equality_rec( boolbv_widtht boolbv_width(ns); + const auto width = boolbv_width(lhs.type()); + + DATA_INVARIANT(width != 0, "add_equality_rec got zero-width bit-vector"); + std::size_t new_lhs_from = lhs_from + index.to_ulong(); - std::size_t new_lhs_to = - lhs_from + index.to_ulong() + boolbv_width(lhs.type()); + std::size_t new_lhs_to = lhs_from + index.to_ulong() + width - 1; add_equality_rec( src, to_extractbits_expr(lhs).src(), new_lhs_from, new_lhs_to, rhs_entry);