What a Reference Model Must Guarantee

Part II · Module 24 · Chapter 24.1 · What a Reference Model Must Guarantee

1. The Moment a Model Becomes an Oracle

Modules 19 through 23 built the machinery: how a call is declared, how every type crosses, how an array carries what C cannot, who calls whom, and what each side may do while the other waits. This module is what the machinery is for.

The architecture is three parts and a comparison. Stimulus drives the design to an actual result; the same stimulus drives a C model to an expected result; something compares them and reports. Chapter 24.2 draws it properly.

What changes in this module is the model's status. Up to now a C function was a useful thing to call. Here it is an oracle — its answer is treated as correct, and a disagreement is written up as a bug in the design. That promotion is often informal and it comes with obligations, and this chapter is those obligations stated so that each one can be checked.

2. The Running Example

One example runs through this whole module, so it is worth a paragraph.

SPEC.txt rev A — a saturating accumulator with a rounded output, in six numbered clauses:

  S1  The accumulator holds a signed 12-bit value, range -2048 .. +2047.
  S2  On each valid sample the 8-bit signed sample is added to the accumulator.
  S3  If the sum exceeds +2047 the accumulator SATURATES to +2047.
      If the sum is below -2048 the accumulator SATURATES to -2048.
  S4  The output is the accumulator divided by 16, rounded HALF AWAY FROM ZERO.
  S5  The rounded output is then saturated to signed 8 bits, -128 .. +127.
  S6  Reset clears the accumulator to 0.

And the model written from it, with every function naming the clause it implements:

int32_t mdl_step(mdl *m, int8_t sample) {
    int32_t sum = m->acc + (int32_t)sample;                   /* S2 */
    m->acc = sat(sum, -2048, 2047);                           /* S1, S3 */
    int32_t a = m->acc;                                       /* S4: half away from zero */
    int32_t q = (a >= 0) ? (a + 8) / 16 : -(((-a) + 8) / 16);
    return sat(q, -128, 127);                                 /* S5 */
}

The clause comments are not decoration. They are what makes §3's obligation auditable: a reader can check every line against a numbered sentence, and a line with no clause is a line that came from somewhere else.

3. Independence, and What Its Absence Costs

The obligation: the model's authority is the specification. Nothing it knows may have come from the design.

The cost of breaking it is this module's headline measurement. One design with a real bug, two C models, 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. The second model was written by reading the design's own Verilog and transcribing it faithfully into C. It is a different language, in a different file, compiled by a different compiler — and it certifies the broken design as correct.

Head to head on the first three samples:

  sample -128 #1: spec model   -8   RTL-derived model   -8   agree
  sample -128 #2: spec model  -16   RTL-derived model  127   DIFFER
  sample -128 #3: spec model  -24   RTL-derived model  120   DIFFER

They agree on the first sample, which is how this kind of model survives its first test. Chapter 24.3 is about how to avoid writing the second one.

4. Determinism, and Determinism Given What

The obligation: where the specification defines a unique answer, the model must give the same answer every time — otherwise a disagreement is noise and nobody can act on it.

Measured:

  40 outputs, run twice from reset: identical

That is the easy half. The half that is usually left unsaid is in the next two measurements.

A stateful model is deterministic given its starting state, not absolutely. Measured, the same forty samples run again without a reset:

  continuing from the previous run's state: 0 of 40 match the fresh run

None of them. The model did nothing wrong — it accumulated, which is its job. But "the same stimulus" produced forty different answers, because the stimulus was not the same: the accumulator's starting value is an input too, and it is one nobody wrote down.

And order is part of the stimulus. Measured, the same forty samples in reverse:

  the same 40 samples in reverse order: 2 of 40 outputs coincide

Two. So for any model that accumulates, "we drove the same stimulus" has to mean the same values in the same order, and a scoreboard that compares a set rather than a sequence is comparing something else — Chapter 21.6 §4 measured the same confusion for a permuted array.

5. The Misconception: It Is in C, So It Is Independent

"The design is Verilog and the model is C. Two languages, two files, two people — that is independence."

Measured false, and it is the sharpest measurement in the module. model_rtl.c is C. It is compiled by a different compiler from the one that built the design. It lives in a different file, in a different language, and it scores 0 mismatches against a design that the specification-derived model fails 51 times.

Independence is not a property of the medium. It is a property of where the knowledge came from.

Three ways the knowledge leaks across, none of which involve copying code:

• Reading the RTL to resolve an ambiguity. The spec is vague, the design is right there, and the question gets answered by the thing being tested.
• Debugging the model until it agrees. A mismatch is investigated, the design turns out to be defensible, and the model is "fixed" — which is Chapter 24.9's chapter, and the most common route.
• The same person writing both, from the same mental model of the paragraph, which Chapter 22.5 §6 measured as a symmetric bug: both halves wrong in the same direction, agreeing perfectly.

The accurate position:

A model written in C is not golden because it is written in C. It is an oracle when its authority is a specification it did not get from the design — and that is a claim about provenance, which a reviewer can check by asking, of any line, which clause it implements.

6. What You Should Be Able to Say Now

1. A model becomes an oracle when its disagreement is treated as a bug report — an informal promotion with real obligations.
2. Three obligations: independence · determinism where required · a specification rather than an implementation as its authority.
3. The headline: one buggy design, 51 mismatches from the spec-derived model and 0 from the RTL-derived one, over the same 70 checks.
4. They agree on the first sample (-8 and -8) and diverge on the second (-16 against 127), which is how such a model survives its first test.
5. Determinism, measured: 40 outputs identical on a repeat run from reset.
6. But given the starting state, not absolutely — measured, 0 of 40 matched when continuing without a reset.
7. Order is part of the stimulus — measured, 2 of 40 coincided in reverse order.
8. Where the spec is silent the model must not quietly decide — name the clause for every line, and treat a line with no clause as a decision to be agreed.
9. Independence is about provenance, not language — model_rtl.c is C and is not independent.
10. Three leaks: reading the RTL to resolve ambiguity · debugging the model until it agrees · one person writing both.
11. A model that agrees with the design is indistinguishable from a model that is right, and the agreement is what is being used as evidence (18.2).

7. Exercises

1. Write a six-clause specification for something you have modelled, and annotate an existing model line by line with the clause each line implements. How many lines cannot name one?
2. Run a stateful model twice from reset on the same stimulus. Then run it twice without the reset. What do the two experiments establish, separately?
3. Reverse the order of a stimulus sequence through an accumulating model. How many outputs coincide, and what does that say about "the same stimulus"?
4. Take a model you trust and ask, of each behaviour it implements, where you learned it. How many answers are "from the RTL"?
5. §4's callout names three kinds of specification gap. Find one of each in a document you work from.
6. A colleague says their model is independent because it is written in a different language. Construct the one-paragraph reply this chapter supports.
7. Describe the sequence of events by which a model that was independent on Monday stops being independent by Friday, without anyone copying any code.
8. For the running example, predict which clause the sat_acc_bug design violates and how many of 70 checks would expose it. Chapter 24.3 gives the measured answer.

8. Summary

• An oracle's disagreement is a bug report — that is the promotion, and it carries obligations.
• Three obligations: independence · determinism where required · the specification as authority.
• Measured: 51 mismatches against 0 on the same buggy design, same 70 checks, two C models.
• They agree on sample 1 and diverge on sample 2 — which is why such a model passes its first test.
• Determinism: 40 outputs identical on repeat from reset.
• Given the starting state — measured 0 of 40 without a reset; a stateful model has a hidden second input.
• Order is part of the stimulus — measured 2 of 40 in reverse.
• Where the spec is silent, do not quietly decide — name the clause for every line.
• Independence is provenance, not language — model_rtl.c is C and certifies a broken design.
• A model that agrees with the design looks exactly like a model that is right.

Three obligations and a comparison that has been described only in words. Before any of it can be wired up, the pieces need to be in one picture — what drives what, where the model sits relative to the design, and exactly where the comparison happens.