11Verification

Find the broken transition in a state machine

Problem

Intended behavior. rise_fsm is the two-state rise detector of the State machines chapter. The state remembers the level sampled at the last rising edge: LOW for 0, HIGH for 1. The Mealy output rise is 1 in a cycle whose level is 1 while the state is LOW. Reset is synchronous and active-high and puts the machine in LOW.

Current state	`level`	Next state	`rise`
`LOW`	0	`LOW`	0
`LOW`	1	`HIGH`	1
`HIGH`	0	`LOW`	0
`HIGH`	1	`HIGH`	0

Current behavior. The starter compiles and runs. The public pattern rises four times, but the trace reports rises=1: after the first rise the machine never reports another one.

Your task. Find the one transition that disagrees with the table and fix it. Keep the ports, the state names, the output logic and the public testbench as they are.

Predict, then read the trace

Before you run, write the expected rise column for the twelve cycles of the pattern 0110_1110_0101 from the table, and count the rises. Then run and mark the first cycle where the printed rise differs from your column.

That cycle is a symptom, not the cause. The output logic only reads the state and the input, so if rise is wrong while level is right, the state must be wrong at that moment. Open the waveform and add tb.dut.state: find the edge after which the state should have changed and did not.

Fix and confirm

Compare each branch of the case with one pair of table rows. Correct the branch that disagrees, run again, and check that:

every 0-to-1 change of level gives exactly one cycle of rise, including rises right after a single 0;
state changes only at rising edges and follows the table after every edge;
rise may change inside a cycle when level changes, because it is a Mealy output.

Completion check

For every input pattern, rise equals level AND (previous sampled level is 0), measured inside each cycle before the rising edge.
After reset the previous level counts as 0, so a level held high through reset rises again in the first cycle after reset.
Grading uses patterns you have not seen, including long runs of 1, single zeros between ones, and reset in the middle of a run. The first failing cycle is reported with the input, the expected and the actual value.

Progressive hints

Hint 1

The machine detects the first rise, so the LOW row with level 1 works. What has to happen before a second rise can be seen?

Hint 2

A second rise needs the state to be LOW again. Which table row takes the machine from HIGH back to LOW, and does the code have it?

Hint 3

Read the HIGH branch for both values of level. One of its two results never matches the table.

Transfer experiment

Change the output so that the machine detects falling edges instead: fall is 1 in a cycle whose level is 0 while the state is HIGH. Which rows of the table change, and does the next-state logic need to change at all? Predict the column for the public pattern before you run it.