The course built DCRouter's plan step by step across Parts 2 to 9. This capstone asks you to do it alone, for a block you have not seen: IRQC, an interrupt controller that collects eight interrupt sources and presents the most important one to a processor.
Your task: write the verification plan for IRQC from the specification below. Give each feature its rule, risk, check, method and coverage; name the formal candidates, the assumptions and the sign-off criteria; and list the questions you would send back to the specification's author. Allow an hour; then compare with the model plan.
Rule | Text |
|---|---|
I1 | Eight interrupt sources irq_in[7:0], level signals synchronous to clk. |
I2 | A source becomes pending on a rising edge of irq_in[i]; PENDING[i] stays set until cleared, even if irq_in[i] falls. |
I3 | Writing 1 to CLEAR[i] clears PENDING[i]; writing 0 has no effect. A rising edge in the same cycle as the clear wins: PENDING stays set. |
I4 | ENABLE[i] masks source i: a disabled source can still become pending but is never signalled. |
I5 | PRIO[i] is 2 bits (3 highest). irq_out is high when any source is both pending and enabled. |
I6 | VECTOR holds the highest-priority pending enabled source; ties go to the lowest index. VECTOR is 8 (none) when irq_out is low. |
I7 | Reading VECTOR acknowledges it: the returned source's PENDING bit clears in the same cycle, and VECTOR updates the next cycle. |
I8 | Registers (APB): ENABLE 0x00 RW, PENDING 0x04 RO, CLEAR 0x08 WO, PRIO 0x0C RW (2 bits per source), VECTOR 0x10 RO. Others: pslverr. |
I9 | Reset: ENABLE 0, PENDING 0, PRIO 0, irq_out low, VECTOR 8. |
I10 | irq_out is registered: it changes one cycle after the PENDING or ENABLE change that causes it. |
Read every rule for same-cycle events (lesson 1.4): two things that can happen in one cycle and which one wins.
Ask where the oracle comes from (lesson 2.1): which features a reference model covers and which need a property.
Look for small, fully specified logic worth proving (lessons 7.5 and 16.2).
Look for what the specification does not say (lesson 2.5).
Write yours before reading this. Risk is High where a bug loses or misroutes an interrupt.
ID | Feature | Rule | Risk | Check | Method / evidence | Coverage |
|---|---|---|---|---|---|---|
F1 | Rising edge sets PENDING; level held does not re-set after clear | I2 | High | Reference model of PENDING; assertion on edge | Random levels and pulses | edge per source; held-level-after-clear |
F2 | PENDING sticky after the input falls | I2 | Medium | Model | Short pulses | pulse of 1 cycle |
F3 | CLEAR write-1-to-clear, 0 ignored | I3 | Medium | Model; read-back | Random CLEAR masks | CLEAR with mixed bits |
F4 | Edge and clear in the same cycle: edge wins | I3 | High | Model; assertion | Directed plus biased random | same-cycle bin per source |
F5 | ENABLE masks signalling, not pending | I4 | High | Model; assertion irq_out vs PENDING&ENABLE | Random enables | pending while disabled; enable while pending |
F6 | irq_out = any pending and enabled, one cycle later | I5, I10 | High | Assertion (formal candidate) | Formal; random | irq_out rise and fall |
F7 | VECTOR: highest priority, ties to lowest index | I6 | High | Model; formal property on the selector | Formal; random | every priority pattern of two contenders; ties |
F8 | VECTOR 8 when nothing signalled | I6 | Medium | Assertion | Formal | VECTOR 8 read |
F9 | Reading VECTOR acknowledges exactly that source | I7 | High | Model; scoreboard of acknowledged sources | Random handler loop | ack while another source rises; ack in the clear cycle |
F10 | Ack and new edge on the same source in the same cycle | I2, I7 | High | Model (ack clears; does the edge win?) - spec question | Directed | same-cycle ack and edge |
F11 | Register map, access types, pslverr | I8 | Medium | Register checks | Register sweep | every address read and write |
F12 | PRIO fields independent | I8 | Medium | Read-back | Walking ones | each field written alone |
F13 | Reset values; reset mid-operation | I9 | Medium | Read after reset; model reset | Directed reset mid-traffic | reset with pending sources |
F14 | No lost interrupt under sustained load | I2, I7 | High | Scoreboard: every edge eventually acknowledged or cleared | Random storms with a handler model | all 8 pending at once |
F15 | Fairness/starvation of low priority (documented behaviour) | I6 | Low | Measurement, not a check: starvation is allowed | Long random runs | low-priority wait length histogram |
Section | Model answer |
|---|---|
Oracle | A cycle-accurate reference model of PENDING, irq_out and VECTOR (the rules are fully specified), plus assertions for timing rules I5 and I10 |
Formal candidates | The VECTOR selector (8 sources × 4 priorities, small and fully specified), irq_out timing, the CLEAR and edge interaction |
Assumptions | irq_in synchronous to clk (I1): CDC is the integrator's responsibility; APB accesses are well formed; one processor acknowledges |
Stimulus | Random levels, pulses and storms; a handler model that reads VECTOR and clears; directed tests for same-cycle cases |
Sign-off criteria | Every feature with evidence; coverage of every same-cycle bin; selector proved; reference-model comparison on 200 seeds clean; planted-bug run on the checks (at least edge, mask, priority and ack bugs) |
Residual risk to state | Starvation of low priority is by design; asynchronous sources outside scope |
I1 versus I2: I1 calls the sources level signals, I2 captures them on a rising edge. Is a source that stays high after its PENDING bit is cleared meant to be seen again (level-sensitive) or not (edge-captured)? F1 assumes edge capture.
I7 versus I2: if a source is acknowledged in the same cycle as a new rising edge on it, does PENDING stay set? I3 says an edge wins over a clear; is an acknowledge a clear?
I7: does reading VECTOR when it is 8 do anything? Does a read with pslverr acknowledge?
I5 and I10: does VECTOR also update one cycle late, or immediately? Can a handler read a VECTOR that disagrees with irq_out?
I6: may VECTOR change while irq_out stays high (a higher priority arrives)? The handler's read then acknowledges the new one.
I4: when a disabled pending source is enabled, irq_out rises one cycle later (I10)?
A good plan finds these before any RTL is verified: each is a place where the designer and the verifier could read the rule differently, and lesson 1.2's specification bugs are the most expensive kind to find late.
You found | Level |
|---|---|
Features for each rule with checks and coverage | Solid foundation |
The same-cycle cases (F4, F9, F10) and the lost-interrupt risk (F14) | Senior |
The selector as a formal candidate and the I2/I7 ambiguity | Senior to principal |
Sign-off criteria, assumptions and residual risk written down | Principal |
The specification does not say whether an acknowledge in the same cycle as a new edge leaves PENDING set; until the author decides, no check can be written.
The specification allows it (strict priority); the plan records how long low priority waits so the system team can judge it, but it is not a bug.
A plan traces every feature to a rule, with risk, check, method and coverage.
Same-cycle events, oracles, formal candidates and silences are where the risk is.
Questions back to the specification are part of the plan.