Design Closure Checklist · RTL Design

Part 4 · FSM & Control · Intermediate

On this page

Questions and answers

Question	Answer for the memory controller
Reset: are all outputs defined?	State resets to IDLE; `req_ready = 1`, `mem_en = 0`, `rsp_valid = 0`. Request copies reset to 0.
Is every state reachable and does every state return to IDLE?	Yes: IDLE → ACCESS → (IDLE \| WAIT/RESP → IDLE). No dead ends.
Illegal state recovery?	All four 2-bit codes are legal. The default is an RTL fallback, not protection from a bit flip into another legal state or proof of synthesized recovery; see illegal states and recovery.
Latches?	None: outputs are `assign` statements of the state and the copies; the next-state logic is a registered `case`.
Is the handshake safe?	`req_ready` is a pure function of state. A requester that holds its request until accepted is served in order.
Is latency exactly as specified?	Source timing: availability after accept + RD_LAT; consumption at accept + RD_LAT + 1. This controller's supplied due-edge queue checks early, late, missing and extra pulses. Passes in simulation.
Hang possible?	No waiting on the outside world: the RAM is assumed to respond at a fixed latency. If the RAM can stall or fail, add a timeout (see the sequencer robustness lesson).
Back-to-back and mixed operations?	Supplied: directed write/write/read/read and random stable offers, with access counts and bounded drain. Passes in simulation.
Read-after-write to the same address?	Supplied: directed same-address overwrite/read plus random traffic in up to eight locations. Passes in simulation.
Parameter sweep?	Supplied (AW,DW,RD_LAT): (1,1,1), (6,8,2), (3,12,3), (4,4,4). Covers minimum ports, latency-one bypass and nontrivial waits; not every parameter combination. Passes in simulation.
Reset cancellation and consumer?	Supplied: reset in ACCESS, every WAIT slot and RESP before consumption; cancel a pre-commit write, preserve committed data, then read in a fresh epoch. A consumer register captures every noncancelled pulse. Passes in simulation.

Coverage ideas

A real verification plan tracks states, crosses, assertions, and stimulus corners.

State coverage: all four states visited, all transitions taken (write path, read with RD_LAT = 1, read with RD_LAT > 1).
Cross coverage: write → read same address; read → read; write → write; each with and without idle gaps.
Protocol assertions: rsp_valid only follows a read; exactly one rsp_valid per read; mem_en only in ACCESS; req_ready low in all other states.
Stimulus corners: request inputs changed on the cycle after accept; reset in the middle of an operation (the controller returns to IDLE and no stray rsp_valid appears).

Verification notes

Formal tools can prove or refute properties, or remain inconclusive. A proof covers the specified model under explicit assumptions: a progressing clock, reset/cancellation epochs, legal stable requester offers, positive parameters, and synchronous fixed-latency memory. Exactly one response applies to accepted reads not cancelled by reset. If the consumer can stall, this interface needs response storage or backpressure before that proof matches integration.

Check yourself Which closure questions are useful formal properties, and what assumptions do they need?

Cover legal state reachability; assert bounded return to IDLE and one response per uncancelled accepted read under progressing clock/reset and fixed-latency RAM assumptions. Require stable offers until acceptance, and scope proofs to legal parameters. Proof, counterexample and inconclusive results are distinct outcomes; a neighboring module's test proves nothing about this controller.

How this was checked

This lesson separates source reasoning from the supplied checks. No new simulation, formal run, synthesis or physical timing measurement is claimed.

Related topics

Timing

Up nextTiming & Clocking

Practice this lesson Report an error

Questions and answers

Question	Answer for the memory controller
Reset: are all outputs defined?	State resets to IDLE; `req_ready = 1`, `mem_en = 0`, `rsp_valid = 0`. Request copies reset to 0.
Is every state reachable and does every state return to IDLE?	Yes: IDLE → ACCESS → (IDLE \| WAIT/RESP → IDLE). No dead ends.
Illegal state recovery?	All four 2-bit codes are legal. The default is an RTL fallback, not protection from a bit flip into another legal state or proof of synthesized recovery; see illegal states and recovery.
Latches?	None: outputs are `assign` statements of the state and the copies; the next-state logic is a registered `case`.
Is the handshake safe?	`req_ready` is a pure function of state. A requester that holds its request until accepted is served in order.
Is latency exactly as specified?	Source timing: availability after accept + RD_LAT; consumption at accept + RD_LAT + 1. This controller's supplied due-edge queue checks early, late, missing and extra pulses. Passes in simulation.
Hang possible?	No waiting on the outside world: the RAM is assumed to respond at a fixed latency. If the RAM can stall or fail, add a timeout (see the sequencer robustness lesson).
Back-to-back and mixed operations?	Supplied: directed write/write/read/read and random stable offers, with access counts and bounded drain. Passes in simulation.
Read-after-write to the same address?	Supplied: directed same-address overwrite/read plus random traffic in up to eight locations. Passes in simulation.
Parameter sweep?	Supplied (AW,DW,RD_LAT): (1,1,1), (6,8,2), (3,12,3), (4,4,4). Covers minimum ports, latency-one bypass and nontrivial waits; not every parameter combination. Passes in simulation.
Reset cancellation and consumer?	Supplied: reset in ACCESS, every WAIT slot and RESP before consumption; cancel a pre-commit write, preserve committed data, then read in a fresh epoch. A consumer register captures every noncancelled pulse. Passes in simulation.

Coverage ideas

A real verification plan tracks states, crosses, assertions, and stimulus corners.

State coverage: all four states visited, all transitions taken (write path, read with RD_LAT = 1, read with RD_LAT > 1).

Cross coverage: write → read same address; read → read; write → write; each with and without idle gaps.

Protocol assertions: rsp_valid only follows a read; exactly one rsp_valid per read; mem_en only in ACCESS; req_ready low in all other states.

Stimulus corners: request inputs changed on the cycle after accept; reset in the middle of an operation (the controller returns to IDLE and no stray rsp_valid appears).