Reusing Existing C Libraries in Verification

Part II · Module 18 · Chapter 18.3 · Reusing Existing C Libraries in Verification

1. The Cheapest Independence

Chapter 18.2 established that a reference model is worth having in proportion to its independence from the design, and measured what happens without it: a model derived from the design passed all 4096 of its tests while the design was broken.

Independence is expensive to manufacture. It requires a separate author, a separate reading of the specification, and the discipline not to converge the model onto the design every time they disagree.

An existing implementation gives you it for free. A CRC routine from a published library, a reference cipher implementation, a codec from the body that standardised it — none of these came from your project, your reading of the specification, or your designer. They were written by someone else, for someone else, and have been exercised by people whose bugs you will never see.

That is the reason to adopt one, and it is a stronger reason than saving time. Saving time is a bonus; the independence is the point.

The rest of this chapter is the two questions that decide whether a given library is actually an oracle for your design, and what you take on by adopting it.

2. Valid for What?

A library is not valid or invalid in itself. It is valid for a particular specification, and the question is whether that is the specification your design implements.

This sounds obvious and is routinely got wrong, because names are reused. Here are four algorithms that all call themselves CRC-8, implemented from one parameterised routine so that only the parameters differ:

static uint8_t crc8_generic(const uint8_t *d, unsigned n,
                            uint8_t poly, uint8_t init,
                            int refin, int refout, uint8_t xorout);

Each checked against its published check value — the CRC of the ASCII string "123456789", which every catalogued variant publishes:

variant             computed  published  match
CRC-8/SMBUS          0xF4      0xF4      yes
CRC-8/MAXIM-DOW      0xA1      0xA1      yes
CRC-8/ROHC           0xD0      0xD0      yes
CRC-8/ITU            0xA1      0xA1      yes

All four implemented correctly. Now the same three bytes, "ABC", through each:

CRC-8/SMBUS        0x52
CRC-8/MAXIM-DOW    0x34
CRC-8/ROHC         0xE3
CRC-8/ITU          0x07

Four completely different answers. Not off by one, not a byte-order difference — unrelated values.

So "we used a standard CRC-8 library" says nothing about what your code computes. The variants differ in five parameters — the polynomial, the initial value, whether input bits are reflected, whether the output is reflected, and a final XOR — and getting any one of them wrong produces a checker that disagrees with the design on essentially every input.

The useful form of the question is therefore not "is this library good?" but:

Does this implement the same specification, with the same parameters, that my design implements?

3. The Check Value, and Why It Is Not Enough

The standard mechanism for confirming you have the right variant is the published check value, and §2 used it: compute the algorithm over "123456789" and compare against the catalogue.

It is necessary. It is not sufficient, and the table above contains the proof.

check vector "123456789" : MAXIM-DOW 0xA1, ITU 0xA1   -> SAME
the bytes    "ABC"       : MAXIM-DOW 0x34, ITU 0x07   -> DIFFERENT

Two genuinely different algorithms agree on the published check vector. MAXIM-DOW uses polynomial 0x31 with input and output reflection; ITU uses polynomial 0x07 with no reflection and a final XOR of 0x55. They have almost nothing in common, and on the one vector everybody tests with, they produce the same byte.

A single matching value is a coincidence waiting to happen — one byte of output has 256 possibilities, and a catalogue of CRC-8 variants has more than 256 entries. So:

Check more than one vector. The empty input, a single zero byte, a single 0xFF, a long run, and some real data from your specification. Agreement across five dissimilar inputs is strong evidence; agreement on one is weak.

Prefer vectors from your own specification. If the document that describes your design gives a worked example — "for this frame the CRC is 0x3A" — that is worth more than any catalogue value, because it tests the thing you actually care about: that the library agrees with your document.

Record the parameters, not the name. CRC-8/SMBUS is a name someone else assigned. poly=0x07 init=0x00 refin=false refout=false xorout=0x00 is what your design implements, and it is checkable against the RTL and against the library's own documentation.

4. The Other Validity Question: What Was It Tested For?

A library that implements the right specification can still be the wrong oracle, for a reason that has nothing to do with correctness.

It may not be exercised in the range you care about. A compression library used for megabyte files is thoroughly tested there and may have had very little exercise with a four-byte input — which is exactly the case your design has to handle. The library's reputation was earned in a region you are not using.

It may have been adapted. A library pulled from a vendor's SDK, or from another project in your company, may have been modified. A model that has been patched by three teams is not the independent artefact you wanted — it is Chapter 18.2's model B with a wider distribution.

Its edge-case behaviour may be undefined rather than specified. What the library does with a zero-length input, a null pointer, or a length exceeding its buffer may be whatever its author's test cases happened to exercise. Your design has defined behaviour there, given by your specification; the library may not.

The practical response is the same for all three: test the oracle on your edges before trusting it. Run it over the inputs your specification calls out specially — zero length, maximum length, all-zeros, all-ones — and confirm it does what your document says. That is a short task and it converts an assumption into a measurement.

5. What You Take On

The purpose of this chapter names obligations, and there are four. None is heavy; all of them are skipped.

Pin the version. A library that is updated underneath you can change behaviour at an edge, and your regression will report it as a design failure. Vendor it into your repository, or pin an exact version, and record which.

Record the parameters and the provenance. Where it came from, which variant, which version, and which document you checked it against:

/* CRC-8 oracle for the frame checksum.
   Source : public-domain reference implementation, vendored 2026-03, unmodified.
   Variant: poly=0x07 init=0x00 refin=false refout=false xorout=0x00
            (CRC-8/SMBUS; check value for "123456789" is 0xF4)
   Checked against: protocol spec rev 2.1 §6.4 worked example (0x3A). */

That comment answers every question §2 to §4 raised, and a reviewer can verify each line without reading the RTL — the same property Chapter 18.2 §5 asked of a reference model.

Keep it unmodified, or stop calling it independent. The moment you patch an adopted library to make a test pass, it has become your code and you have spent the independence you adopted it for. If a patch is genuinely needed — a portability fix, a build integration — keep it minimal, keep it in a separate patch file, and document it.

Check its licence. A reference implementation from a standards body, a GPL library, and a vendor's SDK carry different obligations, and "it is only in the testbench" is not a legal distinction. This is the one obligation that is nobody's favourite and the one most likely to matter to someone outside your team.

6. When Not to Adopt

Three cases where writing it yourself is the better answer.

When the algorithm is trivial. A parity bit, a simple accumulator, a field extraction. The twenty lines you would write are easier to check against the specification than a dependency is to vet, and Chapter 18.2 §5's argument applies — a model should be simpler than the design.

When no implementation matches your specification. A proprietary protocol, or a standard your design extends. Adopting the closest available variant and patching it is the worst of both: the cost of a dependency and none of the independence.

When the library's complexity exceeds the design's. If a model is harder to understand than the RTL, it has the same probability of being wrong and you cannot tell which one failed. This is 18.2 §6's rule — not an implementation — and it applies to adopted code as much as to written code.

7. The Misconception: A Trusted Library Is a Valid Oracle

"It is a well-known, widely-used library. It is correct, so it is a valid oracle."

Correctness and validity are different properties, and only one of them is about the code.

Correctness is whether the library does what it says it does. All four implementations in §2 are correct — each matched its published check value.

Validity is whether what it does is what your design is specified to do. A flawless CRC-8/ROHC implementation used to check an SMBUS design is wrong on essentially every input, and its flawlessness contributes nothing.

The measured form of the correction:

"ABC" under SMBUS : 0x52
"ABC" under ROHC  : 0xE3

Both correct. One of them is your oracle and the other is a bug report generator.

So the question to ask of any adopted implementation is never "is this trustworthy?" It is:

Which specification does this implement, with which parameters, and is that mine?

And the follow-up, which §3 measured the need for: how many independent vectors have I checked it on? One is not enough — MAXIM-DOW and ITU agree on the only vector most people test.

8. What You Should Be Able to Say Now

1. An adopted implementation is the cheapest independence available — it demonstrably did not come from your project's reading of the specification. That is the reason, not time saved.
2. Validity is about the specification, not the code's quality. The question is whether it implements the same specification your design does.
3. Measured: four implementations all called CRC-8 give 0x52, 0x34, 0xE3 and 0x07 for the same three bytes. The name is not a specification.
4. The five parameters — polynomial, initial value, input reflection, output reflection, final XOR — and any one wrong makes the oracle disagree on nearly every input.
5. A published check value is necessary and not sufficient. Measured: MAXIM-DOW and ITU both give 0xA1 on "123456789" and differ on "ABC".
6. Check several dissimilar vectors, and prefer worked examples from your own specification over catalogue values.
7. Record the parameters, not the name.
8. Reflection is bit order, not byte order — it is a property of the algorithm and is the same on every host. A byte-order bug moves between machines; a reflection bug does not.
9. Four obligations: pin the version · record parameters and provenance · keep it unmodified or stop calling it independent · check the licence.
10. Do not adopt when the algorithm is trivial, when nothing matches your specification, or when the library is more complex than the design.

9. Exercises

1. Implement the parameterised CRC-8 from §2 and reproduce all four published check values. Then reproduce the four different "ABC" results.
2. Find a fifth CRC-8 variant in a published catalogue, add it, and confirm its check value. Does it collide with any of the four on "123456789"?
3. Pick the variant your own project uses, or one at random, and write the provenance comment from §5 for it.
4. Take one of the four variants and test it on five dissimilar inputs: empty, one zero byte, one 0xFF, sixteen zero bytes, and a frame from a specification you have. Record which inputs distinguish it from the other three.
5. §3 claims a byte-order bug moves between machines and a reflection bug does not. Explain why, referring to what Chapter 14.3 measured.
6. A colleague has patched an adopted library so a failing test passes. List what the project has lost and the two questions you would ask before accepting it.
7. For a block you know, decide whether an adopted oracle or a written model is right, using §6's three cases. Justify the answer in two sentences.

10. Summary

• An adopted implementation buys independence cheaply — it did not come from your project's reading of the spec. That is the reason.
• Validity ≠ correctness. The question is which specification it implements.
• Measured: four "CRC-8" implementations give 0x52 / 0x34 / 0xE3 / 0x07 for the same bytes. The name is not a specification.
• Five parameters: poly · init · refin · refout · xorout. Any one wrong breaks nearly every input.
• A check value is necessary, not sufficient — measured, MAXIM-DOW and ITU collide at 0xA1 on the usual vector.
• Use several dissimilar vectors, and prefer your own specification's worked examples.
• Record the parameters, not the name.
• Reflection is bit order, not byte order — it does not change between hosts.
• Obligations: pin the version · record provenance · keep it unmodified · check the licence.
• Do not adopt for trivial algorithms, when nothing matches your spec, or when it is more complex than the design.

An adopted oracle and a written model have the same shape: something outside the design that says what the answer should be. The next category is different in kind — code that is not checking the design from outside at all, but running inside it, on the design's own processor, doing what the product will do.