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

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

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

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

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

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

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

11 11 Подход модель микро процессора уравнения шаблоны тесты исполнимая модель инструкций (на Си) на шаблоне из 2 инструкций int r1; int r2 … int L1[8192]; int L2[131072]; задача поиска начальных значений переменных для выделенных ветвлений в control-flow модель на Си – много путей, много переменных

12 12 Подход : что предложено модель микро процессора уравнения шаблоны тесты 1. новая модель инструкций (меньше путей, неявное состояние) 2. способ построения уравнений из модели для шаблона 3. методика построения новой модели

13 13 Подход формализация микропроцессора уравнения шаблоны тесты предложены новые методы построения уравнений предложена специальная формализация микропроцессора (инструкций и состояния)

14 14 Подход формализация микропроцессора уравнения шаблоны тесты предложены новые методы построения уравнений предложена специальная формализация микропроцессора (инструкций и состояния)

15 Основные технические решения отказ от представления в уравнениях изменения состояния MMU компактное представление функциональности инструкции как по таким представлениям инструкций строить уравнения

16 16 Идея об отказе от описания изменения состояния MMU идея – не описывать изменение состояния, а описывать влияние одних инструкций на последующие решает проблему разрешимости уравнений сокращает количество переменных: вместо n – 10 n

17 17 Идея компактного представления инструкций обычное обращение в память: 1. вычисление эффективного адреса 2. трансляция эфф. в виртуальный адрес 3. трансляция вирт. в физический адрес 4. обращение по физ.адресу (с кэш-памятью) идея – этапы 2-4 описывать в едином виде – как обращения к «таблицам»

18 18 Идея компактного представления инструкций таблица – это модельное представление и кэш-памяти, и таблицы страниц (и даже оперативн ой памят и) «кэш-память» как таблица «таблица страниц» как таблица физ.адрес данные физический адрес данные вирт.стр. физ.кадра номер страницы виртуальной пам. номер физического кадра

19 19 Идея компактного представления инструкций всего 2 вида операций с таблицей: обращение с попаданием обращение с промахом гипотеза: таблиц и битовых строк достаточно для описания инструкций обращения к памяти

20 20 Идея о представлении обращений в таблицы в виде уравнений идея – попадание (промах) выражаются без использования состояния MMU : по адресу обращения уже было обращение данные по адресу обращения не вытеснены (вытеснены) «уже было обращение» где? среди предыдущих инструкций шаблона или инициализирующих обращений явно появились инициализирующие обращения, подготавливающие MMU перед шаблоном, в виде цепочки адресов подзадача описания вытеснения (что такое «вытеснены» ?)

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

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

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

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

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

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

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

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