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

2 Место задачи в разработке аппаратного обеспечения... output sm_out; reg [1:0] c, next_state; (posedge sm_cl) begin if (reset == 1'b1) c

3 Системное тестирование генерация тестовых программ эмулятор микропроцессора (эталон) ( на Си ) cравнение трасс Возникла ошибка Успешный прогон cимуляция designа (на Verilog) lui s1,0x27 ori s1,s1,0xc8 lui s3,0x4e ori s3,s3,0xf7... проводится «сравнением с эталоном»

Подсистемы управления памяти (MMU) 4 Memory instr i+2 instr i+1 instr i Pipeline

Задача построения нацеленных тестов факторизация пространства ситуаций нацеленные на ситуации тесты пример ситуации: в 1-й инструкции происходит «деление на ноль», во 2-й – происходит кэш-промах задача – построение теста для данной ситуации

Ситуации в MMU для отдельных инструкций: возникновение исключительных ситуаций промахи/попадания в кэшах разных уровней, в TLB кэшируемые/некэшируемые обращения в память отображаемые/неотображаемые вирт.адреса для цепочек инструкций: зависимости по регистрам (read/write) зависимости по адресам (одинаковые/разные физич./вирт. адреса) зависимости по содержимому (считывается то, что было записано ранее) одинаковые/разные страницы вирт.памяти одинаковые/разные строки кэш-памяти запись/чтение совместно с исключит.ситуациями «длинные» цепочки инструкций (~10 инстр-й) 6

7 Актуальность и задача Актуальность: необходимы методы построения тестов, нацеленных на верификацию MMU в конвейерных микропроцессорах Задача: разработать метод построения нацеленных тестов, пригодный для ситуаций из «длинных» цепочек инструкций на MMU

Существующие методы построения нацеленных тестов 1. прямое конструирование программ (MicroTESK) 2. псевдослучайное дополнение (SEGUE) 3. сведение к системам уравнений (RAVEN, Genesys-Pro)

Схема предлагаемого подхода ситуация S (шаблон программы) модель инструкции 1 в ситуации S... модель блока 1 MMU формализовать микропроцессор система уравнений начальные значения регистров инициализ-я блока 1... подпрограмма подготовки микропроцессора тестовая программа 2. построить уравнения 3. решить уравнения 4. составить текст тестовой программы

Модель блока MMU пример: какие блоки MMU нужны для ситуации (кэш, таблица страниц, TLB) блок моделируется ассоциативным массивом модель блока – значения заданных характеристик: структурные характеристики поведение строк блока L1 { policy=LRU; lines=4; regbits=7; key(tag:24); data(d:32); keyMatch(k:30) { k[29:6] = tag }; }

Модель инструкции пример: (это «вариант» исполнения инстр-и в ситуации)????? утверждения истинности условий на битовых строках источники условий: допустимые входные значения как вычислить адреса какие попадания /промахи происходят в блоках что загружается / сохраняется в блоках условия возникновения исключит. ситуаций LOAD (y,x,c) : «промах в L1» [var y:64; var x:64; const c:16;] phys

Связь моделей инструкций, моделей блоков MMU и шаблонов DIV x, y, z LOAD y, x, c ситуация в виде шаблона программы DIV – деление на 0 (x,y,z) { … } LOAD – промах в L1 (y,x,c) { …... L1... } 1. формализация поведения 2. формализация состояния кэш L1 { … }

Декомпозиция ситуации ситуация hit(miss) p i hit(miss) p i+1... цепочка промахов/ попаданий в блок 1 load(store) q i,d i load(store) q i+1,d i+1... цепочка загрузки/ сохранения данных в блоке 1... phys = x + (64)c phys[1:0] = 0^2... условия на значения регистров, адресов, других промежуточных значений

Построение уравнений hit(miss) p i load(store) q i,d i phys[1:0] = 0^2 система уравнений (битовая и целочисленная арифметика) Hit(p 1, …, p i ; p i+1 ) = ( p i+1 {p 1,…,p i } ΛEv(p 1, …, p i ; p i+1 ) ) Miss(p 1, …, p i ; p i+1 ) = ( p i+1 {p 1,…,p i } Λ Ev(p 1, …, p i ; p i+1 ) ) Load(q i, d i ) = ( if q i = q i-1 then d i =d i-1 elsif q i = q i-2 then d i =d i-2 else … endif ) phys[1:0] = 0^2 … это новые методы

Теоремы корректности и полноты методов построения уравнений доказана корректность: если система уравнений для шаблона совместна, то ее решение «удовлетворяет» шаблону доказана полнота: если для шаблона существует тест, то среди решений системы уравнений есть этот тест (если система уравнений несовместна, то шаблону не соответствует ни один тест)

Особенности предлагаемых методов единая система уравнений компактность уравнений (в них выражается не изменение состояния, а зависимости адресов) блоки инициализируются цепочкой обращений в них по адресам – адреса вычисляет решатель уравнений hit и miss в качестве выразительных возможностей языка описания инструкций

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

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

19 Реализация существующий генератор шаблонов описания инструкций (xml) конструктор текстов asm (Java) тесты (asm) ~100стр. на вариант исполнения инструкции ~2000стр. ~1000стр. уравнения (smt) стр. генератор уравнений (ruby) описания блоков MMU (xml) ~10стр. на блок шаблон теста решение равнений

20 Эксперименты увеличение допустимого размера шаблонов (было 2-3, стало 9-12) среднее время построения одного теста – 1-30с. решатель уравнений внешний (Z3)

Практическое использование микропроцессор архитектуры MIPS кэши 16кБ (L1), 256кБ (L2), TLB 48 строк, microTLB 4 строки обнаружено несколько новых критичных ошибок ????? 21

22 Результаты ????? 1. модель состояния, описывающая характеристики блоков MMU 2. модель инструкции в виде соотношений битовых строк и свойств наличия или отсутствия данных в блоках 3. метод построения разрешаемых уравнений для шаблонов в виде уравнений над битовыми строками без описания изменения состояния MMU 4. методы описания стратегий вытеснения c помощью уравнений над битовыми строками и ограничениями сумм бит

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

Примеры описаний инструкций rs rt rt rs rs rt rt temp temp арифметическое переполнение ADD rd, rs, rt

Уравнения (constraints)

Теоремы о количестве адресов, инициализирующих блок общий случай: m n · (n + 2w) для LRU: m n · w + M n – количество промахов/попаданий (~ длина шаблона) M – количество промахов w – ассоциативность блока

Метод построения уравнений для стратегий вытеснения Ev(x 1,…,x i ;x) = ( u x (x 1 ) + … + u x (x i ) > C ) C – константа (значение зависит от стратегии вытеснения) u x (x k ) = 1, если x k «способствует вытеснению» x; 0, иначе для LRU: u x (x k ) = ( x{x k,…,x i } Λ x k{x k+1,…,x i } )