Skip to question
asic.fyi

Hardware interview practice

Prove an arbiter avoids deadlock and livelock

HardFormal VerificationSystemVerilog

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.

Reviewed example

Work through one case

Input
both requests stay asserted under hold-until-grant; two-requester round-robin starts with requester0 priority
Expected output
grants=01 then10; mutual exclusion and grant-implies-request hold; each request is served within two cycles

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

What to cover

Requirements

  1. Deadlock means the controller becomes stuck with pending work and no grant; livelock means it keeps changing state but never completes service.
  2. Assume a requester holds req until granted, or state another fairness assumption explicitly.
  3. Assert mutual exclusion, grant-implies-request, and a finite service bound for each persistent request.
  4. Make reset exempt from liveness obligations and choose a bound justified by the arbitration policy.
Continue practicing
Temporal ChecksAssert bounded eventual completionTemporal ChecksAssert an integer square-root pipelineTemporal ChecksProve an elastic one-hot checker