[Knowledge Gap] mandelbrot.sv - SInt slice preserves sign but Verilog treats slices as unsigned

[soronpo]

Knowledge Gap

Source file: mandelbrot.sv (projf-explore Mandelbrot set demo)

What it does: Fixed-point Mandelbrot set iterator that extracts the integer part of a signed fixed-point number.

Gap Description

The Verilog code extracts the top FP_INT bits of a signed FP_WIDTH-bit fixed-point value and compares them to a threshold:

logic signed [FP_WIDTH-1:0] xy2;
if ((xy2[FP_WIDTH-1-:FP_INT] <= 4) && ...)

In Verilog, a bit-slice sig[hi:lo] on a signed signal produces an unsigned result. The comparison <= 4 is unsigned.

In DFHDL, the type-system docs state: "Slicing preserves the source type" — SInt → SInt. So the natural translation:

val xy2 = SInt(FP_WIDTH) <> VAR
val xy2_int = xy2(FP_WIDTH - 1, FP_WIDTH - FP_INT)  // returns SInt(FP_INT)
if (xy2_int <= 4 && ...)  // signed comparison — WRONG semantics

This compiles fine but produces incorrect behavior relative to the Verilog, because it uses a signed comparison where Verilog uses unsigned. For example, if the integer part bits are 1000 (value 8 unsigned, or -8 signed), the Verilog condition <= 4 is false (8 > 4), but the DFHDL condition <= 4 is true (-8 < 4). This caused formal verification to fail with 29 unproven $equiv cells.

The fix is to explicitly convert to unsigned before comparing:

val xy2_int = UInt(FP_INT) <> VAR
process(all):
  xy2_int := xy2(FP_WIDTH - 1, FP_WIDTH - FP_INT).bits.uint

What documentation would have helped

1. The Part-Select Notation section in from-verilog already notes that slicing preserves the source type. It should add a warning about Verilog's semantics difference: in Verilog, a part-select on a signed variable is treated as unsigned in comparisons. Users must explicitly convert with .bits.uint when the Verilog uses a signed slice in an unsigned context.

2. A table entry or note in the Part-Select section:

   Verilog	DFHDL	Notes
   sig[hi -: W] <= N (signed sig)	sig(hi, hi-W+1).bits.uint <= N	Verilog treats slice as unsigned even if sig is signed

Discovered during: mandelbrot-1 learner run — formal verification (Yosys) found 29 unproven cells before this fix was applied.