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.
Hear the above talk by Iain Singleton, Engineer Advanced Verification Methodology Group at Imagination Technologies, and 8 other speakers at the free one day Formal Verification conference held at Reading, UK on Thursday, 21 May and you have the option to attend in person or via remote access.
Attendees will gain from the event whether they are just trying to learn how to apply formal verification or expert users.
Places are limited and this event often sells out so we recommend early registration.
Speaker and registration details can be found here