Q065FreeDesign Verification

Prove an arbiter avoids deadlock and livelock

Difficulty: Hard
Topic: Formal Verification
Language: SV

Interview prompt

Question

For a two-requester arbiter, distinguish deadlock from livelock and write formal checks for bounded progress under a hold-until-grant contract. Assume work-conserving round-robin arbitration, where each sampled grant completes service and there is no separate downstream ready signal. Use the conservative checker deadline C through C+2 inclusive for a request sampled at edge C.

Candidate starting point

Implementation scaffold

module arbiter_progress_checks (
  input logic       clk,
  input logic       rst_n,
  input logic [1:0] req,
  input logic [1:0] gnt,
  input logic [1:0] state
);
  // Environment contract: a request persists until its service grant.
  property p_hold_request0;
    // TODO: Implement hold_request0 with the stated clock, reset and timing contract.
  endproperty
  a_hold_request0: assume property (p_hold_request0);
  property p_hold_request1;
    // TODO: Implement hold_request1 with the stated clock, reset and timing contract.
  endproperty
  a_hold_request1: assume property (p_hold_request1);

  // Immediate safety properties.
  property p_exclusive_grant;
    // TODO: Implement exclusive_grant with the stated clock, reset and timing contract.
  endproperty
  a_exclusive_grant: assert property (p_exclusive_grant);
  property p_grant_has_request;
    // TODO: Implement grant_has_request with the stated clock, reset and timing contract.
  endproperty
  a_grant_has_request: assert property (p_grant_has_request);
  property p_known_state;
    // TODO: Implement known_state with the stated clock, reset and timing contract.
  endproperty
  a_known_state: assert property (p_known_state);

  // Bounded progress for a two-way round-robin policy.
  property p_progress0;
    // TODO: Implement progress0 with the stated clock, reset and timing contract.
  endproperty
  a_progress0: assert property (p_progress0);
  property p_progress1;
    // TODO: Implement progress1 with the stated clock, reset and timing contract.
  endproperty
  a_progress1: assert property (p_progress1);

  // Cover simultaneous contention so the proof explores the hard case.
  property p_contention;
    // TODO: Implement contention with the stated clock, reset and timing contract.
  endproperty
  c_contention: cover property (p_contention);
endmodule

// TODO: Distinguish deadlock from livelock and justify the stated conservative progress bound under the supplied policy.

Reviewed example

Trace one case

Input

At edges C0 through C3, req=2'b11 throughout. The work-conserving round-robin arbiter starts with requester 0 priority.

Expected output

Grants at C0, C1, C2, C3 are 01, 10, 01, 10. Each persistent requester is served within two service opportunities and therefore also satisfies the conservative C..C+2 checker.

The grant completes service on its sampling edge. A trace with pending work and no grants fails bounded progress whether the internal state is stuck or keeps changing. Proving these assertions requires a formal engine and the composed arbiter; a simulation trace is only a check of selected behavior.

What to cover

Requirements

Deadlock means the controller becomes stuck with pending work and no grant; livelock means it keeps changing state but never completes service.
Assume a requester keeps req asserted on subsequent sampled edges while its request remains ungranted.
Assert mutual exclusion, grant-implies-request, known control state, and a grant for each sampled request at that edge or either of the next two edges.
Disable these checks during reset. Explain why this finite deadline is valid for the stated work-conserving two-way round-robin policy.

Continue practicing

Q1049 · Assertions and FormalProve a fair round-robin arbiterHardP Q046 · Temporal ChecksProve an elastic one-hot checkerHard Q011 · Temporal ChecksSystemVerilog Assertions (SVA) disable iffEasy Q390 · Temporal ChecksVacuityMediumP Q670 · Assertions and FormalClassify a formal propertyEasyP

module arbiter_progress_checks ( input logic clk, input logic rst_n, input logic [1:0] req, input logic [1:0] gnt, input logic [1:0] state ); // Environment contract: a request persists until its service grant. property p_hold_request0; // TODO: Implement hold_request0 with the stated clock, reset and timing contract. endproperty a_hold_request0: assume property (p_hold_request0); property p_hold_request1; // TODO: Implement hold_request1 with the stated clock, reset and timing contract. endproperty a_hold_request1: assume property (p_hold_request1); // Immediate safety properties. property p_exclusive_grant; // TODO: Implement exclusive_grant with the stated clock, reset and timing contract. endproperty a_exclusive_grant: assert property (p_exclusive_grant); property p_grant_has_request; // TODO: Implement grant_has_request with the stated clock, reset and timing contract. endproperty a_grant_has_request: assert property (p_grant_has_request); property p_known_state; // TODO: Implement known_state with the stated clock, reset and timing contract. endproperty a_known_state: assert property (p_known_state); // Bounded progress for a two-way round-robin policy. property p_progress0; // TODO: Implement progress0 with the stated clock, reset and timing contract. endproperty a_progress0: assert property (p_progress0); property p_progress1; // TODO: Implement progress1 with the stated clock, reset and timing contract. endproperty a_progress1: assert property (p_progress1); // Cover simultaneous contention so the proof explores the hard case. property p_contention; // TODO: Implement contention with the stated clock, reset and timing contract. endproperty c_contention: cover property (p_contention); endmodule // TODO: Distinguish deadlock from livelock and justify the stated conservative progress bound under the supplied policy.

Question

Implementation scaffold

Trace one case

Requirements

Related questions

Question

Implementation scaffold

Trace one case

Requirements

Related questions