Volume 12 Beginner 5 sub-modules ~20 min read

Verifying State Machines

A state machine is only finished when you can show that it works - in every state, on every arrow, for every input. This volume builds a test that walks every arrow of the drink machine, measures what it covered, and adds assertions that catch a broken rule the moment it happens. It explains what formal tools prove, and ends with a method for the most common bug report of all: "it is stuck".

You will learn
  • How to plan a test that takes every transition
  • How to measure state and transition coverage
  • How to write assertions for state machine rules
  • What formal verification proves, in plain words
  • A step-by-step method for debugging a stuck machine
You need

12.1 Tests that hit every transition

A thorough test drives the machine along every arrow of its state diagram at least once, and checks the outputs and the next state at every step.

Visiting every state is not enough

Suppose a test for the turnstile puts in a coin, then pushes the arm. It visits both states, LOCKED and UNLOCKED. But it never pushes while locked, and never puts a coin in while unlocked - the two self-loops. If one of those arrows were wrong, this test would pass anyway.

In plain words

Bugs live on arrows, not in states. A state is only a place; the arrows are the decisions, and a wrong decision is a bug.

So the goal is to take every arrow at least once. A test that does this is a transition tour.

Planning a tour for the drink machine

The drink machine from Volume 03 has four states and one input, so its state table has 4 × 2 = 8 rows - 8 arrows. Starting from reset, in C0, the shortest input sequence that takes all 8 arrows is ten coins long: 0, 1, 0, 1, 0, 1, 1, 1, 1, 0. It cannot be done in 8 - some arrows can only be reached by passing along others again.

The drink machine with each arrow labelled by the tour steps that take it C0 C1 C2 VEND step 2 steps 4, 8 steps 6, 9 step 10 step 7 step 1 step 3 step 5 reset
Figure 12.1 - The ten-step tour on the drink machine. Each arrow shows the step numbers at which the tour takes it. Every arrow has at least one number, so every transition is tested.
Step State before coin Expected next state vend (in the state before)
1 C0 0 C0 0
2 C0 1 C1 0
3 C1 0 C1 0
4 C1 1 C2 0
5 C2 0 C2 0
6 C2 1 VEND 0
7 VEND 1 C1 1
8 C1 1 C2 0
9 C2 1 VEND 0
10 VEND 0 C0 1

Checking every step

A tour is only useful if every step is checked. The testbench below holds the state table as data, in a function, and runs its own copy of the machine beside the design. After every clock edge it compares the two. This is the reference model idea from Volume 06, written as a table.


module drink_tour_tb;
  reg  clk = 0, rst = 1, coin = 0;
  wire vend;
  reg  [1:0] model;                          // the reference model's state
  reg  [0:9] tour = 10'b0101011110;          // the ten-step tour, step 1 first
  integer i, errors = 0;

  drink_fsm dut (.clk(clk), .rst(rst), .coin(coin), .vend(vend));
  always #5 clk = ~clk;

  function [1:0] model_next(input [1:0] s, input c);   // the state table, as data
    case ({s, c})
      3'b00_0: model_next = 2'b00;  3'b00_1: model_next = 2'b01;   // C0
      3'b01_0: model_next = 2'b01;  3'b01_1: model_next = 2'b11;   // C1
      3'b11_0: model_next = 2'b11;  3'b11_1: model_next = 2'b10;   // C2
      default: model_next = c ? 2'b01 : 2'b00;                     // VEND
    endcase
  endfunction

  initial begin
    model = 2'b00;
    repeat (2) @(negedge clk); rst = 0;
    for (i = 0; i < 10; i = i + 1) begin
      coin = tour[i];                        // this step's input, away from the rising edge
      @(negedge clk);                        // one rising edge later...
      model = model_next(model, tour[i]);    // ...the model takes the same step
      if (dut.state !== model || vend !== (model == 2'b10)) begin
        errors = errors + 1;
        $display("step %0d: state %b, expected %b", i + 1, dut.state, model);
      end
    end
    if (errors == 0) $display("PASS: all 8 transitions taken and checked");
    else             $display("FAIL: %0d error(s)", errors);
    $finish;
  end
endmodule

dut.state looks inside the design by name, so the test checks the state itself, not only the output. Checking the internal state makes a failure much easier to understand: the message says exactly which step went wrong, and where the machine went instead.

Common mistake

Writing the reference model by copying the design's code. If the design has a wrong arrow, the copy has it too, and they agree perfectly. Build the model from the specification - here, the state table - never from the design.

Quick check

A test visits all four states of the drink machine but never puts in a coin while in C2. What is missing?

Show the answer

Answer: C. Visiting C2 is not the same as taking every arrow out of it. Without a coin in C2, the arrow from C2 to VEND - the one that sells the drink - was never tested, and a bug on it would go unnoticed.

Try it in FSM StudioIn FSM Studio, the button Take every arrow runs the shortest test that covers the whole table - ten inputs for the drink machine, as above. The Testbench tab turns it into a self-checking testbench.
Open FSM Studio

12.2 State and transition coverage

Coverage measures what your tests actually did: which states they visited, and which arrows they took. It turns "I think we tested everything" into a number.

Two measures

Coverage records, during a simulation, which situations the design actually met. For a state machine, two measures matter most:

The turnstile test from sub-module 12.1 had 100% state coverage, but only 50% transition coverage - two of its four arrows were never taken. Transition coverage is the one to trust.

Counting arrows in plain Verilog

Add one counter per row of the state table. On every clock edge, the current state and the current input together name the row about to be taken:


integer hits [0:7];                              // one counter per (state, coin) row
integer k, taken;
initial for (k = 0; k < 8; k = k + 1) hits[k] = 0;

always @(posedge clk)
  if (!rst) hits[{dut.state, coin}] = hits[{dut.state, coin}] + 1;

// at the end of the test:
//   taken = 0;
//   for (k = 0; k < 8; k = k + 1) if (hits[k] > 0) taken = taken + 1;
//   $display("transition coverage: %0d of 8 arrows", taken);

{dut.state, coin} joins the 2-bit state and the 1-bit input into a 3-bit number from 0 to 7 - the row of the state table. Any counter still at 0 at the end is an arrow the test never took.

Covergroups in SystemVerilog

SystemVerilog has this built in. A covergroup samples signals on a clock and counts the values it sees:


covergroup drink_cov @(posedge clk);
  st:     coverpoint dut.state { bins state[] = {2'b00, 2'b01, 2'b11, 2'b10}; }  // C0 C1 C2 VEND
  cn:     coverpoint coin;
  arrows: cross st, cn;             // every (state, input) pair = every row of the table
endgroup

drink_cov cov = new();              // create it once, in the testbench

The cross counts every combination of state and input, which for a single-input machine is exactly transition coverage. Coverpoints can also count sequences directly: bins steps[] = (2'b00 => 2'b01) counts the step from C0 to C1. Covergroups need a simulator that supports SystemVerilog coverage; most commercial simulators do, but the free Icarus Verilog does not - the plain counters above work everywhere.

Remember

Coverage tells you where you looked. Checking - comparing with a reference model, or assertions - tells you what you found. A test with 100% coverage and no checks proves nothing.

Common mistake

Aiming for coverage with random input alone, then stopping when the number stops rising. Some arrows are hard to reach by chance - a state that needs a rare combination of inputs. When coverage stalls, look at which arrows are missing and write a directed test that goes straight to them.

Quick check

A test reaches 100% state coverage and 75% transition coverage. What does that tell you?

Show the answer

Answer: B. State coverage counts places visited; transition coverage counts arrows taken. 75% transition coverage means some arrows - some decisions - were never exercised, so bugs on them could still be hiding.

12.3 Assertions for FSMs

An assertion is a rule about the design, written as code and checked on every clock cycle. A broken rule is reported the moment it breaks - not later, when its effects finally reach an output.

Rules that watch all the time

A testbench checks what it looks at, when it looks. An assertion checks a rule on every clock cycle of every test, including the random ones, forever. When the rule breaks, the simulator reports the time and the rule, right at the source of the bug.

State machines have natural rules:

Writing them in SystemVerilog

SystemVerilog Assertions (SVA) express rules that span clock cycles. A few symbols carry most of the meaning:

Symbol Read it as
@(posedge clk) check at every rising edge
disable iff (rst) ignore the rule during reset
a |-> b if a is true, then b must be true in the same cycle
a |=> b if a is true, then b must be true in the next cycle
##[1:300] b b must happen within 1 to 300 cycles

Here are rules for safe_ctrl from Volume 11, written inside the module:


// 1. the state is always legal
assert property (@(posedge clk) disable iff (rst)
                 state inside {IDLE, RUN, DONE})
  else $error("illegal state %b", state);

// 2. from IDLE, go leads to RUN at the next edge
assert property (@(posedge clk) disable iff (rst)
                 (state == IDLE && go) |=> (state == RUN));

// 3. busy is 1 exactly in RUN
assert property (@(posedge clk) busy == (state == RUN));

And two from earlier volumes. For the GCD calculator of Volume 09, "every start is answered within 300 cycles" - for 8-bit inputs the slowest case needs 254 subtractions, so 300 is a safe limit:


// GCD: done must follow start within 300 cycles (it catches the gcd(0, x) hang)
assert property (@(posedge clk) disable iff (rst) start |-> ##[1:300] done);

// four-phase handshake: a request is never taken back, and its data never changes, until ack
assert property (@(posedge clk) disable iff (rst) (req && !ack) |=> req);
assert property (@(posedge clk) disable iff (rst) (req && !ack) |=> $stable(data));

$stable(data) means "data has the same value as in the previous cycle".

Without SystemVerilog

If your simulator does not support SVA - Icarus Verilog does not - a plain check in an always block does the simplest job:


always @(posedge clk)
  if (!rst && state == 2'b11)
    $display("ERROR at time %0t: illegal state", $time);
Common mistake

Writing assertions that only restate the code. "When the code says next_state = RUN, next_state is RUN" can never fail and finds nothing. Write rules from the specification - what must be true - and the assertion becomes a second, independent opinion.

Quick check

What does (state == C2 && coin) |=> (state == VEND) check?

Show the answer

Answer: D. |=> means "then, in the next cycle". So the rule says: in any cycle where the state is C2 and coin is 1, the state one cycle later must be VEND. If the design ever takes a different arrow, the simulator reports it on the spot.

12.4 Formal reachability in plain words

A formal tool does not run tests. It works out every state the design can reach from reset, and then either proves that a rule always holds, or hands you the input sequence that breaks it.

Reachability, by hand

In Volume 10 you removed unreachable states by starting at reset and following every arrow. Do it carefully, one step at a time, on this machine:

A machine with five states, one of which - TEST - can never be reached from reset IDLE LOAD RUN DONE TEST go always fin ack always else else else reset
Figure 12.2 - A machine with a hidden problem. Start at IDLE and follow the arrows: IDLE, LOAD, RUN and DONE can all be reached, but no arrow ever leads into TEST.
Step States reached for the first time
0 IDLE (reset)
1 LOAD
2 RUN
3 DONE
4 nothing new - DONE only leads back to IDLE

The set of reachable states stops growing after step 3. TEST is not in it, so no test can ever reach TEST. If it was put there for factory testing, the designer must provide another way in; if not, it is dead logic.

What a formal tool does

Formal verification does exactly this, but for the whole design at once - every register, every input combination, every cycle - using mathematics rather than simulation. You give it the design and your assertions. It answers in one of two ways:

Formal tools also make excellent test generators. Give one the deliberately false rule "vend is never 1", and it will reply with the shortest way to get a drink: reset, then coin, coin, coin.

What formal tools find in state machines

A related failure is livelock: the machines keep changing state, but never make progress. Think of two people in a corridor who keep stepping the same way to let each other pass.

Going deeper: how far can a formal tool see?

A design with many registers has an astronomical number of states, so tools use two main tricks. Bounded model checking looks at every input sequence up to some length - say, 30 cycles - and finds any failure within that depth. Induction then tries to show that no failure can happen at any depth. Free tools exist: SymbiYosys, built on the open-source Yosys synthesis tool, runs formal checks on Verilog designs with assertions.

Common mistake

Treating "proven" as "correct". A formal proof shows that your assertions always hold - nothing more. If an important rule was never written as an assertion, nothing proved it. Formal verification is exactly as good as the rules you give it.

Quick check

A formal tool reports "failed" for an assertion. What does it give you?

Show the answer

Answer: A. When a rule can be broken, the tool shows how: a sequence of inputs, starting from reset, that leads to the failure. You can replay it in simulation and watch the bug happen step by step.

12.5 Debugging a stuck FSM

When a machine seems stuck, find the state it is stuck in, read which input would move it on - and then find out why that input never comes.

A method, not a guess

"The machine is stuck" is the most common state machine bug report. Work through it in order:

  1. Is it alive? Is the clock running? Is reset released - with the right polarity? A reset held active looks exactly like a stuck machine.
  2. Where is it? Read the state - in the waveform, or on hardware with a logic analyser probe. Remember that synthesis may have re-encoded it (Volume 05): use the synthesis report to translate the codes.
  3. Is that a legal state? If not, the problem is a fault, a timing violation or a reset issue - Volume 11.
  4. What is it waiting for? Read the arrows out of that state. Which input would move it on?
  5. Why does that input never come? This is where the real bug is.

Why the input never comes

What you see The usual cause The fix
waits for a pulse that never seems to come the pulse came while the machine was in another state catch it in a sticky flag
two machines each waiting each is waiting for the other - a deadlock fix the protocol, or add a timeout
waits for a signal from another clock a short pulse was lost crossing clocks handshake or stretch it (Volume 09)
never leaves IDLE start is active low, but coded as active high fix the polarity - and name it start_n
stuck in a timed state the timer was never loaded, or done compares the wrong value check the load and the done condition

The missed pulse

The first row is the most common of all. A parent machine starts a child, does one more cycle of setup work, then waits for the child's one-cycle done pulse. But this child is fast: its pulse comes during the setup cycle, when the parent is not looking.

A missed pulse: the parent reaches WAIT after the child's one-cycle done pulse has gone, and waits for ever; with a sticky flag it moves on 0 1 2 3 4 5 6 7 clk parent_bug IDLE KICK SETUP WAIT start done got_done parent_fix IDLE KICK SETUP WAIT NEXT IDLE
Figure 12.3 - The done pulse comes in cycle 2, while the parent is still in SETUP. The buggy parent reaches WAIT in cycle 3 and waits for ever. The fixed parent keeps the pulse in a sticky flag, got_done, sees it in WAIT, and moves on.

The fix is a sticky flag: a register that is set by the pulse, whenever it comes, and stays set until the machine has used it.


always @(posedge clk)
  if (rst)                            got_done <= 1'b0;
  else if (done)                      got_done <= 1'b1;   // catch the pulse, whenever it comes
  else if (state == WAIT && got_done) got_done <= 1'b0;   // clear it once it has been used

// in the next-state logic:  WAIT: if (got_done) next_state = NEXT;
Think of it like this

A one-cycle pulse is like a doorbell rung once while you are in the garden - if you were not there, you missed it. A sticky flag is a note pushed under the door: it waits until you come back and read it.

Common mistake

Adding a delay to "fix" a missed pulse - waiting one cycle less in SETUP, say. It passes the test, until the child becomes faster or slower in the next design and the pulse is missed again. Fix the protocol, so that it works whatever the timing: sticky flags, handshakes or levels instead of pulses.

Quick check

A machine waits in WAIT for done. The waveform shows a done pulse two cycles before the machine entered WAIT. What is the best fix?

Show the answer

Answer: C. The pulse came while the machine was not looking. A sticky flag remembers it, so it does not matter when the pulse arrives - before or during WAIT. The fix works whatever the timing of the other block.

What you learned

Key words from this volume

Every word below has a plain-English entry in the glossary.

Practice

Practice 1

A tour for the turnstile

Using the full turnstile table from Volume 01 - two states and two inputs, coin and push - how many rows does a complete tour need to cover? Give a sequence that covers them all from reset.

Show the solution

2 states × 4 input combinations = 8 rows. Here is one tour that covers them all from LOCKED:

Step coin push From To
1 0 0 LOCKED LOCKED
2 0 1 LOCKED LOCKED
3 1 1 LOCKED UNLOCKED
4 0 0 UNLOCKED UNLOCKED
5 1 0 UNLOCKED UNLOCKED
6 1 1 UNLOCKED LOCKED
7 1 0 LOCKED UNLOCKED
8 0 1 UNLOCKED LOCKED

Every LOCKED row and every UNLOCKED row appears exactly once: eight steps, eight rows.

Practice 2

Write the rule

Write an SVA assertion for the edge detector of Volume 02: "pulse is never 1 in two cycles in a row".

Show the solution

assert property (@(posedge clk) disable iff (rst) pulse |=> !pulse);

It reads: whenever pulse is 1, it must be 0 in the next cycle. Run it with random button input, and any bug that lets the detector pulse twice for one press is caught at once.

Practice 3

Find the deadlock

Machine A sends a request and waits in WAIT_ACK for an acknowledge. Machine B waits in WAIT_READY until A raises ready, and only then sends the acknowledge. A raises ready only in its IDLE state. What happens?

Show the solution

Deadlock. A waits in WAIT_ACK for B's acknowledge. B waits for ready, which A only raises in IDLE - which it will never reach, because it is waiting. Each waits for the other, for ever. The fix is in the protocol: for example, A raises ready whenever it can accept the acknowledge, including in WAIT_ACK. A timeout would also stop the hang - but it would hide the design mistake rather than fix it.

Interview corner

Interview question 1

How do you verify an FSM?

"How would you verify a state machine?"

Show the solution

"I start from the specification, not the code. I write a reference model - often the state table as data - and check the design's state and outputs against it every cycle. I drive a transition tour so that every arrow is taken, then add constrained-random input for the combinations I did not think of. I measure state and transition coverage and write directed tests for any arrow that is missing. I add assertions for the rules that must always hold: legal state, correct transitions, output rules and time limits. For anything critical, I run a formal tool to prove them, and to check for unreachable states and deadlocks. Finally, I inject faults to test the recovery from illegal states."

Interview question 2

State or transition coverage?

"Your FSM has 100% state coverage. Is that enough?"

Show the solution

"No. State coverage only shows that each state was entered. Most FSM bugs are on transitions - a wrong arrow for an unusual input, or a missing self-loop. I need transition coverage - every arrow taken - and ideally a cross of states with inputs, so that every row of the state table has been exercised. And even 100% transition coverage means nothing unless each step was also checked."

Next, Volume 13 turns to speed: why some state machines can run faster than others, and how to make the outputs clean and the critical path short.