Writing a Model That Is Independent of the RTL

Part II · Module 24 · Chapter 24.3 · Writing a Model That Is Independent of the RTL

1. The Failure This Chapter Is Named After

Chapter 24.1 stated independence as an obligation and gave its headline cost. This chapter is about how the obligation actually gets broken, which is never by anyone deciding to break it.

The failure has a precise shape: the model reproduces the design's own mistake, so the comparison passes. No alarm, no warning, no diagnostic — a clean run, reported as a clean run, on a design that does not meet its specification.

The example is real and is worth looking at, because it is the kind of mistake that gets written rather than one invented for a tutorial.

2. The Design's Bug

sum = acc + {{5{sample[7]}}, sample};

The author sign-extended the 8-bit sample to 13 bits by hand and added it to the accumulator. It looks careful — the replication of sample[7] is exactly the right sign-extension pattern.

A concatenation in Verilog is always unsigned, and one unsigned operand makes the whole expression unsigned. So acc is read as a 12-bit unsigned value, the addition is unsigned, and the saturation comparisons that follow are testing the wrong quantity.

This is a well-known Verilog trap and it is not hypothetical here: I hit it by accident while writing the supposedly clean DUT for this module. The first version of the design in the previous chapter's figure had this bug, and it was found by the model — which is the module's architecture doing the job it exists for, on its own author.

3. Two Models, One Design

Now the model. Writing one from SPEC.txt gives Chapter 24.1 §2's function. Writing one by reading the RTL — line by line, faithfully, the way it is done when the specification is thin and the Verilog is right there — gives something that transcribes the unsigned concatenation along with everything else.

Measured, both pointed at the same buggy design, over the same seventy checks:

  judged by the model written from the SPEC : 70 checks, 51 mismatch(es)
  judged by the model written from the RTL  : 70 checks,  0 mismatch(es)

Fifty-one against zero. Both are C. Both compile clean under -Wall -Wextra -Wpedantic. Both are a different language from the design, written in a different file, compiled by a different compiler.

One of them is an oracle and the other is a photocopier.

4. The Finding: The Cheapest Test Cannot Tell Them Apart

The obvious question is how a model like that survives long enough to be trusted. The answer is measurable, and it is stronger than "it is unlikely to be caught".

Measured, every possible single sample from reset:

  all 256 single samples from reset: 256 agree, 0 differ
  -> a one-sample test cannot distinguish the two models at all

All 256. That is the entire domain, not a sample of it. A test that drives one transaction from reset and checks the answer is provably incapable of telling the two models apart — not unlikely to, unable to, for every input it could possibly use.

And one transaction later, measured over the whole 256 × 256 domain:

  65536 two-sample sequences: 32768 agree, 32768 differ (50.0% differ)

Exactly half. The cliff is between the first transaction and the second.

Driving toward the bound shows it directly:

  step 1: spec acc  -128 out   -8 | rtl acc  -128 out   -8  agree
  step 2: spec acc  -256 out  -16 | rtl acc  2047 out  127  DIFFER

This is the pattern this track has now measured six times — the array models that are byte-identical for 8-bit elements (21.2), the zero-based range (21.5), the symmetric matrix (21.6), the symmetric codec bug (22.5), the one-stream state designs (22.7) — and it is the only one where the common case's blindness is proven exhaustively rather than observed on an example.

5. How Independence Leaks

None of these involves copying code, which is why "we didn't copy the RTL" is not a defence.

Reading the RTL to resolve a specification ambiguity. The spec is vague about a corner, the Verilog answers it immediately, and the question is settled by the artefact under test. §7 is about why this is the worst possible place to look.

Debugging the model until it agrees. A mismatch is investigated, the design turns out to be defensible, and the model gets "fixed". Repeat for a few months and the model is a slow transcription of the design. This is the commonest route and Chapter 24.9 is about handling it without producing it.

One person writing both from the same reading. Chapter 22.5 §3 measured this for an encoder and decoder written as a pair: both wrong in the same direction, round-tripping perfectly over the whole input domain. The same mechanism applies to a model and a design written by one person from one reading of one paragraph.

Calibrating against an early run. The model is written, the DUT is run, the outputs are compared, and the differences are reconciled "to get a baseline". The baseline is the design.

And the defences, each checkable by a person rather than a tool:

• Name the clause on every line — Chapter 24.1 §2's comments. A line that cannot name one is a decision the model made alone, and those lines are where leaks live.
• Write the model before reading the RTL, and record that you did.
• Have a different person write the model, or at minimum write it from the specification in a session where the RTL is not open.
• When the spec is ambiguous, change the spec — §7.

6. The Misconception: From the Spec, Checking the RTL Where It Is Unclear

"We will write the model from the specification. Where the specification is unclear, we will look at the RTL to see what was intended."

This sounds like a reasonable compromise and it is the leak, stated as a plan.

Where the specification is unclear is exactly where the design's behaviour is unverified. Every clause the spec states clearly is a clause two people can check independently. Every corner it leaves open is a corner where the design made a choice that nobody has checked — and the model is the only thing that could have checked it.

So consulting the RTL there removes the check precisely where it was the only one available. The model becomes correct everywhere it did not matter and silent everywhere it did.

Three replacements, in order of preference:

Change the specification. An ambiguity found while writing a model is a specification bug, discovered early and cheaply by exactly the activity that should discover it. Write the clause, get it agreed, implement it.

Make the model's assumption explicit and loud. If the ambiguity cannot be resolved in time, the model should implement a stated choice with a comment naming it as unspecified — and ideally report when the DUT exercises that corner, so the count is known.

Or decline to check that corner. A model that explicitly does not judge a case is far better than one that silently judges it the design's way. Chapter 20.5 §5 made the same argument for four-state values: refusing is a result, and a model that computes on something it cannot justify is producing fiction.

The accurate position:

The RTL may never be an input to the model, and "only where the spec is unclear" is the worst possible exception, because that is the only place the model was the sole check. An ambiguity is a specification defect; fix it there.

7. What You Should Be Able to Say Now

1. The failure is silent: the model reproduces the design's mistake and the comparison passes, with no diagnostic anywhere.
2. The design's bug is a real Verilog trap — a concatenation is always unsigned, and one unsigned operand makes the whole expression unsigned. I wrote it by accident building this module's "clean" DUT.
3. Measured, the headline: 51 mismatches against 0, same design, same 70 checks, two C models.
4. The finding, exhaustive: across all 256 single samples from reset the two models agree on every one — a one-sample test is provably unable to tell them apart.
5. The cliff is one transaction wide — measured, 32768 of 65536 two-sample sequences differ, exactly 50%.
6. A transcription is not reliably faithful either — measured, 22 mismatches from a version with one wrong width, which would have reported 22 bugs that were not bugs.
7. So an RTL-derived model is a third artefact, agreeing with neither the spec nor the design.
8. Four leaks: resolving an ambiguity from the RTL · debugging the model until it agrees · one person writing both · calibrating against an early run.
9. Four defences: name the clause on every line · write the model first and record it · a different author · fix the specification.
10. "Check the RTL where the spec is unclear" is the leak as a plan — that is the only place the model was the sole check.
11. Sixth instance of the common case that cannot fail, and the only one proven exhaustively.

8. Exercises

1. Write a model from a specification, then write a second one by transcribing an implementation. Compare them over one input from reset, then over two.
2. For the running example, explain why 256 of 256 single samples agree. What is it about the first transaction that hides the difference?
3. Why does the two-sample domain split exactly in half? Work it out from the bug rather than from the number.
4. Take a model you have and mark every line with the specification clause it implements. What fraction cannot be marked?
5. §5 lists four leaks. For each, describe what a reviewer could ask that would detect it.
6. Your specification is silent on a corner the design clearly handles somehow. Write down the three options from §6 and say which you would take and why.
7. A colleague reports that their model and the RTL agreed on 10,000 random transactions. What single question does this chapter suggest, and what answer would worry you?
8. Reproduce the transcription error from §4's callout — change a width in a transcribed model — and count the mismatches it produces. What would you have concluded from them without this chapter?

9. Summary

• The failure is a clean run on a non-conforming design.
• The design's bug is a real Verilog trap — an unsigned concatenation — written by accident while building this module.
• Measured: 51 mismatches against 0, same design, same 70 checks.
• Exhaustively: all 256 single samples from reset agree — a one-sample test is unable to distinguish the models.
• One transaction later: 32768 of 65536 differ, exactly 50%.
• A transcription is not reliably faithful — measured 22 mismatches from one wrong width; a third artefact agreeing with neither.
• Four leaks: ambiguity from the RTL · debugging until it agrees · one author · calibrating on a run.
• Four defences: name the clause · model first · different author · fix the spec.
• "Only where the spec is unclear" is the worst exception — that is where the model was the sole check.

An independent model exists. Nothing yet connects it to the design's output, pairs its answers with the right transactions, or decides who owns the data at each step — and those are the decisions that turn a correct model into a correct comparison.