1,000+ ASIC Interview Questions: SystemVerilog, UVM & RTL

DescriptionQ177

Q177DVDesignASIC interview problem

Prove an arbiter avoids deadlock and livelock

TechniquesDeadlockLivelockLivenessSVA

DifficultyHard

TopicFormal Verification

LanguageSystemVerilog

Requirements4 checkpoints

Problem

For a two-requester arbiter, distinguish deadlock from livelock and write formal checks that prove requests make bounded progress under a hold-until-grant environment contract.

Example input and output

Use this case to check your interpretation

Input

both requests stay asserted under hold-until-grant; two-requester round-robin starts with requester0 priority

Output

grants=01 then10; mutual exclusion and grant-implies-request hold; each request is served within two cycles

Explanation

The finite round-robin bound proves persistent work cannot deadlock or livelock under the stated environment assumption.

Requirements (4)

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 holds req until granted, or state another fairness assumption explicitly.
Assert mutual exclusion, grant-implies-request, and a finite service bound for each persistent request.
Make reset exempt from liveness obligations and choose a bound justified by the arbitration policy.