Conference:Formal Verification 2015 (click here to see full programme)
Speaker:Iain Singleton, Engineer Advanced Verification Methodology Group
Organisation:Imagination Technologies Limited
Presentation Title:It’s all in the Model: Verifying Complex Arbitration Schemes using Formal
Abstract:The design of multi-transactional systems is a key to optimize performance where several masters arbitrate over a shared resource. The arbitration schemes are carefully designed to avoid hazards, race conditions, starvation and deadlocks. Arbitration verification is a challenge when policies are complex and the number of requestors is large. We present an abstract formal model within 80 lines of modelling code that uses a single assertion to exhaustively verify a range of arbiters within Imagination. We provide a reusable model that provides one of the highest levels of assurance and proves correctness in seconds for some arbiters with 256 requestors.
BiographyIain Singleton is a verification engineer in the Advanced Verification Methodologies group at Imagination Technologies. After completing his Masters from Newcastle University Iain joined Imagination last year, where he works on cutting edge pre-silicon verification of next generation products. Iain as filed two patents since he has joined Imagination.

Presentation Material

  • At the request of the speaker the Presentation Slides will not be available post-event
  • At the request of the speaker the recording will not be available post-event


Formal Verification 2015 is made possible through the generous support of our sponsors.
Formal Logo 2015