ИСТИНА

Contemporary trend to develop multi-core microprocessors is accompanied with verification difficulties. The complexity of cache coherence protocols (CCPs) prevents from complete verification of shared memory subsystems by means of widely used random test-program generators (TPGs). To target the problem is possible by means of the following steps. The first step is to separately specify CCP features and generate protocol-specific events to be used in a TPG when generating a test program (TP). We suggest specifying the protocol in Promela, and then receive a test template (TT) by means of Spin. This approach also allows generation of testbenches in UVM (or C++TESK, our own methodology for unit-level verification) to check cores stand-alone (abstract interface to pin level binding is necessary) and to make the execution of the resulting TPs to be controllable and deterministic. The second step is to let TPG produce the memory access instructions causing desired CPP-specific behavior. As a TPG we use MicroTESK, being a reconfigurable (retargetable and extendable) model-based TPG for microprocessors and other programmable devices. Its Ruby-based TTs abstractly describe future instruction sequences. MicroTESK's test sequence generator easily processes that TT making TP with CCP-specific events. The resulting TP is executed together with the unit-level testbench to exactly reproduce the situation Spin had found to be important for such a protocol. As a result, the final TPs contain instructions to check general functionality, and instructions for difficult-to-approach communication part of the microprocessor.