ASIC Point Explore

FSMs and Handshake Controllers

Catch a deadlock as a safety property, find dead states with covers, write a transition check per state, and tell deadlock, livelock and starvation apart.

Lesson
F8.4
Time
20 min
Runs on
SymbiYosys
Check
4 questions

A producer raised req and waited for ack. The consumer, written by someone else from the same one-page spec, waited for req to fall before raising ack. The two stopped on the first transfer and stayed stopped, and the simulation timeout was filed as a bench hang.

Two Machines, One Handshake, One Dead PairThe producer raises req and waits for ack. The fixed consumer raises ack while req is high. The buggy consumer waits for req to fall first, so both wait forever.
data: where the transaction goes
Two machines, one handshake, one dead pairThe producer raises req and waits for ack. The fixed consumer raises ack while req is high. The buggy consumer waits for req to fall first, so both wait forever. component P_IDLE start: raise req dead pair P_WAIT_ACK req = 1, waits for ack component P_WAIT_REL req = 0, waits for ackto fall component C_IDLE sees req dead pair C_WAIT (bug) waits for req to fallbefore ack component C_ACK ack = 1 until req falls startackreq (fixed)req (bug)!req: never comes
Read the diagram as text
  • P_IDLE: start: raise req
  • P_WAIT_ACK: req = 1, waits for ack
  • P_WAIT_REL: req = 0, waits for ack to fall
  • C_IDLE: sees req
  • C_WAIT (bug): waits for req to fall before ack
  • C_ACK: ack = 1 until req falls
  • P_IDLE → P_WAIT_ACK: start
  • P_WAIT_ACK → P_WAIT_REL: ack
  • C_IDLE → C_ACK: req (fixed)
  • C_IDLE → C_WAIT (bug): req (bug)
  • C_WAIT (bug) → C_ACK: !req: never comes

P_DONE and C_REL close the four phases and are left out of the drawing.

Deadlock Is a State Pair

The deadlock: nothing moves after step 3
01234clkfreestartp_stc_streqackWAIT_ACK and WAITreported step 4

Measured with smtbmc yices: FAIL at reported step 4, 0.5 s. p_st 1 is P_WAIT_ACK; c_st 1 is C_WAIT.

A deadlock is a pair of states neither machine can leave. "Never both waiting for each other" is safety: it fails on a finite trace, here at reported step 4. The trace names the two guards: the producer waits for ack, the consumer waits for !req.

One Cover per State, One Check per State

StateFixed designBUG_DEADLOCKBUG_LIVELOCK
P_IDLEstep 2step 2step 2
P_WAIT_ACKstep 3step 3step 3
P_WAIT_RELstep 5not reached within 20not reached within 20
P_DONEstep 7not reached within 20not reached within 20
P_BACKOFFnot reached within 20not reached within 20step 4
C_IDLEstep 2step 2step 2
C_WAITnot reached within 20step 4not reached within 20
C_ACKstep 4not reached within 20step 4
C_RELstep 6not reached within 20step 5
donestep 7not reached within 20not reached within 20
second donestep 13not reached within 20not reached within 20

Cover mode, depth 20, smtbmc yices. Each cell is the reported step of the shortest trace to that cover.

On the fixed design two states are never reached: C_WAIT and P_BACKOFF exist only for the buggy guards. An unreached state is dead code or an over-constraint (F3.5); here it is dead code to delete. On each buggy design the cover for done stops reaching.

Illegal transitions are checks over last cycle's state: from each state, the next state is in its row of the FSM table. Generated from the table, they fire on the deadlock at step 4. Automatic FSM checks (F5.2) produce exactly these covers and checks from the encoding.

Three Shapes of "stuck"

The livelock: both machines move, nothing completes
01234567891011clkreqackretry_cnt01234doneretry_cnt = 4reported step 11

Measured: FAIL at reported step 11, 0.5 s. done never rises.

ShapeWhat the trace showsWritten here asMeasured
Deadlockboth machines frozensafety on the state pairFAIL at reported step 4
Livelockboth move, nothing completesbounded: retry_cnt < 4FAIL at reported step 11
Starvationone requester never winsbounded wait per requester (F8.2)see F8.2

Livelock and starvation are liveness properties; their bounded forms are safety and run in bmc. F3.7 shows the liveness view.

In the livelock trace the producer withdraws req one cycle after raising it. The ack arrives just as req falls, so the consumer releases and the producer retries. The bench counts the withdrawals. The cover for done tells the same story with no bound to choose: it is unreached on both buggy designs.

The Proof

Fixed design: dead pair, transitions, retry boundMeasured result
bmc depth 20BMC PASS to depth 20, 0.6 s
prove k = 2UNKNOWN at k = 2 (base case passed, induction step failed), 0.5 s
prove k = 4Prove PASS (k = 4), 0.5 s

hs_pc has 5 flops: the two state registers.

The retry counter is bench state, and an induction start may hold any value of it. Four steps of history pin it to what the machines can do.

Asked in Interviews

QuestionAnswer
How does formal find a deadlock?As a safety property over the state pair. The trace shows the two guards that wait on each other.
How do you check an FSM has no unreachable states and no illegal transitions?A cover per state, and a check per state that the next state is in its allowed set.
Deadlock, livelock, starvation?Frozen, moving without progress, one party never served. The first is a state pair; the other two are liveness, often checked in bounded form.

Try It

The lab task. The twins switch the bug, the checks and the mode.
[options]
mode bmc
depth 20
[engines]
smtbmc yices
[script]
read_verilog -formal -sv design.sv
prep -top hs_pc
[files]
design.sv
In concurrent SVA: the dead pair, one transition row, the retry bound and one state cover.
assert property (@(posedge clk) disable iff (rst) !(p_st == P_WAIT_ACK && c_st == C_WAIT));
assert property (@(posedge clk) disable iff (rst) $past(p_st) == P_WAIT_ACK |-> p_st inside {P_WAIT_ACK, P_WAIT_REL});
assert property (@(posedge clk) disable iff (rst) retry_cnt < 4);
cover property (@(posedge clk) disable iff (rst) c_st == C_WAIT);
As the engine runs it. f_past_valid keeps the transition checks off the first cycle.
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  reg f_past_valid = 0;                // a previous cycle exists
  reg [2:0] p_q = 0;                     // last cycle's states: the registered form of $past
  reg [1:0] c_q = 0;
  reg [2:0] retry_cnt = 0;               // back-offs since the last completed transfer
  reg [1:0] n_done = 0;                  // completed transfers, saturating at 3
  always @(posedge clk) begin
    f_past_valid <= !rst; p_q <= p_st; c_q <= c_st;
    retry_cnt <= rst || done ? 3'd0 : p_st == P_BACKOFF && retry_cnt != 3'd7 ? retry_cnt + 3'd1 : retry_cnt;
    n_done <= rst ? 2'd0 : done && n_done != 2'd3 ? n_done + 2'd1 : n_done;
  end
  always @(posedge clk) if (!rst) begin
    assert(!(p_st == P_WAIT_ACK && c_st == C_WAIT));   // never both waiting for each other
    assert(retry_cnt < 3'd4);                         // a transfer completes within four tries
  end
  always @(posedge clk) if (!rst && f_past_valid) begin   // each state goes only where the table allows
    if (p_q == P_IDLE) assert(p_st == P_IDLE || p_st == P_WAIT_ACK);
    if (p_q == P_WAIT_ACK) assert(p_st == P_WAIT_ACK || p_st == P_WAIT_REL);
    if (p_q == P_WAIT_REL) assert(p_st == P_WAIT_REL || p_st == P_DONE);
    if (p_q == P_DONE) assert(p_st == P_IDLE);
    if (c_q == C_IDLE) assert(c_st == C_IDLE || c_st == C_ACK);
    if (c_q == C_ACK) assert(c_st == C_ACK || c_st == C_REL);
    if (c_q == C_REL) assert(c_st == C_IDLE);
  end

  1. Covers

    Run the fixed-design cover twin and fill the state table. Which states never appear?

  2. Deadlock

    Run as loaded: FAIL at reported step 4. Name the guard each machine is stuck on.

  3. Fix and prove

    Send the consumer from C_IDLE straight to C_ACK, then prove the fixed design at k = 2 and k = 4.

design.sv

props.sv

Use assert property (@(posedge clk) ...);. Leave blank for immediate assertions in the design.

Inputs are free unless constrained. Run to find a counterexample or check a proof.

Model: one positive-edge clock, binary data. Sampled history requires declaration-initialized variables; primary-input history is unsupported.

SBY summary and log

    
Check Yourself

      

        
Predict the outpuths_pc with BUG_DEADLOCK, mode cover, default depth 20, smtbmc yices, reset assumed in step 0, the full cover list (every state, done, a second done). The verdict is:
      
module hs_pc(input clk, rst, start, output req, output ack, output done);
  localparam P_IDLE = 3'd0, P_WAIT_ACK = 3'd1, P_WAIT_REL = 3'd2, P_DONE = 3'd3, P_BACKOFF = 3'd4;
  localparam C_IDLE = 2'd0, C_WAIT = 2'd1, C_ACK = 2'd2, C_REL = 2'd3;
  reg [2:0] p_st = P_IDLE;
  reg [1:0] c_st = C_IDLE;
  assign req = p_st == P_WAIT_ACK;
  assign ack = c_st == C_ACK;
  assign done = p_st == P_DONE;
  always @(posedge clk)
    if (rst) begin p_st <= P_IDLE; c_st <= C_IDLE; end
    else begin
      case (p_st)                                   // producer
        P_IDLE:     if (start) p_st <= P_WAIT_ACK;
        P_WAIT_ACK: if (ack) p_st <= P_WAIT_REL;
        P_WAIT_REL: if (!ack) p_st <= P_DONE;
        P_DONE:     p_st <= P_IDLE;
        default:    p_st <= P_WAIT_ACK;             // P_BACKOFF: retry
      endcase
      case (c_st)                                   // consumer
        C_IDLE: if (req) c_st <= C_WAIT;   // bug: waits for req to drop first
        C_WAIT: if (!req) c_st <= C_ACK;
        C_ACK:  if (!req) c_st <= C_REL;
        default: c_st <= C_IDLE;                    // C_REL
      endcase
    end
`ifdef FORMAL
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  reg f_past_valid = 0;                // a previous cycle exists
  reg [2:0] p_q = 0;                     // last cycle's states: the registered form of $past
  reg [1:0] c_q = 0;
  reg [2:0] retry_cnt = 0;               // back-offs since the last completed transfer
  reg [1:0] n_done = 0;                  // completed transfers, saturating at 3
  always @(posedge clk) begin
    f_past_valid <= !rst; p_q <= p_st; c_q <= c_st;
    retry_cnt <= rst || done ? 3'd0 : p_st == P_BACKOFF && retry_cnt != 3'd7 ? retry_cnt + 3'd1 : retry_cnt;
    n_done <= rst ? 2'd0 : done && n_done != 2'd3 ? n_done + 2'd1 : n_done;
  end
  always @(posedge clk) if (!rst) begin
    c_p_idle: cover(p_st == P_IDLE);
    c_p_wait_ack: cover(p_st == P_WAIT_ACK);
    c_p_wait_rel: cover(p_st == P_WAIT_REL);
    c_p_done: cover(p_st == P_DONE);
    c_p_backoff: cover(p_st == P_BACKOFF);
    c_c_idle: cover(c_st == C_IDLE);
    c_c_wait: cover(c_st == C_WAIT);
    c_c_ack: cover(c_st == C_ACK);
    c_c_rel: cover(c_st == C_REL);
    c_done: cover(done);
    c_done2: cover(done && n_done == 2'd1);   // the second completion
  end
`endif
endmodule


      

      

      


ConceptWhich FSM property is the wrong one to write?


ConceptDeadlock, livelock, starvation: which is a safety property as written in this lesson?


Read the waveformIn the deadlock trace, which signal is each machine waiting for?
The deadlock: nothing moves after step 3

    
  01234clkfreestartp_stc_streqackWAIT_ACK and WAITreported step 4
Measured with smtbmc yices: FAIL at reported step 4, 0.5 s. p_st 1 is P_WAIT_ACK; c_st 1 is C_WAIT.

        

        
      

    

    
Remember
  • Deadlock is a state pair: assert the pair never happens and bmc finds it in a few steps.
  • One cover per state: unreached states are dead code or over-constraint.
  • One transition check per state, generated from the FSM table, catches a wrong guard at once.
  • Livelock and starvation are liveness; bounded counters make them safety you can run.