[Clarification] - Zvabd: Clarification on the Signedness of Instruction Results

[xxfl990]

Summary

Thanks for the recent revision. Moving the difference into unbounded integers
and applying abs_int makes the intermediate widths much easier to follow.

One point I could not settle from the current text is that every instruction’s
source operands are qualified as signed or unsigned, whereas the destination is
qualified only by width. This leaves three related questions:

1. What does vabs.v produce for the most negative input,
   -2^(SEW-1)—for example, -128 when SEW=8?
2. What do vabd.vv and vabdu.vv produce when the difference reaches
   2^SEW - 1—for example, 255 when SEW=8?
3. How do vwabda.vv and vwabdau.vv behave when the accumulator exceeds
   the range of a 2*SEW-bit value?

My reading is that the pseudocode already answers (1) and (2), so those cases
may only need a sentence in the normative prose. Case (3) appears to require a
rule of its own. I would be happy to be corrected on any of these points.

(cc @riscv/arc)

---

Specification Reference

Permalink:

https://github.com/riscv/integer-vector-absolute-difference/blob/60b6370c6/src/unpriv/zvabd.adoc#L68

On dev at commit 60b6370c6:

Line	Code
L68	to_bits(SEW, abs_int(signed(vs2_val[i])))
L112	to_bits(SEW, abs_int(signed(vs2_val[i]) - signed(vs1_val[i])))
L161	to_bits(SEW, abs_diff)
L212	to_bits_unsafe(SEW_widen, signed(vd_val[i]) + abs_int(diff))
L264	to_bits_unsafe(SEW_widen, unsigned(vd_val[i]) + abs_diff)

The normative prose I reviewed includes:

• norm:vabs_op (L58): “An absolute value operation is performed on each
  element of vs2.”
• norm:vabd_op (L102) / norm:vabdu_op (L147): the operation is performed
  “between the elements of two signed/unsigned integer SEW-bit source operands
  vs1 and vs2.”
• norm:vwabda_op (L198) / norm:vwabdau_op (L248): the operation
  “accumulates the results into the elements of a 2*SEW-bit integer operand
  vd.”

The sources are consistently qualified as signed or unsigned, while the
destination is qualified only by width. I may have missed an existing
statement, but searching the document for most negative, saturate,
overflow, wrap, and vxsat returned no hits. I therefore believe that the
signedness of the destination is not stated anywhere.

---

Expected vs. Observed

Expected	Observed
A rule stating that vabs.v, vabd.vv, and vabdu.vv produce unsigned SEW-bit results	The destination is qualified only by width.
A defined result for vabs.v applied to -2^(SEW-1)	to_bits(8, abs_int(-128)) = to_bits(8, 128) = 0x80; this is 128 when interpreted as unsigned and -128 when interpreted as signed.
A defined result for vabd.vv at the maximum difference	to_bits(8, 255) = 0xFF, which represents the correct value only when interpreted as unsigned.
Explicit overflow behavior for the widening instructions	to_bits_unsafe is used, although the Sail prelude says that it “should never be used.”

---

(1) and (2): The Pseudocode Appears to Imply Unsigned Results

As far as I can tell, no truncation occurs at L68, L112, or L161.

to_bits
has the following type:

// Convert an integer to bits. This requires that the integer is known to fit
// inside the resulting bit vector. Note this only admits non-negative numbers.
val to_bits : forall 'l 'x, 'l >= 0 & 0 <= 'x < 2 ^ 'l .
              (implicit('l), int('x)) -> bits('l)

All three call sites satisfy this constraint:

• abs_int(signed(bits(SEW))) ranges over 0 .. 2^(SEW-1).
• abs_int(signed(a) - signed(b)) ranges over 0 .. 2^SEW - 1.
• The unsigned abs_diff also ranges over 0 .. 2^SEW - 1.

In every case, the upper bound is less than 2^SEW. These therefore appear to
be exact conversions rather than wrapping conversions:

to_bits(8, 128) = 0x80
to_bits(8, 255) = 0xFF

If this interpretation is correct, the apparent wraparound in case (1) comes
from how the destination is interpreted afterward, rather than from the
operation itself.

abs_int does guarantee a non-negative integer, but at the boundary that
property cannot be preserved by the bit pattern alone: when SEW=8, 128 and
-128 share the bit pattern 0x80. An SEW-bit field has no additional state
with which to carry the intended signedness.

Moreover, choosing to_bits—which “only admits non-negative numbers”—instead
of to_bits_truncate suggests that the pseudocode is already treating the
destination as an unsigned value.

A signed destination also seems difficult to reconcile with vabd.vv, since
an SEW-bit signed value cannot represent 255 when SEW=8. Consequently, a
rule covering only the most-negative vabs.v input would not be sufficient.
This asymmetry is what leads me to believe that unsigned results are intended.

If that is indeed the intent, wording along the following lines might cover
both cases:

[#norm:vabd_result_unsigned]#The results of `vabs.v`, `vabd.vv`, and
`vabdu.vv` are unsigned SEW-bit values. Consequently, when `vabs.v` is
applied to the most negative value -2^(SEW-1), it produces the unsigned
value 2^(SEW-1). These instructions do not saturate and do not modify
`vxsat`.#

This would avoid the need for a separate most-negative rule and would exclude
saturation from the interpretation. That would be consistent with RVV
convention, under which saturating operations have distinct mnemonics—such as
vsadd, vssub, and vnclip—and set vxsat. Neither characteristic applies
here.

---

(3): Possible Ambiguity Around to_bits_unsafe

The widening accumulators appear capable of exceeding the range of a
2*SEW-bit value. Under norm:vwabda_op and norm:vwabdau_op, the source
elements are SEW bits wide, where SEW ∈ {8, 16}, and the destination elements
are 2*SEW bits wide.

For example, when SEW=8:

• For vwabdau.vv (L264):

  unsigned(vd) + abs_diff
  = 65535 + 255
  = 65790
  > 65535
  

• For vwabda.vv (L212):

  signed(vd) + abs_int(diff)
  = 32767 + 255
  = 33022
  

  This exceeds the maximum signed 16-bit value.

This boundary is reachable in ordinary use, not merely in theory. A SAD
reduction over a 16×16 block of 8-bit samples can accumulate up to:

256 × 255 = 65280

That value fits in 16 bits only if the destination is interpreted as unsigned.
If it is interpreted as signed, the number of maximum-difference elements that
can be accumulated without exceeding the positive range is limited to:

floor(32767 / 255) = 128

That is only half of a 16×16 block. Since motion estimation is listed among
the target workloads in the Introduction, it would be useful to state which
interpretation is intended.

Ordinary to_bits therefore cannot be used at these two call sites for every
possible input; some overflow behavior must be selected. This makes the use of
to_bits_unsafe understandable. My only hesitation is the following comment in
the Sail prelude:

// This version should never be used. It is only for migrating code from
// when there was no distinction between checked and truncating to_bits.
val to_bits_unsafe : forall 'l, 'l >= 0 .
                     (implicit('l), int) -> bits('l)

to_bits_unsafe and to_bits_truncate are identical in both signature and
implementation, differing only in that comment. It is therefore unclear
whether the use of to_bits_unsafe here is intended to specify wraparound or
is a placeholder left over from an earlier migration.

If wraparound is intended, stating that behavior in the normative prose and
replacing to_bits_unsafe with to_bits_truncate would make the semantics
unambiguous for implementers.

Thanks for considering these points.