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. 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.

multicore microprocessors, cache memory, out-of-order execution, test system, nondeterministic behavior, model-based verification, stand-alone verification, “SPARC-V9”, “Elbrus-8C”

1. Sorin D.J., Hill M.D., Wood D.A. A Primer on Memory Consistency and Cache Coherence. Morgan and Claypool, 2011, 195 p.

2. Bergeron J. Writing testbenches: functional verification of HDL models. Boston: Kluwer Academic Publishers, 2003.

3. Stotland I, Meshkov A., Kutsevol V. Standalone functional verification of multicore microprocessor memory subsystem units based on application of memory subsystem models. Proc. оf IEEE East-West Design & Test Symposium (EWDTS 2015), Batumi, Georgia, September 26-29, 2015, pp. 326-330.

4. Kamkin A., Chupilko M. A TLM-based approach to functional verification of hardware components at different abstraction levels. Proc. оf the 12th Latin-American Test Workshop (LATW), 2011, pp. 1-6.

5. Tessier T., Lin H., Ringoen D., Hickey E., Anderson S. Designing, verifying and building an advanced L2 cache sub-system using SystemC. Proc. of Design and Verification Conference (DV-CON), 2012, pp.1-8.

6. Kamkin A., Petrochenkov M. A Model-Based Approach to Design Test Oracles for Memory Subsystems of Multicore Multiprocessors. Trudy ISP RAN / Proc. ISP RAS, vol. 27, issue 3, pp. 149-157.

7. TLM-2.0.1. TLM Transaction-Level Modeling Library. (online publication). Available at: http://www.accellera.org/downloads/standards/systemc (accessed 20.05.2016).

8. Stotland I., Lagutin A. Using stand alone behavioural models to verify microprocessor components. Voprosy radioelektroniki, seriya EVT [Issues of radio electronics], 2014, issue 3, pp. 17-27.

9. Ho R. Validation tools for complex digital designs. PhD thesis, Standford University, 1996.

10. Standard Universal Verification Methodology (online publication). Available at: http://accellera.org/downloads/standards/uvm (accessed 20.05.2016).