A Model-Based Approach to Design Test Oracles for Memory Subsystems of Multicore Microprocessors
https://doi.org/10.15514/ISPRAS-2015-27(3)-11
Abstract
The paper describes a method for constructing test oracles for memory subsystems of multicore microprocessors. The method is based on using nondeterministic reference models of systems under test. The key idea of the approach is on-the-fly determinization of the model behavior by using reactions from the system. Every time a nondeterministic choice appears in the reference model, additional model instances are created and launched (each simulating a possible variant of the system behavior). When the testbench receives a reaction from the system under test, it terminates all model instances whose behavior is inconsistent with that reaction. An error is detected if there is no active instance of the reference model. The suggested method has been used in verification of the L3 cache of the Elbrus-8C microprocessor and allowed to find three bugs.
About the Authors
Alexander Kamkin
ISP RAS
Russian Federation
Russian Federation
Mikhail Petrochenkov
MCST
Russian Federation
Russian Federation
References
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. Kamkin A., Petrochenkov M. Sistema podderzhki verifikatsii realizatsii protokolov kogerentnosti s ispol'zovaniem formal'nykh metodov [A system to support formal methods-based verification of coherence protocol implementations]. Voprosy radioelektroniki, seriya EVT, 2014, 3. p. 27-38.
3. Bergeron J. Writing Testbenches: Functional Verification of HDL Models. Kluwer Academic Publishers, 2000. 354 p.
4. von Bochmann G., Haar S., Jard C., Jourdan G.V. Testing Systems Specified as Partial Order Input/Output Automata. ICTSS, 2008. p. 169-183.
5. Kuliamin V., Petrenko A., Pakoulin N., Kossatchev A., Bourdonov I. Integration of Functional and Timed Testing of Real-Time and Concurrent Systems. PSI, 2003. p. 450-461.
6. Chupilko M., Kamkin A. Runtime Verification Based on Executable Models: On-the-Fly Matching of Timed Traces. MBT, EPTCS 111, 2013, p. 67-81.
7. Baratov R., Kamkin A., Maiorova V., Meshkov A., Sortov A., Yakusheva M. Trudnosti modul'noi verifikatsii apparatury na primere bufera komand mikroprotsessora «El'brus-2S» [Difficulties of the unit-level hardware verification on the example of the instruction buffer of the Elbrus-2S microprocessor]. Voprosy radioelektroniki, seriya EVT, 2013, 3. p. 84-96.
8. Kozhin A., Kozhin E., Kostenko V., Lavrov A. Kesh tret'ego urovnya i podderzhka kogerentnosti mikroprotsessora «El'brus-4S+» [L3 cache and cache coherence support in «Elbrus-4C+» microprocessor]. Voprosy radioelektroniki, seriya EVT, 2013, 3. p. 26-38.
Review
For citations:
Kamkin A., Petrochenkov M. A Model-Based Approach to Design Test Oracles for Memory Subsystems of Multicore Microprocessors. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2015;27(3):149-160. (In Russ.) https://doi.org/10.15514/ISPRAS-2015-27(3)-11
Email this article 