Encoding and Decoding Functions

Part II · Module 22 · Chapter 22.5 · Encoding and Decoding Functions

1. The Appeal of a Pair

Chapter 22.4's CRC is a one-way function: the testbench computes it and compares against something. Many imports come in pairs instead — encode and decode, pack and unpack, serialise and parse — and a pair offers something a single function cannot:

Feed a value through both and you should get the value back.

No reference data, no expected-value table, no specification lookup. For a small enough domain you can do it exhaustively, which feels like proof.

This chapter builds three pairs, puts the same checks through all three, and measures exactly what the round trip establishes.

2. The Codec and the Three Pairs

A deliberately tiny field codec, small enough to exhaust: a 4-bit value becomes a 7-bit codeword.

  format: bits 6:5 = tag 0b10
          bit 4    = even parity of the value
          bits 3:0 = the value

uint8_t codec_encode(uint8_t v4) {
    v4 = (uint8_t)(v4 & 0x0Fu);
    uint8_t p = parity4(v4);
    return (uint8_t)((0x2u << 5) | (p << 4) | v4);
}
int codec_decode(uint8_t c7) {
    if (((c7 >> 5) & 0x3u) != 0x2u) return -1;         /* wrong tag */
    uint8_t v = (uint8_t)(c7 & 0x0Fu);
    if (((c7 >> 4) & 1u) != parity4(v)) return -1;     /* parity mismatch */
    return (int)v;
}

Three versions, so every check can be scored against all three:

• The correct pair — the code above.
• A symmetric bug — both encoder and decoder use tag 0b01 instead of 0b10. Perfectly self-consistent; wrong on the wire.
• An asymmetric bug — the encoder is correct, and the decoder reads the value field three bits wide instead of four.

3. What the Round Trip Catches

Measured, encode-then-decode over the entire input domain, all sixteen values:

  good pair  : all 16 values round-trip: yes
  BROKEN pair: all 16 values round-trip: yes   <- and it is still wrong
  ASYMMETRIC bug (good encoder, narrow decoder): round-trips: NO, 8 of 16 fail

The asymmetric bug is caught, and caught decisively — half the domain fails.

The symmetric bug passes exhaustively. Every value in, every value back. And here is what it was doing while passing:

  value : good   broken
    0   : 0x40   0x20
    1   : 0x51   0x31
    2   : 0x52   0x32
    3   : 0x43   0x23
  ... they differ on every single value

Not one codeword in common. A design on the other end of that link receives 0x20 where the format calls for 0x40, and the round trip has nothing to say about it, on any input, ever.

4. The Check That Closes the Gap

The round trip's blind spot has a precise shape, so the fix does too: a reference that comes from outside both functions.

For a CRC that was the published check value (22.4). A field codec rarely has one, so derive a codeword by hand from the format — which takes a minute and cannot inherit a mistake that lives in the code:

  value 5 = 0b0101, parity of 0101 is 0, so the codeword is
    0b10 << 5  |  0 << 4  |  0101   =  0x40 | 0x00 | 0x05  =  0x45

Measured:

  good_encode(5) = 0x45 : match
  bad_encode(5)  = 0x25 : MISMATCH
  value 3 -> derived 0x43 ; good_encode(3) = 0x43 : match
  value 1 -> derived 0x51 ; good_encode(1) = 0x51 : match

Three hand-derived codewords, three matches, and the symmetric bug caught on the first one. That is the entire fix: the round trip stays (it catches asymmetric bugs, which are the more common kind), and a handful of externally-derived values stand beside it.

Note what makes the derivation trustworthy: it was done from the format description, with the arithmetic written out, by a route that does not run any of the three implementations. If you derive your expected value by running the encoder, you are back where you started.

And the same codec.c through the import. Measured:

  round trip over all 16 values through the import: 0 failure(s)
  encode(5) = 0x45 (derived 0x45): match
  encode(3) = 0x43 (derived 0x43): match
  encode(1) = 0x51 (derived 0x51): match

5. The Finding, Stated Exactly

A round trip proves that the two functions agree with each other. It proves nothing about what either of them does.

That is not a weakness to be compensated for with more stimulus. For a symmetric bug the two errors cancel by construction, on every input, so exhaustive coverage of the domain — which §3 actually performed — changes nothing. The check is not weak; it is measuring a different property than the one you want.

Which is worth putting beside what each check is for:

• A round trip answers "are these two consistent?" — and catches an asymmetric bug, measured, 8 of 16 failures.
• An externally derived value answers "is this the right format?" — and catches a symmetric bug, measured on the first value tried.

Both are cheap. Neither substitutes for the other, and a suite with only the first is in exactly the position Chapter 18.2 described: passing, confidently, on a question nobody asked.

6. The Misconception: It Is Exhaustive, So It Is Proof

"I round-tripped every value in the input domain. All sixteen. There is nothing left to test."

Measured false. The symmetric pair round-tripped all sixteen and produced the wrong codeword for all sixteen.

Exhaustiveness is a property of the stimulus, and it is a genuine strength — but it says nothing about whether the property being checked is the one that matters. Exhaustive over the wrong property is still the wrong property, and the confidence that comes with the word "exhaustive" is what makes this the dangerous version of the mistake.

Three ways to see that the trap is structural rather than a matter of care:

The errors cancel by construction. The encoder writes tag 0b01; the decoder accepts tag 0b01. There is no input for which that disagrees, because it is the same constant in both places.

More stimulus cannot help, since the domain was already complete. This is the only situation in verification where "run more vectors" is provably useless.

And it generalises past codecs. Pack and unpack, serialise and parse, compress and decompress, transmit and receive models written by the same person from the same paragraph — every pair checked only against itself has this hole, in the same shape.

The accurate position:

Keep the round trip; it is cheap and it catches the asymmetric bugs, which are the common ones. Then add a small number of values derived from the format by hand, because that is the only check in the set that did not come from the code it is checking.

7. What You Should Be Able to Say Now

1. A pair can be checked against itself — encode, decode, compare — with no reference data, exhaustively for a small domain.
2. Measured, a round trip catches an asymmetric bug: 8 of 16 failed when only the decoder was wrong.
3. Measured, it passes a symmetric bug exhaustively: 16 of 16, while every codeword differs from the correct one.
4. The errors cancel by construction, so more stimulus is provably useless.
5. Derive a reference by hand from the format — 0b10 << 5 | 0 << 4 | 0101 = 0x45 — and it cannot inherit a mistake in the code.
6. Measured: three derived codewords, three matches; the symmetric bug caught on the first.
7. The same codec.c through the import gives the same answers — round trip 0 failures, 0x45/0x43/0x51 all matching.
8. A bare acceptance count distinguishes nothing — measured, all three decoders accept 16 of 128; the good and symmetric sets are disjoint.
9. A live instance of 22.2 §5: comparing the call directly gave 128 of 128; through a signed destination, 16 of 128. Nothing reported it.
10. What caught that was an expectation written down in advance, not a tool (21.8's conclusion).
11. Exhaustive over the wrong property is still the wrong property.

8. Exercises

1. Write an encode/decode pair and round-trip the whole input domain. What have you established, stated as precisely as §5 does?
2. Introduce a symmetric bug — change a constant in both functions. Does the round trip still pass? Over how much of the domain?
3. Introduce an asymmetric bug. How much of the domain fails, and why is that fraction informative?
4. Derive one codeword by hand from your format, writing out the arithmetic. Run it against both the correct and the symmetric pair.
5. Why must the derivation not use the encoder? Describe the failure of a "reference" produced by running the code.
6. Count how many of the possible codewords your decoder accepts. Is the count what you expected? Now compare the accepted sets between two implementations.
7. Reproduce §5's testbench bug: compare a function returning -1 against zero without a signed destination. What count do you get, and what would have made you notice?
8. List the function pairs in a project you know that are checked only against each other. For each, write the one externally-derived value you would add.

9. Summary

• A pair checks against itself — cheap, needs no reference, exhaustive for a small domain.
• Measured: the round trip catches an asymmetric bug (8 of 16 fail) and passes a symmetric one (16 of 16) whose every codeword is wrong.
• The errors cancel by construction — more stimulus is provably useless.
• Derive a codeword by hand from the format: 0x45, 0x43, 0x51 — measured, all three match, and the symmetric bug is caught on the first.
• The same codec.c through the import gives the same answers.
• A bare acceptance count distinguishes nothing — measured 16 of 128 for all three; the good and symmetric sets are disjoint.
• A live 22.2 instance: 128 of 128 comparing the call directly, 16 of 128 through a signed destination, with nothing reported.
• What caught it: an expectation written down in advance.
• Exhaustive over the wrong property is still the wrong property.
• Keep the round trip; add a few externally derived values.

A codec moves one small value at a time, which keeps every question about it small. Give the same import a buffer to work on and the questions from Module 21 come back at once — how long it is, who owns it, and whether the function is allowed to write where it is reading.