18 / 37 · Check

Design check: boundaries of width, priority and wraparound

Use a specified state-transition contract to reason about boundaries and simultaneous controls.

The modulo-10 counter contract

For four-bit unsigned^{Unsigned A rule for interpreting a bit pattern as a nonnegative integer. The n-bit range is 0 through 2^n−1 and may differ from the signed interpretation of the same bits. Learn more} count, priority is reset, then enable, then hold. Reset=1 forces 0. With enable=1, values at or above 9 return to 0; other states increment by 1.

N=\lceil\log_2 10\rceil=4

Four bits mean 16 representable states. They do not automatically implement the specification to use only ten. In particular, count=9 with enable=0 must not return to 0.

Each column below records a rising edge^{Rising edge The instant at which the clock changes from 0 to 1. Distinguish it from a level, which refers to the entire interval during which CLK=1. Learn more}. Inputs are pre-edge; states labeled “after” are post-update. Alignment shows sampling order, not physical propagation delay^{Propagation delay The time from an input change until the output settles to the correct value. Logical equivalence and timing behavior are separate properties. Learn more}. Initially count=9. The first column has no reset and enable=0, so 9 is retained. Only the next column with enable=1 returns it to 0.

Hold must remain valid at the boundary

View waveform data

Wave data: each character is one interval; a dot holds the previous state; p is a clock cycle.
Signal	Wave	Bus values
edge	`2345`	E0 → E1 → E2 → E3
reset	`0.10`
enable	`01..`
count after	`23.4`	9 → 0 → 1

Further design questions

Find the next value for count=9, reset=0, enable=0.
Explain recovery when count=15 and enable=1.
Specify whether a terminal pulse should occur for count=9, reset=1, enable=1. Assume the output is defined to be 0 during reset^{Reset A control that returns state to a specified initial value. Define whether it is synchronous or asynchronous and whether it has priority over other controls. Learn more}.

Try it yourself

How many one-step transitions exhaustively cover every count from 0–15 and every reset/enable combination? Does this alone automatically prove all requirements for long state sequences?

Read the explanation

$16\times2\times2=64$ cases. If count represents the complete state and the next-state/output specification is precise, as in this design, one-step checking is strong evidence. It does not establish omitted requirements such as initialization, input assumptions, separate terminal-pulse state or physical timing.

With current count=9, reset=1 and enable=1 are sampled together. What next count and terminal pulse satisfy reset priority?

Choose an answercount=0, terminal pulse=1: treat it as normal wraparound.count=10, terminal pulse=0: enable takes priority.count=0, terminal pulse=0: reset initializes both state and pulse.