'

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

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





Слайд 1

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


Слайд 2

Евгений Корныхин 2 Верификация моделей аппаратного обеспечения 70% общих усилий, 80% общего объема кода имитационное тестирование моделей – компрописс между ценой и качеством верификации моделей имитационное тестирование на системном уровне – системное тестирование


Слайд 3

Евгений Корныхин 3 Системное тестирование микропроцессоров тестовая система модель CPU машинная программа протокол исполнения


Слайд 4

Евгений Корныхин 4 Методы автоматической генерации программ случайная генерация целенап- равленная генерация (constraints) коммерческие инструменты (Genesys-Pro, RAVEN) сложность генерации разнообразие произошедших ситуаций


Слайд 5

Евгений Корныхин 5 Методы автоматической генерации программ случайная генерация целенап- равленная генерация (constraints) RAVEN сложность генерации разнообразие произошедших ситуаций Genesys-Pro


Слайд 6

Евгений Корныхин 6 Основанная на моделях генерация программ модели генератор тестовая программа шаблон программы


Слайд 7

Евгений Корныхин 7 Основанная на моделях генерация программ тестовая программа шаблон программы 1. экспертный этап 2. механический этап


Слайд 8

Евгений Корныхин 8 Основанная на моделях генерация программ модели генератор тестовая программа шаблон программы


Слайд 9

Евгений Корныхин 9 Тестовый шаблон что такое программа, соответствующая шаблону (с инициализирующей частью)


Слайд 10

Евгений Корныхин 10 Модели модель инструкции модель MMU начальное состояние микропроцессора


Слайд 11

Евгений Корныхин 11 Модель инструкции ветви функциональности и дополнительные ситуации последовательность операторов типа assert, присваивания и процедур-обращений к MMU


Слайд 12

Евгений Корныхин 12 Модель MMU процедуры: трансляция адресов, загрузка из памяти через кэш построение ограничений для последовательности процедур (основная часть диссертации)


Слайд 13

Евгений Корныхин 13 . . . LOAD x, y, c @ tlbHit . . . Модели (= v (+ y c)) t1 структурная модель MMU генерация ограничений LOAD x, y, c: v ? y + c; AddrTr(v,p); . . . tlbHit(t, ts) { «(or » (t1:ts)«(= t t1)» «)» } (= t (extract[30:10] v)) (or (= t t1) (= t t2)) tlb шаблон программы модель MMU модель инструкции ограничения ограничения v = 145 y = 52 . . . значения параметров шаблона


Слайд 14

Евгений Корныхин 14 Ядро генератора шаблон инструкция1 инструкция2 инструкцияn оператор1 оператор2 операторN … … … … оператор1 оператор2 операторN1 … последовательность операторов- не процедур последовательность операторов-процедур оператор1 оператор2 операторN2 … тестовый шаблон модели инструкций ограничения модель MMU


Слайд 15

Евгений Корныхин 15 Модель инструкции процедура – шаг исполнения инструкции, являющийся неделимым обращением к MMU LOADWORD x, y, c: vAddr ? y + c; vAddr[1:0] = 0; AddrTrans(vAddr, pAddr); pAddr ? pAddr[35:3] || (pAddr[2:0] + 4); LoadMem(pAddr, memdw); x ? memdw[vAddr[2:0]:0];


Слайд 16

Евгений Корныхин 16 Модель инструкции LOADWORD x, y, c: vAddr ? y + c; vAddr[1:0] = 0; AddrTrans(vAddr, pAddr); pAddr ? pAddr[35:3] || (pAddr[2:0] + 4); LoadMem(pAddr, memdw); x ? memdw[vAddr[2:0]:0]; процедура – шаг исполнения инструкции, являющийся неделимым обращением к MMU


Слайд 17

Евгений Корныхин 17 Структурная модель MMU связный набор ассоциативных буферов и таблиц модель таблицы – множество (тег, данные) и, возможно, доп.данные обращением является запрос данных по некоторому тегу ассоциативный буфер – подмножество таблицы, состояние которого изменяется автоматически при каждом обращении


Слайд 18

Евгений Корныхин 18 Структурная модель MMU связный набор ассоциативных буферов и таблиц ассоциативный буфер таблица тег ? данные тег ? данные


Слайд 19

Евгений Корныхин 19 Успешность обращений Обращение в буфер по заданному тегу является (не)успешное, если этот тег в нем (не) присутствует «hit x» («попадание») - успешное обращение по тегу «х» «miss х» («промах») - неуспешное обращение по тегу «х» шаблон полный, если для каждой процедуры в последовательности операторов известна успешность обращений к ассоц.буферам и таблицам


Слайд 20

Евгений Корныхин 20 Ограничения для последовательности обращений буфер hit/miss x1 hit/miss x2 hit/miss xn … P1(t1,…,tm, x1) P2(t1,…,tm, x1, x2) Pn(t1,…,tm, x1, …, xn-1, xn) …


Слайд 21

Евгений Корныхин 21 Ограничения для обращений в буферы hit(xi) : xi ? Li miss(xi) : xi ? Li Li = ?(L0, x1,…, xi-1) как записать ? ? как уменьшить размер L0 ?


Слайд 22

Евгений Корныхин 22 «Совместная» эвристика: уменьшать множества констант x f(x) T L x?T f(x)?L ? x?T’ x?T?T’ f(x)?L[T’]


Слайд 23

Евгений Корныхин 23 «Зеркальная» эвристика: избавиться от множеств констант hit/miss y1 hit/miss y2 … hit/miss yk hit x «х» встречался раньше и (не) был вытеснен x?{y1,…,yk} hit/miss y1 hit/miss y2 … hit/miss yk miss x x?{y1,…,yk}


Слайд 24

Евгений Корныхин 24 Описание стратегий вытеснения в виде ограничений функция вытеснения «полезная» инструкция, функция полезности тег еще не вытеснен ? количество полезных инструкций ? константа пример (LRU): u(xi) = xi?{?p+1,…,?w} ? xi?{x1,…,xi-1} … \/?p?L0 (x=?p ? ?u(xi) ? w-p)


Слайд 25

Евгений Корныхин 25 Коммерческие аналоги (новизна) тоже основанный на моделях подход, но: не известно существование технологичного подхода к тестированию MMU трудоемкая подготовка решателя ограничений для новой архитектуры микропроцессора


Слайд 26

Евгений Корныхин 26 Апробация Z3 2,29 ГГц 800 МБ MIPS64


Слайд 27

Евгений Корныхин 27 Апробация: время генерации программ Z3 2,29 ГГц 800 МБ MIPS64


Слайд 28

Евгений Корныхин 28 Апробация: структурные модели MMU MIPS Alpha P6 PowerPC


Слайд 29

Евгений Корныхин 29 Результаты (все новые) предложена модель MMU предложены методы генерации ограничений для последовательностей обращений к MMU предложены методы генерации ограничений для описания стратегий вытеснения построены модели MMU микропроцессоров MIPS, Alpha, PowerPC, Pentium; написан прототип генератора тестовых программ для микропроцессора MIPS64


Слайд 30

Евгений Корныхин 30 Публикации Kornikhin E. Test Data Generation for Arithmetic Subsystem of CPUs MIPS64 // Proceedings of SYRCoSE'08, Volume 2, 4pp. Корныхин Е.В. Генерация тестовых данных для тестирования арифметических операций центральных процессоров // Труды ИСП РАН: том 15, 12с Корныхин Е.В. Система генерации тестовых программ с использованием ограничений ТЕСЛА // "Ломоносов-2009", 1с Корныхин Е.В. Система генерации тестовых данных для системного функционального тестирования микропроцессоров ТЕСЛА // "Микроэлектроника и информатика-2009", 1с Корныхин Е.В. Генерация тестовых данных для системного функционального тестирования FIFO-кэш-памяти микропроцессоров // журнал «Вычислительные методы и программирование», вып.10, 2009, 10с Kornikhin E. Test Data Generation for LRU Cache-Memory testing // SYRCoSE'09, 5pp. Kornikhin E. SMT-based Test Program Generation for Cache-memory Testing // East and West-2009, 3pp. Корныхин Е.В. Генерация тестовых данных для системного функционального тестирования микропроцессоров с учетом кэширования и трансляции адресов // Труды ИСП РАН, 2009 (выходит из печати) Корныхин Е.В. Генерация тестовых данных для тестирования механизмов кэширования и трансляции адресов микропроцессоров // журнал «Программирование», 36(1), 2010, 10с (выходит из печати)


Слайд 31

Евгений Корныхин 31 Выступления на конференциях Kornikhin E. Test Data Generation for Arithmetic Subsystem of CPUs MIPS64 // SYRCoSE'08 Kornikhin E. Test Data Generation for LRU Cache-Memory testing // SYRCoSE'09 Корныхин Е.В. Система генерации тестовых программ с использованием ограничений ТЕСЛА // "Ломоносов-2009" Корныхин Е.В. Система генерации тестовых данных для системного функционального тестирования микропроцессоров ТЕСЛА // "Микроэлектроника и информатика-2009" Kornikhin E. SMT-based Test Program Generation for Cache-memory Testing // East and West-2009


×

HTML:





Ссылка: