A specification-driven method for automating simulation-based verification of pipelined microprocessors.
The thesis is devoted to automation of simulation-based verification of microprocessors. The result is a set of methods and tools for unit- and system-level testing. The approach to unit testing is based on specifying pre- and post-conditions of micro-operations (pipe stages); the developed tools allows cycle-accurately describing microprocessor units, automatically generating sequences of test actions and checking behavior of the units in response to those actions. The system-level approach involves instruction set specifications, combinatorial test template enumeration and constraint-driven test data generation; the developed tools allows automatically constructing assembly programs targeted at reaching particular conditions in the microprocessor state. The software created in the context of this work has been used in SRISA RAS for testing units and subsystems of the Komdiv64-SMP microprocessor (the translation lookaside buffer, the L2 cache unit and the memory management unit), the Komdiv64 microprocessor core and the Komdiv128 arithmetical co-processor. As a result, dozens of bugs, including critical ones, have been discovered.Full text of the paper in pdf (in Russian)
Diss. Institute for System Programming of the Russian Academy of Sciences, 2009.