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

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- й инструкции происходит кэш-промах

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

7 Неэффективность существующих методов построения тестов форма ситуации – шаблон теста шаблон задает набор условий, в тесте эти условия должны быть выполнены методы типа монте-карло неэффективны при построении тестов длиннее 3 инструкций условия 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 тестовая программа

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

9 Неэффективность существующих методов построения тестов методы на основе сведения к системам уравнений (~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 тестовая программа

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

Общее описание подхода 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 тестовая программа 11

Общее описание подхода DIV x, y, z LOAD y, x, c шаблон теста варианты исполнения инструкции система уравнений/неравенств тестовая программа 12 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:4;] phys

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

Детальное описание подхода 3. Решение уравнений, построение текстов программ система уравнений x = 0 y = 0 z = 0 c = 1 t1 = 3 t2 = 9 t3 = 7 t4 = 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 тестовая программа 15

Разработаны модели 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 » доказаны теоремы корректности и полноты методов 17 дает определение «phys вытеснен» в виде свойства «исчерпания» для цепочек предыдущих инструкций

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

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

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

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

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

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

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

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