Метод генерации тестовых программ на основе формальных спецификаций механизмов кэширования и трансляции адресов

В данной работе предложен метод генерации тестовых программ для функциональной верификации блока управления памятью микропроцессора. В основе метода лежат формальные спецификации инструкций доступа к памяти, а именно инструкций чтения и записи, и устройств памяти, таких как блоки кэш-памяти и буферы трансляции адресов. Использование формальных спецификаций помогает автоматизировать разработку генераторов тестовых программ и обеспечивает систематичность верификации благодаря четкому определению целей тестирования. В предложенном подходе тестовые программы составляются при помощи комбинаторных методов. Т.е. тестовые воздействия (последовательности инструкций чтения и записи) создаются путем перечисления всех возможных комбинаций инструкций, ситуаций (путей выполнения инструкций) и зависимостей (множеств конфликтов между инструкциями). Важно отметить, что тестовые ситуации и зависимости автоматически извлекаются из спецификаций. Данный подход применялся в нескольких промышленных проектах и позволил выявить критические ошибки в механизмах управления памятью.

микропроцессоры, управление памятью, кэширование, трансляция адресов, функциональная верификация, формальные спецификации, генерация тестовых программ, генерация потока инструкций

1. Bryant R.E., O’Hallaron D.R. Computer Systems: A Programmer’s Perspective. Pearson, 2010. 1080 p.

2. Adir A., Almog E., Fournier L, Marcus E., Rimon M., Vinov M., Ziv A. Genesys-Pro: Innovations in Test Program Generation for Functional Processor Verification. Design & Test of Computers, 2004. pp. 84-93.

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

4. Adir A., Fournier L., Katz Y., Koyfman A. DeepTrans – Extending the Model-based Approach to Functional Verification of Address Translation Mechanisms. High-Level Design Validation and Test Workshop, 2006. pp. 102-110.

5. Д.Н. Воробьев, А.С. Камкин. Генерация тестовых программ для подсистемы управления памятью микропроцессора. Труды ИСП РАН, 17, 2009. с. 119-132.

6. Kamkin A., Tatarnikov A. MicroTESK: An ADL-Based Reconfigurable Test Program Generator for Microprocessors. Spring/Summer Young Researchers’ Colloquium on Software Engineering, 2012, pp. 64-69.

7. Страница инструмента MicroTESK — http://forge.ispras.ru/projects/microtesk

8. Freericks M. The nML Machine Description Formalism. Technical Report TR SM-IMP/DIST/08, TU Berlin CS Department, 1993.

9. MIPS64™ Architecture For Programmers. MIPS Technologies Inc.

10. Страница библиотеки Fortress — http://forge.ispras.ru/projects/solver-api