Skip to content

Verilog: fix three type-checker gaps from LogikBench triage - #2052

Draft
kroening wants to merge 3 commits into
mainfrom
kroening/logikbench-typecheck-gaps
Draft

Verilog: fix three type-checker gaps from LogikBench triage#2052
kroening wants to merge 3 commits into
mainfrom
kroening/logikbench-typecheck-gaps

Conversation

@kroening

Copy link
Copy Markdown
Collaborator

This addresses the type-checker gaps bucket of the LogikBench RTL
triage (parse+elaborate only, ebmc --bound 0). Three independent
root causes, one commit each, each with a hand-authored regression test.

Root cause 1 — "failed to get identifier on LHS constant" (genvar)

parameterize_instantiated_modules() did not restore the per-iteration
genvar values when descending into a set_genvars wrapper, so port
connections / parameter assignments of a generate-loop instance were
evaluated against the post-loop genvar value. A module output
connected to a genvar-indexed vector bit (child u(.o(arr[g]))) then
used the wrong index; for the top index arr[WIDTH-1] this looked
out-of-bounds, was folded to constant 0, and check_lhs rejected it.
Fix: restore (and afterwards re-restore) the captured genvar values,
mirroring convert_module_item.

  • blocks/lpddr5 — now fully passes.
  • blocks/chiplink, koios/bwave_like_fixed_small,
    koios/bwave_like_float_small — clear this error; they now fail
    later on a different, unrelated synthesis issue ("conflicting
    assignment types" / "conflict with previous assignment"), which is a
    separate root-cause bucket, not fixed here.

Root cause 2 — implicit nets in a concatenation LHS

IEEE 1800-2017 6.10 implicitly declares an undeclared identifier used on
the LHS of a continuous assignment as a net. This was handled for a bare
identifier but not for a concatenation member, e.g.
assign {cout, out} = a - b; (discard-carry idiom). Fix: declare each
undeclared bare-identifier member as a scalar net before converting.

  • arithmetic/sub — now fully passes.

Root cause 3 — integer has unknown number of bits

verilog_bits_opt() had no case for the mathematical integer type
ID_integer (produced by $clog2 and unsized integer constants), so a
width query threw. Assigning such a value to a sized parameter reaches
assignment_conversion, which needs the width, e.g.
localparam [2:0] ARSIZE = $clog2(DW/8);. Fix: treat integer as 32
bits in width contexts, consistent with the existing
integer→signedbv{32} casts (IEEE 1800-2017 6.11, 11.8.1).

  • blocks/dma — now fully passes.
  • koios/dnnweaver — clears this error; then fails on an unrelated
    hierarchical reference into a generate-block array
    (LOOP_N[n-1].buf_read_req_fwd), a separate feature not in scope.

Not fixed (left failing, with rationale)

  • large/vortex — uses deep hierarchical references rooted at the
    module's own name into nested SystemVerilog interface instances
    (vortex_core_wrap.core.warp_ctl_if.split_valid). This is valid SV but
    needs substantial cross-module hierarchical-interface-reference support
    that EBMC does not have; out of scope for a targeted type-checker fix.
  • koios/dnnweaver — beyond the integer fix it needs generate-block-
    array hierarchical references (see above).

Summary of the 8 circuits

Circuit Status
arithmetic/sub fixed
blocks/dma fixed
blocks/lpddr5 fixed
blocks/chiplink past this error; blocked by unrelated synthesis issue
koios/bwave_like_fixed_small past this error; blocked by unrelated synthesis issue
koios/bwave_like_float_small past this error; blocked by unrelated synthesis issue
koios/dnnweaver past this error; blocked by generate-block hierarchical ref
large/vortex not fixed — needs hierarchical interface references

make -C regression/verilog test passes with the three new tests added.

🤖 Generated with Claude Code

kroening and others added 3 commits July 23, 2026 06:45
parameterize_instantiated_modules() walks generate-elaborated module
items and, for each instance, constant-folds parameter assignments and
type-checks port connections. When it descended into a set_genvars
wrapper it did not restore the genvar values captured for that generate
iteration, so those expressions were evaluated against the live genvars
map, which still held the post-loop value of the loop index.

As a result a module output connected to a genvar-indexed vector bit
inside a generate for-loop (e.g. `child u(.o(arr[g]))`) was evaluated
with the wrong index. For the top index arr[WIDTH-1] this looked
out-of-bounds and was folded to the constant 0, after which check_lhs
rejected it with "failed to get identifier on LHS constant".

Restore the captured genvar values (mirroring convert_module_item)
before recursing, and put them back afterwards.

Fixes elaboration of LogikBench blocks/lpddr5 and unblocks
blocks/chiplink and koios/bwave_like_{fixed,float}_small past this
error.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
… LHS

IEEE 1800-2017 6.10 declares an undeclared identifier used on the LHS of
a continuous assignment as an implicit net of the default net type.
convert_continuous_assign already did this for a bare-identifier LHS but
not when the identifier appeared as a member of a concatenation, e.g.

  assign {carry, sum} = a + b;   // carry is undeclared

which was rejected with "unknown identifier". Declare each undeclared
bare-identifier member as a scalar net before converting the
concatenation.

Fixes LogikBench arithmetic/sub.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
verilog_bits_opt() (used by both get_width and verilog_bits) had no case
for the mathematical integer type ID_integer, so any width query on it
threw "type `integer' has unknown number of bits". This type arises from
$clog2 and other unsized integer constant expressions. Assigning such a
value to a sized net/parameter reaches assignment_conversion, which needs
the width, e.g.

  localparam [2:0] ARSIZE = $clog2(DW/8);

Treat the integer type as 32 bits wide in width contexts, consistent with
how the type checker already casts integer/$clog2 results to signedbv{32}
(IEEE 1800-2017 6.11, 11.8.1).

Fixes LogikBench blocks/dma; unblocks koios/dnnweaver past this error.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
@kroening

Copy link
Copy Markdown
Collaborator Author

I'll split this PR up.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant