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

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

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

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

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

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

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

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

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

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

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

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

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

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

Евгений Корныхин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 Модель инструкции 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 Структурная модель MMU связный набор ассоциативных буферов и таблиц модель таблицы – множество (тег, данные) и, возможно, доп.данные обращением является запрос данных по некоторому тегу ассоциативный буфер – подмножество таблицы, состояние которого изменяется автоматически при каждом обращении

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

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

Евгений Корныхин20 Ограничения для последовательности обращений буфер hit/miss x 1 hit/miss x 2 hit/miss x n … P 1 (t 1,…,t m, x 1 ) P 2 (t 1,…,t m, x 1, x 2 ) P n (t 1,…,t m, x 1, …, x n-1, x n ) …

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

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

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

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

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

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

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

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

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

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

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