Построение тестовых программ для проверки подсистем управления памяти микропроцессоров Евгений Корныхин научный руководитель: д.ф.-м.н. А.К.Петренко

2 Место задачи в разработке аппаратного обеспечения... output sm_out; reg [1:0] c, next_state; (posedge sm_cl) begin if (reset == 1'b1) c

3 Тестирование designа lui s1, 0x2779 ori s1, s1, 0xc8b9 lui s3, 0x4ee ori s3, s3, 0xf798 add v0, a0, a2 sub t1, t3, t5 add t7, s1, s3 Системное тестированиеМодульное тестирование Тестируется design всего микропроцессора с помощью тестовых программ Тестируется design отдельного модуля через входные и выходные сигналы

4 Системное тестирование Генерация тестов эмулятор микропроцессора (эталон) ( на Си ) cравнение трасс Возникла ошибка Успешный прогон cимуляция designа (на Verilog) тестовые программы проводится «сравнением с эталоном»

5 Построение эффективных тестов Генерация тестов ситуации факторизация пространства ситуаций нацеленные на ситуации тесты пример «ситуации»: в 1- й инструкци и возникает исключение «деление на ноль», во 2- й инструкции происходит кэш-промах

Подсистемы управления памяти (MMU) 6

Ситуации в MMU для отдельных инструкций: возникновение исключительных ситуаций промахи/попадания в кэшах разных уровней, в TLB кэшируемые/некэшируемые обращения в память отображаемые/неотображаемые вирт.адреса для цепочек инструкций: зависимости по регистрам (read/write) зависимости по адресам (одинаковые/разные физич./вирт. адреса) зависимости по содержимому (считывается то, что было записано ранее) одинаковые/разные страницы вирт.памяти одинаковые/разные строки кэш-памяти запись/чтение совместно с исключит.ситуациями 7

8 Современная практика Генерация тестов ситуации нацеленных тестов надо много ( ситуаций порядка ) современная практика: ситуации из 2-3 инструкций но не все ситуации выражаются в 2- 3 инструкциях

9 Шаблоны тестов форма ситуации – шаблон теста шаблон задает набор условий, в тесте эти условия должны быть выполнены условия DIV x, y, z LOAD y, x, c ситуация (шаблон теста) MOV x,0 MOV y,0 STORE y,x,3 STORE y,x,9 STORE y,x,7 STORE y,x,5 MOV z,0 DIV x,y,z LOAD y,x,1 тестовая программа

Существующие методы построения тестов прямое конструирование программ для ситуаций (MicroTESK) псевдослучайное дополнение шаблона до программы (SEGUE) методы сведения к системам уравнений прямая запись изменений состояния MMU последовательное решение ограничений с возвратами (Genesys-Pro, RAVEN) 10

11 Систематическое построение тестовых шаблонов выполняется на основе классификации поведения микропроцессора (модели) 1)цепочка инструкций 2)аргументы 3)варианты исполнения инструкций DIV LOAD divby0 … l 1-miss … ADD norm … DIV LOAD x,y, x, z l 1-miss ситуация (шаблон теста)... instruction set specification

12 Неэффективность существующих методов построения тестов методы на основе сведения к системам уравнений (~SAT) напрямую запись изменени я состояния даёт громоздкие уравнения ( переменных) условия DIV x, y, z LOAD y, x, c ситуация (шаблон теста) MOV x,0 MOV y,0 STORE y,x,3 STORE y,x,9 STORE y,x,7 STORE y,x,5 MOV z,0 DIV x,y,z LOAD y,x,1 тестовая программа

13 Актуальность и задача Актуальность: необходимы методы построения тестов, нацеленных на верификацию MMU в микропроцессорах с высоким уровнем параллелизма современные доступные методы не позволяют целенаправленно строить тесты для ситуаций, которые задаются шаблонами длиной более 3 инструкций, на практике требуется порядка 10 инструкций Задача: разработать метод построения нацеленных тестов, пригодный для длинных шаблонов

Компоненты генерации шаблон варианты исполнения инструкций описания блоков MMU генератор уравнений решатель уравнений конструктор текстов тестовых программ

«Структура терминов» Шаблоны (описывают, задают)... Варианты исполнения инструкций (описывают, задают набор свойств....) Описания блоков MMU...

Общее описание подхода шаблонвариантыблоки MMU assume hit/missload/store система

Общее описание подхода DIV x, y, z LOAD y, x, c шаблон теста варианты исполнения инструкции MOV x,0 MOV y,0 STORE y,x,3 STORE y,x,9 STORE y,x,7 STORE y,x,5 MOV z,0 DIV x,y,z LOAD y,x,1 тестовая программа 17

Общее описание подхода DIV x, y, z LOAD y, x, c шаблон теста варианты исполнения инструкции система уравнений/неравенств тестовая программа 18 MOV x,0 MOV y,0 STORE y,x,3 STORE y,x,9 STORE y,x,7 STORE y,x,5 MOV z,0 DIV x,y,z LOAD y,x,1 z0 = 0 0 x0, y0 < c < x0+c, l 1, l 2, l 3, l 4 < 2 32 { l 1, l 2, l 3, l 4} попарно неравны (x0+c){ l 1, l 2, l 3, l 4}

Детальное описание подхода 1. Описание вариантов исполнения инструкций, описание блоков MMU DIV x, y, z LOAD y, x, c [var x:64, y:64, z:64;] assume: z = 0^64; [var y:64, x:64; const c:16;] phys

Детальное описание подхода 2. Построение системы уравнений var x:64,y:64,z:64; const c:16; assume: z = 0^64; phys

Детальное описание подхода 3. Решение уравнений, построение текстов программ система уравнений x = 0 y = 0 z = 0 c = 1 l 1 = 3 l 2 = 9 l 3 = 7 l 4 = 5 решатель уравнений MOV x,0 MOV y,0 STORE y,x,3 STORE y,x,9 STORE y,x,7 STORE y,x,5 MOV z,0 DIV x,y,z LOAD y,x,1 тестовая программа 21

Разработаны модели 1. «модель состояния» 2. «модель инструкции» L1 { policy=LRU; lines=4; regbits=7; key(tag:24); data(d:32); keyMatch(k:24) { k = tag }; } [ var y:64, x:64; const c:4;] vAddr

Разработаны методы 1. метод построения разрешаемых уравнений 2. два метода описания стратегий вытеснения miss (phys){…} – «с момента последнего обращения к phys он вытеснен» дает определение «phys вытеснен» в виде « сумма характеристик инструкций C » доказаны теоремы корректности и полноты методов 23 дает определение «phys вытеснен» в виде свойства «исчерпания» для цепочек предыдущих инструкций

24 Апробация увеличили допустимый размер шаблонов (было 2-3, стало 8-10)

25 Апробация увеличили допустимый размер шаблонов (было 2-3, стало 8-10)

26 Реализация существующий генератор шаблонов описания инструкций (xml) конструктор текстов asm (Java) тесты (asm) ~100стр. на вариант исполнения инструкции ~2000стр. ~1000стр. уравнения (smt) стр. генератор уравнений (ruby) описания блоков MMU (xml) ~10стр. на блок шаблон теста решение равнений

27 Эксперименты увеличение допустимого размера шаблонов (было 2-3, стало 9-12) среднее время построения одного теста – 1-30с. решатель уравнений внешний (Z3)

Практическое использование микропроцессор архитектуры MIPS кэши такие-то, TLB такие-то обнаружено несколько новых критичных ошибок 28

29 Где предложенные методы работают многоуровневая кэш-память обращение в память с / без виртуальной памяти сквозная запись / отложенная запись доп.условия на строки кэш-памяти virtually indexed кэш-память virtually tagged кэш-память

30 Где эти методы НЕ работают псевдослучайное вытеснение псевдослучайный выбор блоков MMU в инструкции временные ограничения (длительности, зависимости от скорости выполнения) циклические действия (например, sqrt) кэш-память инструкций «совместная» кэш-память ( инструкции/данные, многоядерные м.пр.) но и тестирование, нацеленное на эти особенности, надо проводить иначе

31 Результаты 1. модель состояния, описывающая характеристики блоков MMU 2. модель описания инструкций в виде соотношений битовых строк и свойств наличия или отсутствия данных в блоках 3. метод построения разрешаемых уравнений для шаблонов в виде уравнений над битовыми строками без описания изменения состояния MMU 4. методы описания стратегий вытеснения c помощью уравнений над битовыми строками и ограничениями сумм бит

32 Публикации 1. статья в «Программировании» [из списка ВАК] 2. статья в «Вычислительных методах и программировании» 3-4. статьи на SYRCoSE-2008 и статья на EWDTS статьи в сборниках трудов ИСП РАН (тт.15, 17)

Примеры описаний инструкций rs rt rt rs rs rt rt temp temp арифметическое переполнение ADD rd, rs, rt

Уравнения (constraints)