Skip to content

Verilog: fix array index direction for descending and ascending ranges#1729

Merged
tautschnig merged 1 commit intomainfrom
kroening/fix-array-direction
Mar 13, 2026
Merged

Verilog: fix array index direction for descending and ascending ranges#1729
tautschnig merged 1 commit intomainfrom
kroening/fix-array-direction

Conversation

@kroening
Copy link
Copy Markdown
Collaborator

Arrays declared with descending ranges (e.g., [4:0]) or ascending ranges with non-zero offsets were not correctly mapping Verilog indices to internal array indices. This affected both packed and unpacked arrays.

Problem

For a descending range like int my_array[4:0], the assignment pattern '{ 1, 2, 3, 4, 5 } should assign index 4=1, index 3=2, ..., index 0=5 per IEEE 1800-2017 §10.9.1. However, my_array[0] was returning 1 instead of 5 because no index adjustment was performed.

The same issue affected packed arrays like bit [4:0][31:0].

Fix

  • Unpacked arrays: Adjust the Verilog index to the internal index in convert_bit_select_expr() based on range direction and offset.
  • Packed arrays: Reverse assignment pattern operands for descending ranges so that internal index 0 corresponds to Verilog index 0. Update to_bitvector() in the lowering to match the new convention.
  • Packed array types: Set ID_C_increasing on multi-dimensional packed array types (was previously missing).

Test updates

  • packed_direction1 and unpacked_direction1: promoted from KNOWNBUG to CORE
  • array_conversion3: updated expectations from REFUTED to PROVED
  • array_in_struct1: corrected assertions to match IEEE 1800-2017 descending range semantics

@kroening kroening force-pushed the kroening/fix-array-direction branch 2 times, most recently from d71c782 to c301e4c Compare March 13, 2026 03:31
Arrays declared with descending ranges (e.g., [4:0]) or ascending ranges
with non-zero offsets were not correctly mapping Verilog indices to
internal array indices. This affected both packed and unpacked arrays.

For unpacked arrays, the Verilog index is now adjusted to the internal
index based on the range direction and offset. For packed arrays, the
assignment pattern operands are reversed for descending ranges so that
internal index 0 corresponds to Verilog index 0, and the bitvector
lowering is updated to match.

Per IEEE 1800-2017 section 10.9.1, assignment patterns assign elements
left-to-right starting from the left index of the range.
@kroening kroening force-pushed the kroening/fix-array-direction branch from c301e4c to bbd1589 Compare March 13, 2026 03:35
@tautschnig tautschnig merged commit 74fac00 into main Mar 13, 2026
11 checks passed
@tautschnig tautschnig deleted the kroening/fix-array-direction branch March 13, 2026 15:29
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants