|
ИСТИНА |
Войти в систему Регистрация |
ИПМех РАН |
||
An Approach to Test Program Generation Based on Formal Specifications of Caching and Address Translation Mechanismsстатья
Статья опубликована в журнале из списка RSCI Web of Science
Статья опубликована в журнале из перечня ВАКДата последнего поиска статьи во внешних источниках: 20 апреля 2016 г.
- Авторы: Kamkin A., Protsenko A., Tatarnikov A.
- Журнал: Труды Института системного программирования РАН (электронный журнал)
- Том: 27
- Номер: 3
- Год издания: 2015
- Первая страница: 125
- Последняя страница: 138
- DOI: 10.15514/ISPRAS-2015-27(3)-9
- Аннотация: In this work, an approach to generate test programs for functional verification of memory management units of microprocessors is proposed. The approach is based on formal specification of memory access instructions, namely load and store instructions, and memory devices such as cache units and address translation buffers. The use of formal specifications helps automate development of test program generators and makes verification systematic due to clear definition of testing goals. In the suggested approach, test programs are constructed by using combinatorial techniques, which means that stimuli – sequences of loads and stores – are created by enumerating all feasible combinations of instructions, situations (instruction execution paths) and dependencies (sets of conflicts between instructions). It is of importance that test situations and dependencies are automatically extracted from specifications. The approach has been used in a number of industrial projects and allowed to discover critical bugs in memory management mechanisms.
- Добавил в систему: Камкин Александр Сергеевич