Preview

Труды Института системного программирования РАН

Расширенный поиск

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

https://doi.org/10.15514/ISPRAS-2015-27(3)-9

Полный текст:

Аннотация

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

Об авторах

А. С. Камкин
ИСП РАН
Россия


А. С. Проценко
ИСП РАН
Россия


А. Д. Татарников
ИСП РАН
Россия


Список литературы

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


Для цитирования:


Камкин А.С., Проценко А.С., Татарников А.Д. Метод генерации тестовых программ на основе формальных спецификаций механизмов кэширования и трансляции адресов. Труды Института системного программирования РАН. 2015;27(3):125-138. https://doi.org/10.15514/ISPRAS-2015-27(3)-9

For citation:


Kamkin A..., Protsenko A..., Tatarnikov A... An Approach to Test Program Generation Based on Formal Specifications of Caching and Address Translation Mechanisms. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2015;27(3):125-138. (In Russ.) https://doi.org/10.15514/ISPRAS-2015-27(3)-9

Просмотров: 114


Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 2079-8156 (Print)
ISSN 2220-6426 (Online)