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

Authors

A. Kamkin, M. Petrochenkov.

Abstract

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.

Keywords

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

Edition

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

Research Group

Software Engineering

All publications during 2014

All publications