A Model-Based Approach to Design Test Oracles for Memory Subsystems of Multicore Microprocessors
Alexander Kamkin, M.V. Petrochenkov · Proceedings of the Institute for System Programming of RAS · 2015
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.