An Arithmetic Reference Model

Part II · Module 24 · Chapter 24.6 · An Arithmetic Reference Model

1. Three Places a Clause Has to Choose

Modelling arithmetic in C is not hard; Module 3 covered the conversions. What makes an arithmetic model difficult is that three operations have no single correct answer until a specification picks one:

• Rounding — at least five readings, all defensible.
• Saturation — at which bounds, and symmetrically or not.
• Overflow — what happens when the intermediate does not fit.

This chapter is about writing those three down and about what it costs to read the clause differently from the design's author. The running example's clause S4 is the test case, and it is deliberately well written:

  S4  The output is the accumulator divided by 16, rounded HALF AWAY FROM ZERO.
      (+8 and above rounds up; -8 and below rounds down.)

The parenthesis is doing real work. Without it the clause would say "rounded", and §2 is what that word covers.

2. One Word, Five Implementations

Measured, the same accumulator values through five functions that all deserve the name:

  acc  | half away | half up | trunc | floor | half even
    24 |       2   |     2   |    1  |    1  |      2
     8 |       1   |     1   |    0  |    0  |      0
     4 |       0   |     0   |    0  |    0  |      0
     0 |       0   |     0   |    0  |    0  |      0
    -4 |       0   |     0   |    0  |   -1  |      0
    -8 |      -1   |     0   |    0  |   -1  |      0
   -24 |      -2   |    -1   |   -1  |   -2  |     -2
   -40 |      -3   |    -2   |   -2  |   -3  |     -2
    40 |       3   |     3   |    2  |    2  |      2

Every column is a reasonable thing to mean by "rounded":

• Half away from zero — the clause's choice. -8 goes to -1.
• Half up — ties go toward positive infinity. -8 goes to 0.
• Truncate toward zero — what plain C division does (Chapter 22.3 §2 measured it).
• Floor — what an arithmetic right shift does. -4 goes to -1, not 0.
• Half to even — ties go to the even neighbour. 8 goes to 0, 24 goes to 2.

Note the fourth row. A design implementing the divide as acc >> 4 — the obvious hardware choice — has chosen floor, and floor and truncation differ on every negative value with a remainder.

3. The Finding: The Near Misses Are the Quiet Ones

Measured, each alternative against the specified behaviour, over all 4096 accumulator values:

  half up   differs on  128 (3.1%)
  truncate  differs on 2048 (50.0%)
  floor     differs on 1920 (46.9%)
  half even differs on  128 (3.1%)

The ordering is the point, and it inverts the usual intuition about severity.

The two readings closest to correct are the two hardest to find. Half up and half-to-even differ from the specification only at half-way points — 128 values out of 4096, 3.1%. A random stimulus hits one about one time in thirty-two, and a directed test that does not deliberately target exact half-way values may never hit one at all.

The two you get by accident are loud. Truncation is what you get by writing /, and floor is what you get by writing >>. They differ on about half the range, so almost any stimulus finds them in the first few transactions.

So the error made by someone being careless is obvious, and the error made by someone being careful but reading one word differently is nearly invisible. That is worth stating plainly because it is the opposite of how review effort usually gets allocated.

And one more measurement that halves the detection surface again:

  of the 2048 values where truncation differs, 1024 are negative (50%)
  -> a test that only drives positive samples cannot see it

4. Saturation and Overflow

The other two choices, more briefly, because each has one decision in it.

Saturation — clauses S1 and S3 fix the bounds at +2047 and -2048. The asymmetry is deliberate: a signed 12-bit value has one more negative code than positive, and a specification has to say whether the low bound is the type's minimum or the negative of the high bound.

Chapter 24.2 measured what getting that one value wrong costs. The sat_acc_bug design saturates the low bound at -2047 instead of -2048, and over seventy checks it produced 2 mismatches, first at check 28. One number, one code, and a bug that 68 of 70 checks did not notice.

Overflow — the model must not overflow where the specification says saturate:

int32_t sum = m->acc + (int32_t)sample;   /* widened before adding */
m->acc = sat(sum, -2048, 2047);           /* then saturated */

The addition is done in int32_t, where a 12-bit value plus an 8-bit value cannot overflow, and the saturation happens afterwards. That is a deliberate choice rather than an accident: signed overflow in C is undefined behaviour (Chapter 13.2), so a model that lets the intermediate wrap is relying on something the language does not provide — and Chapter 21.8 measured that sanitizers do not help with values that stay inside their storage.

The rule, which is the same one Chapter 20.5 §5 reached for unknown values: widen, compute, then clamp. Never clamp by letting something wrap.

5. The Misconception: Rounding Differences Are Only Off by One

"Even if the model and the design round differently, it is one LSB. That is not worth holding a release for."

Two replies, and the second is the one that costs time.

One LSB of the output is not one LSB of the quantity. In this block the output is the accumulator divided by sixteen, so a one-LSB output difference is a sixteen-LSB difference in the accumulated value. Whether that matters is a question for whoever wrote the specification, and the fact that it is expressible in a small number does not answer it.

And the scoreboard does not care how small it is. A model and a design that round differently disagree permanently, on 3.1% of inputs, for as long as both exist. That is not a one-off discrepancy to be waved through — it is a scoreboard that fires every thirty-two transactions or so, forever.

Chapter 24.4 §5 measured what that does to a team: a recurring mismatch with no obvious pattern gets triaged as flaky, then as expected, and the scoreboard's reports stop being read. The cost is not the one LSB; it is that the next real bug arrives into a channel nobody trusts.

The accurate position:

A rounding disagreement is not a small error, it is a permanent one. Resolve it by deciding what the clause means — and then either the design changes, the model changes, or the specification gets the parenthesis that S4 already has.

6. What You Should Be Able to Say Now

1. Three places a clause must choose: rounding, saturation, overflow.
2. "Rounded" covers at least five implementations, all defensible — half away from zero, half up, truncate, floor, half to even.
3. Measured, against the specified reading over all 4096 values: half up 128 (3.1%) · half to even 128 (3.1%) · truncate 2048 (50%) · floor 1920 (46.9%).
4. The finding: the two readings closest to correct are the two hardest to catch; the two that differ on half the range are what / and >> give you by accident.
5. A positive-only stimulus halves the surface again — measured, 1024 of 2048 truncation differences are negative.
6. Saturation bounds are asymmetric by nature — a signed 12-bit value has one more negative code, and the clause has to say which bound is which.
7. Measured (24.2): a one-code saturation error showed in 2 of 70 checks, first at check 28.
8. Widen, compute, then clamp — signed overflow is undefined (13.2), so never clamp by letting something wrap.
9. Write a boundary table by hand before the code: it forces the ambiguity out, validates the oracle without the design, and gives the stimulus a target.
10. A rounding disagreement is permanent, not small — 3.1% of inputs, forever, and it trains a team to ignore the scoreboard.

7. Exercises

1. Implement all five roundings and reproduce the table in §2. Which rows separate which pairs?
2. Count how often each differs from "half away from zero" over your full input range. Do you get 3.1% for the two tie-breaking variants?
3. Why do truncation and floor agree on positive values and differ on negatives? Answer from the definitions, not the measurement.
4. Write acc >> 4 and acc / 16 in C for a negative acc. Which rounding has each chosen?
5. A specification says only "rounded". Write the parenthesis that S4 has, and say which of the five you chose and why.
6. Produce the boundary table for an arithmetic clause in your own work. How many rows, and how many did you have to ask someone about?
7. A design saturates at the negative of its positive bound. How many of your tests would notice? Compare with §4's 2 of 70.
8. §5 says the cost is not the LSB. Describe the sequence by which a 3.1% disagreement stops being reported at all.

8. Summary

• Rounding, saturation and overflow are where a clause must choose.
• Five readings of "rounded", all defensible.
• Measured over all 4096 values: half up 3.1% · half to even 3.1% · truncate 50% · floor 46.9%.
• The near misses are the quiet ones; / and >> give you the loud ones by accident.
• Positive-only stimulus halves the surface — 1024 of 2048 truncation differences are negative.
• Saturation bounds are asymmetric, and a one-code error showed in 2 of 70 checks (24.2).
• Widen, compute, then clamp — signed overflow is undefined behaviour.
• Hand-derive a boundary table before writing code: it exposes the ambiguity, validates the oracle, and aims the stimulus.
• A rounding disagreement is permanent, not small — and its real cost is a scoreboard nobody reads.

Arithmetic has one answer per input once the clause is pinned down. A transformation has two halves that must agree with each other and with a layout on the wire — which brings back a technique from Chapter 22.5 along with the precise limit that was measured on it.