Ivannikov Institute for System Programming of the RAS

A System to Support Formal Methods-Based Verification of Coherence Protocol Implementations.


A. Kamkin, M. Petrochenkov.


The paper describes an approach to develop test systems aimed at verification of RTL implementations of memory coherence protocols. Tasks for verification of memory management mechanisms of multi-core microprocessors are analyzed; basing on the analysis, a test system architecture is suggested. The emphasis is put on such a task as deterministic replay of tests constructed with the help of formal methods. An experience of applying the suggested approach to the Elbrus-2S microprocessor is considered.


memory consistency, coherence protocols, verification, testing, model checking, deterministic replay.


Voprosy radioehlektroniki [Issues of Radio Electronics], no. 3, 2014. P. 27-38.

Research Group

Software Engineering

All publications during 2014 All publications