
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.
недетерминированное поведение, Electronic computers. Computer science, кэш-память, «sparc-v9», тестовая система, автономная верификация, QA75.5-76.95, микропроцессор «эльбрус», MULTICORE MICROPROCESSORS,CACHE MEMORY,OUT-OF-ORDER EXECUTION,TEST SYSTEM,NONDETERMINISTIC BEHAVIOR,MODEL-BASED VERIFICATION,STAND-ALONE VERIFICATION,"SPARC-V9","ELBRUS-8C",МНОГОЯДЕРНЫЙ МИКРОПРОЦЕССОР,КЭШ-ПАМЯТЬ,ВНЕОЧЕРЕДНОЕ ИСПОЛНЕНИЕ,ТЕСТОВАЯ СИСТЕМА,НЕДЕТЕРМИНИРОВАННОЕ ПОВЕДЕНИЕ,ВЕРИФИКАЦИЯ НА ОСНОВЕ ЭТАЛОННЫХ МОДЕЛЕЙ,АВТОНОМНАЯ ВЕРИФИКАЦИЯ,МИКРОПРОЦЕССОР "ЭЛЬБРУС", внеочередное исполнение, верификация на основе эталонных моделей, многоядерный микропроцессор
недетерминированное поведение, Electronic computers. Computer science, кэш-память, «sparc-v9», тестовая система, автономная верификация, QA75.5-76.95, микропроцессор «эльбрус», MULTICORE MICROPROCESSORS,CACHE MEMORY,OUT-OF-ORDER EXECUTION,TEST SYSTEM,NONDETERMINISTIC BEHAVIOR,MODEL-BASED VERIFICATION,STAND-ALONE VERIFICATION,"SPARC-V9","ELBRUS-8C",МНОГОЯДЕРНЫЙ МИКРОПРОЦЕССОР,КЭШ-ПАМЯТЬ,ВНЕОЧЕРЕДНОЕ ИСПОЛНЕНИЕ,ТЕСТОВАЯ СИСТЕМА,НЕДЕТЕРМИНИРОВАННОЕ ПОВЕДЕНИЕ,ВЕРИФИКАЦИЯ НА ОСНОВЕ ЭТАЛОННЫХ МОДЕЛЕЙ,АВТОНОМНАЯ ВЕРИФИКАЦИЯ,МИКРОПРОЦЕССОР "ЭЛЬБРУС", внеочередное исполнение, верификация на основе эталонных моделей, многоядерный микропроцессор
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 0 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
