'

Построение тестовых программ для проверки подсистем управления памяти микропроцессоров

Понравилась презентация – покажи это...





Слайд 0

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


Слайд 1

2 Место задачи в разработке аппаратного обеспечения ... output sm_out; reg [1:0] c, next_state; always @ (posedge sm_cl) begin    if (reset == 1'b1) c <= 2'b00;    else c <= next_state; end ... проектные документы design на Verilog микропроцессор тестирование design’а


Слайд 2

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 отдельного модуля через входные и выходные сигналы


Слайд 3

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


Слайд 4

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


Слайд 5

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


Слайд 6

7 Неэффективность существующих методов построения тестов форма ситуации – шаблон теста шаблон задает набор условий, в тесте эти условия должны быть выполнены методы типа монте-карло неэффективны при построении тестов длиннее 3-4 инструкций DIV LOAD x, y, y, x, z c @ divby0 @ l1-miss ситуация (шаблон теста) условия


Слайд 7

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


Слайд 8

9 Неэффективность существующих методов построения тестов методы на основе сведения к системам уравнений (~SAT) сведение в виде изменений состояния даёт громоздкие уравнения (104-106 переменных) собственные решатели - это является нетривиальной задачей DIV LOAD x, y, y, x, z c @ divby0 @ l1-miss ситуация (шаблон теста) условия


Слайд 9

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


Слайд 10

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


Слайд 11

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


Слайд 12

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


Слайд 13

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


Слайд 14

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


Слайд 15

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


Слайд 16

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


Слайд 17

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


Слайд 18

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


Слайд 19

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


Слайд 20

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


Слайд 21

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


Слайд 22

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


Слайд 23

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


Слайд 24

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


Слайд 25

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


Слайд 26

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


Слайд 27

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


×

HTML:





Ссылка: