Verilog: don't treat 'integer' loop counters as synthesis driver conflicts

[kroening]

Summary

Part of the LogikBench elaboration triage (benchmarking/logikbench.sh,
report at https://diffblue.github.io/hw-cbmc/). This addresses the
synthesis driver-conflict bucket: circuits that failed ebmc --bound 0
during synthesis with either

• "conflict with previous assignment", or
• "conflicting assignment types for X (new: clocked, old: combinational)".

Both are thrown from src/verilog/verilog_synthesis.cpp while tracking, per
signal, which bit-ranges/members have already been assigned so that a signal
driven twice in an unmergeable way is rejected.

Root cause (differs from the original branch-merge / generate-instance hypotheses)

The tracking in assignment() runs for every assigned symbol, but
synth_assignments() never turns Verilog integer-typed variables into state
or wires — they are elaboration-only scratch. Module-level integer
variables are idiomatically used as for-loop counters and shared across
several always/initial blocks. Because the member tracking persists across
blocks (move_assignments() runs at each block's end), a loop counter such as
integer i assigned in two blocks was flagged as a spurious multiple-driver
conflict:

• assigned in two combinational blocks → "conflict with previous assignment"
  (the reported location is the for (i = 0; …) header, i.e. the counter, not
  the data signal);
• assigned in a combinational and a clocked block → "conflicting assignment
  types (new: clocked, old: combinational)".

Only the last block's value of such a counter is ever observable, so the reuse
is benign.

Fix

Exempt symbols carrying the Verilog integer type
(type.get(ID_C_verilog_type) == ID_integer) from assignment-type and
member/driver-conflict tracking — consistent with synth_assignments(), which
already excludes them from synthesis. One-line guard plus a comment; no change
to how genuine state/wire signals are checked.

Circuits fixed (3)

Circuit	Was failing on
basic/crossbar	conflict on shared integer i across two always @(*)
blocks/viterbi	integer j combinational vs clocked (rtl/viterbi.v:121)
large/qr	integer k combinational vs clocked (rtl/qr.v:90)

All three now elaborate (ebmc --bound 0 → exit 0/10).

Circuits deliberately left failing (12) — genuine conflicts / real EBMC limitation, not false positives

• blocks/reedsolomon — genuinely invalid RTL. Register s_nz is driven
  by two separate always @(posedge clk) blocks (rs_syndrome.v:58 and
  :72/:75). This is a real multiple-driver situation that hardware synthesis
  tools also reject; EBMC is correct to error.

• 11 koios circuits (attention_layer, clstm_like_small,
  clstm_like_medium, conv_layer, conv_layer_hls, dla_like_small,
  dla_like_medium, eltwise_layer, spmv, tpu_like_small_os,
  tpu_like_small_ws) — all conflict on a .ram array inside a true
  dual-port RAM (two write ports, ram[address_a] <= data_a and
  ram[address_b] <= data_b, in two separate clocked blocks, non-constant
  indices). EBMC models array writes as a single per-signal "next value"
  (last-writer-wins), so it cannot represent two independent write ports; the
  conflict check is honestly reporting that limitation. Suppressing it would
  silently drop one write port and produce a semantically wrong model, so these
  are left failing. Real multi-write-port memory support is a separate, larger
  enhancement.

Regression tests

regression/verilog/shared-integer-loop-variable/:

• two_combinational_blocks — shared integer counter in two always @(*)
  (models crossbar / the koios loop-counter idiom);
• combinational_and_clocked — shared integer counter in a combinational and
  a clocked block (models viterbi/qr).

Both PROVED after the fix and would previously have hit the conflict errors.
make -C regression/verilog test passes (no other tests regress; no existing
test relied on the removed conflict behaviour).

Known follow-up (out of scope here)

After the fix, blocks/viterbi gets past the conflict error but its synthesis
is very slow/heavy (min-path-metric logic explodes into a large WITH/wire
network), so it may still not pass CI within resource limits. That is a
separate synthesis-performance issue, not a driver-conflict one, and is not
addressed in this PR.