Practice problems

Each problem is small enough to finish in under an hour. Write the design (or use ours where given), a formal wrapper with assertions and covers, and run it. Solutions for problems 1 and 2 are in the next lesson — try first!

Problem 1 — Gray-code counter (easy)

A W-bit counter outputs its value in Gray code. Write properties that check: exactly one output bit changes per enabled cycle (including the wrap-around); the output holds when not enabled; the wrap-around is reachable.

Problem 2 — Pulse stretcher (easy)

A single-cycle input pulse must produce an output that is high for exactly N cycles; a new pulse while the output is high restarts the N-cycle window. Write properties for "on for N cycles", "off after N quiet cycles" and "output only rises because of a pulse".

Problem 3 — Button debouncer (medium)

The output follows a noisy input only after the input has been stable for K consecutive cycles. Hints: write one property for "output changes ⇒ input was stable K cycles", and one for "input stable K cycles ⇒ output equals input". Cover a glitch shorter than K.

Problem 4 — Four-phase req/ack handshake (medium)

req rises, ack rises, req falls, ack falls — repeat. Write a reusable checker (like vr_checker) that asserts the rules for the side under test and assumes them for the other. Cover two complete handshakes back to back.

Problem 5 — One-hot FSM (medium)

Take any FSM (for example, the lift controller from Chapter 5) and re-encode it one-hot. Assert the encoding is always one-hot and that only legal transitions occur. Then use the sequential equivalence technique from Chapter 8 to prove the one-hot version behaves exactly like the original.

Problem 6 — Credit counter, complete (tricky)

Return to the credit counter from Chapter 1. Write a complete property set (range, increment, decrement, simultaneous inc/dec, saturation at MAX), with covers for empty and full. Run a mutation campaign with at least five mutants and make sure every one is caught.