A System to Support Formal Methods-Based Verification of Coherence Protocol Implementations.
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.
Voprosy radioehlektroniki [Issues of Radio Electronics], no. 3, 2014. P. 27-38.