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

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

23 Евгений Корныхин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 Евгений Корныхин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 Евгений Корныхин25 Коммерческие аналоги (новизна) тоже основанный на моделях подход, но: не известно существование технологичного подхода к тестированию MMU трудоемкая подготовка решателя ограничений для новой архитектуры микропроцессора

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

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

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

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

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