'

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

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





Слайд 0

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


Слайд 1

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


Слайд 2

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


Слайд 3

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


Слайд 4

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


Слайд 5

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


Слайд 6

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


Слайд 7

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


Слайд 8

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


Слайд 9

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


Слайд 10

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


Слайд 11

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


Слайд 12

Евгений Корныхин 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 . . . значения параметров шаблона


Слайд 13

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


Слайд 14

Евгений Корныхин 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];


Слайд 15

Евгений Корныхин 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


Слайд 16

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


Слайд 17

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


Слайд 18

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


Слайд 19

Евгений Корныхин 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) …


Слайд 20

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


Слайд 21

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


Слайд 22

Евгений Корныхин 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}


Слайд 23

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


Слайд 24

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


Слайд 25

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


Слайд 26

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


Слайд 27

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


Слайд 28

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


Слайд 29

Евгений Корныхин 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с (выходит из печати)


Слайд 30

Евгений Корныхин 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:





Ссылка: