Towards the formal verification of cache coherency at the architectural level

F. Verbeek, J. Schmaltz

Onderzoeksoutput: Bijdrage aan tijdschriftTijdschriftartikelAcademicpeer review

2 Citaten (Scopus)

Samenvatting

Cache coherency is one of the major issues in multicore systems. Formal methods, in particular model-checking, have been successful at verifying high-level protocols, but, to the best of our knowledge, the verification of cache coherency at the architectural level is still an open issue. All existing verification efforts assume a reliable interconnect, that is, messages eventually reach their destination. We discuss the challenge of discharging this assumption at the architectural level where implementation details of the interconnect are mixed with a cache coherency protocol. Our automatic approach is based on a well-defined set of primitives to express architectural models, a generic model of communication fabrics expressed in an automated theorem proving system, and a dedicated algorithm for deadlock and livelock detection. We argue that reliability depends on the interaction between the interconnect and the cache coherency protocol. They must be verified altogether as their combination creates intricate message dependencies. We sketch our verification approach and apply it to a simple write-invalidate protocol on the Spidergon network-on-chip from STMicroelectronics. Our approach is promising. For this simple protocol, networks with tens of agents and hundreds of components can be analyzed within seconds.
Originele taal-2Engels
Artikelnummer20
Pagina's (van-tot)20-1/16
Aantal pagina's16
TijdschriftACM Transactions on Design Automation of Electronic Systems
Volume17
Nummer van het tijdschrift3
DOI's
StatusGepubliceerd - 2012
Extern gepubliceerdJa

Vingerafdruk

Duik in de onderzoeksthema's van 'Towards the formal verification of cache coherency at the architectural level'. Samen vormen ze een unieke vingerafdruk.

Citeer dit