Approaches to Stand-alone Verification of Multicore Microprocessor Caches
The paper presents an overview of approaches used in verifying correctness of multicore microprocessors caches. Common properties of memory subsystem devices and those specific to caches are described. We describe the method to support memory consistency in a system using cache coherence protocol. T...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Ivannikov Institute for System Programming of the Russian Academy of Sciences
2018-10-01
|
| Series: | Труды Института системного программирования РАН |
| Subjects: | |
| Online Access: | https://ispranproceedings.elpub.ru/jour/article/view/115 |
| _version_ | 1818662808835850240 |
|---|---|
| author | M. . Petrochenkov I. . Stotland R. . Mushtakov |
| author_facet | M. . Petrochenkov I. . Stotland R. . Mushtakov |
| author_sort | M. . Petrochenkov |
| collection | DOAJ |
| description | The paper presents an overview of approaches used in verifying correctness of multicore microprocessors caches. Common properties of memory subsystem devices and those specific to caches are described. We describe the method to support memory consistency in a system using cache coherence protocol. The approaches for designing a test system, generating valid stimuli and checking the correctness of the device under verification (DUV) are introduced. Adjustments to the approach for supporting generation of out-of-order test stimuli are provided. Methods of the test system development on different abstraction levels are presented. We provide basic approach to device behavior checking - implementing a functional reference model, reactions of this model could be compared to device reactions, miscompare denotes an error. Methods for verification of functionally nondeterministic devices are described: the «gray box» method based on elimination of nondeterministic behavior using internal interfaces of the implementation and the novel approach based on the dynamic refinement of the behavioral model using device reactions. We also provide a way to augment a stimulus generator with assertions to further increase error detection capabilities of the test system. Additionally, we describe how the test systems for devices, that support out of order execution, could be designed. We present the approach to simplify checking of nondeterministic devices with out-of-order execution of requests using a reference order of instructions. In conclusion, we provide the case study of using these approaches to verify caches of microprocessors with “Elbrus” architecture and “SPARC-V9” architecture. |
| first_indexed | 2024-12-17T05:06:50Z |
| format | Article |
| id | doaj.art-8cb468c606d64161ac2ec078e6183c72 |
| institution | Directory Open Access Journal |
| issn | 2079-8156 2220-6426 |
| language | English |
| last_indexed | 2024-12-17T05:06:50Z |
| publishDate | 2018-10-01 |
| publisher | Ivannikov Institute for System Programming of the Russian Academy of Sciences |
| record_format | Article |
| series | Труды Института системного программирования РАН |
| spelling | doaj.art-8cb468c606d64161ac2ec078e6183c722022-12-21T22:02:24ZengIvannikov Institute for System Programming of the Russian Academy of SciencesТруды Института системного программирования РАН2079-81562220-64262018-10-0128316117210.15514/ISPRAS-2016-28(3)-10115Approaches to Stand-alone Verification of Multicore Microprocessor CachesM. . Petrochenkov0I. . Stotland1R. . Mushtakov2АО «МЦСТЭ»АО «МЦСТЭ»АО «МЦСТЭ»The paper presents an overview of approaches used in verifying correctness of multicore microprocessors caches. Common properties of memory subsystem devices and those specific to caches are described. We describe the method to support memory consistency in a system using cache coherence protocol. The approaches for designing a test system, generating valid stimuli and checking the correctness of the device under verification (DUV) are introduced. Adjustments to the approach for supporting generation of out-of-order test stimuli are provided. Methods of the test system development on different abstraction levels are presented. We provide basic approach to device behavior checking - implementing a functional reference model, reactions of this model could be compared to device reactions, miscompare denotes an error. Methods for verification of functionally nondeterministic devices are described: the «gray box» method based on elimination of nondeterministic behavior using internal interfaces of the implementation and the novel approach based on the dynamic refinement of the behavioral model using device reactions. We also provide a way to augment a stimulus generator with assertions to further increase error detection capabilities of the test system. Additionally, we describe how the test systems for devices, that support out of order execution, could be designed. We present the approach to simplify checking of nondeterministic devices with out-of-order execution of requests using a reference order of instructions. In conclusion, we provide the case study of using these approaches to verify caches of microprocessors with “Elbrus” architecture and “SPARC-V9” architecture.https://ispranproceedings.elpub.ru/jour/article/view/115многоядерный микропроцессоркэш-памятьвнеочередное исполнениетестовая системанедетерминированное поведениеверификация на основе эталонных моделейавтономная верификация«sparc-v9»микропроцессор «эльбрус» |
| spellingShingle | M. . Petrochenkov I. . Stotland R. . Mushtakov Approaches to Stand-alone Verification of Multicore Microprocessor Caches Труды Института системного программирования РАН многоядерный микропроцессор кэш-память внеочередное исполнение тестовая система недетерминированное поведение верификация на основе эталонных моделей автономная верификация «sparc-v9» микропроцессор «эльбрус» |
| title | Approaches to Stand-alone Verification of Multicore Microprocessor Caches |
| title_full | Approaches to Stand-alone Verification of Multicore Microprocessor Caches |
| title_fullStr | Approaches to Stand-alone Verification of Multicore Microprocessor Caches |
| title_full_unstemmed | Approaches to Stand-alone Verification of Multicore Microprocessor Caches |
| title_short | Approaches to Stand-alone Verification of Multicore Microprocessor Caches |
| title_sort | approaches to stand alone verification of multicore microprocessor caches |
| topic | многоядерный микропроцессор кэш-память внеочередное исполнение тестовая система недетерминированное поведение верификация на основе эталонных моделей автономная верификация «sparc-v9» микропроцессор «эльбрус» |
| url | https://ispranproceedings.elpub.ru/jour/article/view/115 |
| work_keys_str_mv | AT mpetrochenkov approachestostandaloneverificationofmulticoremicroprocessorcaches AT istotland approachestostandaloneverificationofmulticoremicroprocessorcaches AT rmushtakov approachestostandaloneverificationofmulticoremicroprocessorcaches |