Every block has registers, and register bugs are integration bugs in miniature: a read-only bit that accepts writes, a clear that sets, a reset value one revision out of date, an error returned a cycle late. This topic proves the four-register control block from its register table: reset values, read-write behaviour, write-1-to-clear, read-only discipline, access timing with wait states, and the race between a hardware event and a software clear in the same cycle. The table is the source of truth throughout.
Lesson | After it you can... |
|---|---|
Turn a register table into a property set with a generator and see a table typo fail. | |
Write sampling-correct properties for clear-on-write and read-only bits, and kill each family with a bug. | |
Prove same-cycle error responses and wait-state-safe properties. | |
Specify a race priority, prove it, and cover the collision. |
Suggested order: top to bottom. The table lesson builds the method, the access-type lesson is the heart of it, timing extends it to bus behaviour, and the race lesson handles the one cycle every register team argues about. For the map itself and the simulation-side flow, see the register-map and register-model lessons linked below.
One table row, then regenerate: the reset, access-type and isolation checks for that register appear automatically, and the proof reruns. Nothing is hand-edited, so nothing is forgotten.