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

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 Системное тестирование (core testing) Генерация тестов эталонная реализация микропроцессора ( на Си ) cравнение трасс Возникла ошибка Успешный прогон cимуляция designа (на Verilog) тестовые программы проводится «сравнением с эталоном»

5 Систематическое построение тестов Генерация тестов ситуации факторизация пространства ситуаций нацеленные на класс ситуаций тесты пример «ситуации»: «1-я инструкция даёт кэш-промах, 2-я – NOP, 3-я – безусловный переход по загруженному из памяти адресу»

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

7 Неэффективность существующих методов построения тестов форма ситуации – шаблон теста шаблон задает набор условий, в тесте эти условия должны быть выполнены методы типа монте-карло неэффективны при построении тестов длиннее 3-4 инструкций DIV LOAD x,y, x, z l 1-miss ситуация (шаблон теста) MOV z, 0 STORE z,x,3 STORE z,x,9 STORE z,x,7 STORE z,x,5 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 LOAD x,y, x, z l 1-miss ситуация (шаблон теста) MOV z, 0 STORE z,x,3 STORE z,x,9 STORE z,x,7 STORE z,x,5 DIV x, y, z LOAD y, x, 1 тест условия

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

Общее описание подхода DIV x, y, z LOAD y, x, c тестовый шаблон варианты исполнения инструкции z0 = 0 0x0,y01023, 0c15 0x0+c,t1,t2,t3,t4255 {t1,t2,t3,t4}-разные (x0+c){t1,t2,t3,t4} система уравнений MOV x,0 MOV y,0 STORE x,x,1 STORE x,x,2 STORE x,x,3 STORE x,x,4 MOV z,0 DIV x,y,z LOAD y,x,0 тестовая программа

Детальное описание подхода 1. Описание вариантов исполнения инструкций, описание кэшей, таблиц страниц и т.п. DIV x, y, z LOAD y, x, c var x:10, y:10, z:10; assume: z = 0^10; var a:10, b:10, ofs:4; phys

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

Детальное описание подхода 3. Решение уравнений, построение текстов программ система уравнений x0 = 0 y0 = 0 z0 = 0 c = 0 t1 = 1 t2 = 2 t3 = 3 t4 = 4 решатель уравнений MOV x,0 MOV y,0 STORE x,x,1 STORE x,x,2 STORE x,x,3 STORE x,x,4 MOV z,0 DIV x,y,z LOAD y,x,0 тестовая программа

это скрытый слайд

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

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

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

19 Апробация существующая среда MicroTESK (генерирует шаблоны) описания инструкций (xml) синт.анал.xml, генер.ур-ний (ruby) связь с MicroTESK, конструктор текстов asm (Java) ур-ния (smt) тесты (asm) ~100стр. на инструкцию ~2000стр. ~1000стр стр.

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

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

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

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