Towards the formal verification of cache coherency at the architectural level

F. Verbeek, J. Schmaltz

Research output: Contribution to journalArticleAcademicpeer-review

2 Citations (Scopus)

Abstract

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.
Original languageEnglish
Article number20
Pages (from-to)20-1/16
Number of pages16
JournalACM Transactions on Design Automation of Electronic Systems
Volume17
Issue number3
DOIs
Publication statusPublished - 2012
Externally publishedYes

Fingerprint

Dive into the research topics of 'Towards the formal verification of cache coherency at the architectural level'. Together they form a unique fingerprint.

Cite this