Every question in this section is graded on four dimensions, each scored 0 to 4. Assumption states the environment and reset model. Mechanism explains the proof at cycle level. Trade-off compares at least two options with costs. Evidence names what shows the result is not vacuous. A first answer usually scores 2 per dimension: right but generic. One specific sentence turns a 2 into a 3; a failure mode and its check turn a 3 into a 4.
Score | Anchor |
|---|---|
0 | The dimension is absent. |
1 | Vague or wrong: 'some assumptions', 'the tool checks everything'. |
2 | Right but generic: could be said about any design. |
3 | Specific and mostly correct: names the reset model, the depth, the step, the cover. |
4 | Specific, correct, and anticipates a failure mode with the check that catches it. |
Lesson | After it you can... |
|---|---|
Score any answer 0 to 4 per dimension, and list the five acceptance checks behind a fast proof. | |
Answer the six questions on fast proofs, assume versus assert, bounded results, induction, FIFO depth, and arbiter liveness. | |
Answer the six questions on counterexample triage, memory abstraction, reset gating, equivalence, method choice, and signoff. |
Restate the question in one sentence, so the panel hears which obligation you are answering.
State the assumptions first: reset model, free inputs, protocol rules, depth.
Name the outcome you expect (proven, counterexample or inconclusive) before describing the run.
Common failures: yes or no with no checks; a bounded pass called a proof; fairness placed on a design output; an assume nobody owns; a number with no run behind it; waiving a counterexample without an invariant.
Suggested order: top to bottom. Learn the shape and the rubric, then the twelve answers: the first six fix the results vocabulary and induction, the last six fix triage, abstraction and signoff. Cover the answer, say it aloud, score yourself, then read on.
The working around the correctness: stated assumptions, a costed alternative, and verification evidence. Each is worth a full dimension on the rubric.