'

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

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





Слайд 0

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


Слайд 1

2 Место задачи в разработке аппаратного обеспечения ... output sm_out; reg [1:0] c, next_state; always @ (posedge sm_cl) begin    if (reset == 1'b1) c <= 2'b00;    else c <= next_state; end ... проектные документы design на Verilog микропроцессор тестирование design’а


Слайд 2

3 Тестирование design’а lui s1, 0x2779 ori s1, s1, 0xc8b9 lui s3, 0x4ee ori s3, s3, 0xf798 add v0, a0, a2 sub t1, t3, t5 add t7, s1, s3 Системное тестирование Модульное тестирование Тестируется design всего микропроцессора с помощью тестовых программ Тестируется design отдельного модуля через входные и выходные сигналы


Слайд 3

4 Системное тестирование Генерация тестов эмулятор микропроцессора (эталон) ( на Си ) cравнение трасс Возникла ошибка Успешный прогон cимуляция design’а (на Verilog) тестовые программы проводится «сравнением с эталоном»


Слайд 4

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


Слайд 5

Подсистемы управления памяти (MMU) 6


Слайд 6

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


Слайд 7

8 Современная практика Генерация тестов ситуации нацеленных тестов надо много (ситуаций порядка 104-106) современная практика: ситуации из 2-3 инструкций но не все ситуации выражаются в 2-3 инструкциях


Слайд 8

9 Шаблоны тестов форма ситуации – шаблон теста шаблон задает набор условий, в тесте эти условия должны быть выполнены условия DIV x, y, z <деление на 0> LOAD y, x, c <промах в L1> ситуация (шаблон теста) MOV x,0 MOV y,0 STORE y,x,3 STORE y,x,9 STORE y,x,7 STORE y,x,5 MOV z,0 DIV x,y,z LOAD y,x,1 тестовая программа


Слайд 9

Существующие методы построения тестов прямое конструирование программ для ситуаций (MicroTESK) псевдослучайное дополнение шаблона до программы (SEGUE) методы сведения к системам уравнений прямая запись изменений состояния MMU последовательное решение ограничений с возвратами (Genesys-Pro, RAVEN) 10


Слайд 10

11 Систематическое построение тестовых шаблонов выполняется на основе классификации поведения микропроцессора (модели) цепочка инструкций аргументы варианты исполнения инструкций DIV LOAD divby0 … l1-miss … ADD norm … DIV LOAD x, y, y, x, z c @ divby0 @ l1-miss ситуация (шаблон теста) ... instruction set specification


Слайд 11

12 Неэффективность существующих методов построения тестов методы на основе сведения к системам уравнений (~SAT) напрямую запись изменения состояния даёт громоздкие уравнения (104-106 переменных) условия DIV x, y, z <деление на 0> LOAD y, x, c <промах в L1> ситуация (шаблон теста) MOV x,0 MOV y,0 STORE y,x,3 STORE y,x,9 STORE y,x,7 STORE y,x,5 MOV z,0 DIV x,y,z LOAD y,x,1 тестовая программа


Слайд 12

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


Слайд 13

Компоненты генерации шаблон варианты исполнения инструкций описания блоков MMU генератор уравнений решатель уравнений конструктор текстов тестовых программ


Слайд 14

«Структура терминов» Шаблоны (описывают, задают) ... Варианты исполнения инструкций (описывают, задают набор свойств....) Описания блоков MMU ...


Слайд 15

Общее описание подхода шаблон варианты блоки MMU assume hit/miss load/store система


Слайд 16

Общее описание подхода DIV x, y, z <деление на 0> LOAD y, x, c <промах в L1> шаблон теста варианты исполнения инструкции MOV x,0 MOV y,0 STORE y,x,3 STORE y,x,9 STORE y,x,7 STORE y,x,5 MOV z,0 DIV x,y,z LOAD y,x,1 тестовая программа 17


Слайд 17

Общее описание подхода DIV x, y, z <деление на 0> LOAD y, x, c <промах в L1> шаблон теста варианты исполнения инструкции система уравнений/неравенств тестовая программа 18 MOV x,0 MOV y,0 STORE y,x,3 STORE y,x,9 STORE y,x,7 STORE y,x,5 MOV z,0 DIV x,y,z LOAD y,x,1 z0 = 0 0 ? x0, y0 < 264 0 ? c < 216 0 ? x0+c, l1, l2, l3, l4 < 232 {l1,l2,l3,l4} попарно неравны (x0+c)?{l1, l2, l3, l4}


Слайд 18

Детальное описание подхода Описание вариантов исполнения инструкций, описание блоков MMU DIV x, y, z <деление на 0> LOAD y, x, c <промах в L1> [var x:64, y:64, z:64;] assume: z = 0^64; [var y:64, x:64; const c:16;] phys <- x + (64)c; miss<L1>(phys){replace(y)}; hit<Mem>(phys){load(y)}; шаблон теста вариант исполнения «деление на 0» вариант исполнения «промах в L1» L1 { policy=LRU lines=4 regbits=7 line(tag:24,key; d:32,data ) keyMatch(k:24) {k=tag} } Mem { policy=none … } описания кэша L1 и памяти 19


Слайд 19

Детальное описание подхода Построение системы уравнений var x:64,y:64,z:64; const c:16; assume: z = 0^64; phys <- x + (64)c; miss<L1>(phys){replace(y)}; hit<Mem>(phys){load(y)}; цепочка вариантов исполнения инструкций система уравнений переменные x, y, z, c phys,l1,l2,l3,l4 20 методы построения уравнений для hit/miss


Слайд 20

Детальное описание подхода Решение уравнений, построение текстов программ система уравнений x = 0 y = 0 z = 0 c = 1 l1 = 3 l2 = 9 l3 = 7 l4 = 5 решатель уравнений MOV x,0 MOV y,0 STORE y,x,3 STORE y,x,9 STORE y,x,7 STORE y,x,5 MOV z,0 DIV x,y,z LOAD y,x,1 тестовая программа 21


Слайд 21

Разработаны модели «модель состояния» «модель инструкции» L1 { policy=LRU; lines=4; regbits=7; key(tag:24); data(d:32); keyMatch(k:24) { k = tag }; } [ var y:64, x:64; const c:4;] vAddr <- x + (64)c; assume: vAddr[1..0] = 0^2; assume: vAddr[58..36] = 0^23; pAddr <- vAddr[35..0]; cca <- vAddr[63..61]; assume: cca != 2; pAddr2 <- pAddr[35..3] || (pAddr[2] + 1) || pAddr[1..0]; tag <- pAddr2[35..12]; region <- pAddr2[11..5]; phys <- pAddr2[35..3]; miss<L1>(tag, region){replace(y)}; hit<Mem>(phys){load(memdw)}; byte <- vAddr[2..0]; assume: byte=0 and y=memdw[31..0] or byte=4 and y=memdw[63..32]; 22


Слайд 22

Разработаны методы метод построения разрешаемых уравнений два метода описания стратегий вытеснения miss<L1>(phys){…} – «с момента последнего обращения к phys он вытеснен» дает определение «phys вытеснен» в виде « сумма характеристик инструкций ? C » доказаны теоремы корректности и полноты методов 23 дает определение «phys вытеснен» в виде свойства «исчерпания» для цепочек предыдущих инструкций


Слайд 23

24 Апробация увеличили допустимый размер шаблонов (было 2-3, стало 8-10)


Слайд 24

25 Апробация увеличили допустимый размер шаблонов (было 2-3, стало 8-10)


Слайд 25

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


Слайд 26

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


Слайд 27

Практическое использование микропроцессор архитектуры MIPS кэши такие-то, TLB такие-то обнаружено несколько новых критичных ошибок 28


Слайд 28

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


Слайд 29

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


Слайд 30

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


Слайд 31

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


Слайд 32

Примеры описаний инструкций <situation>     <argument name="rd" length="64" status="readonly" />     <argument name="rs" length="64" status="readonly" />     <argument name="rt" length="64" status="readonly" />     <assume><eq>             <bits end="63" start="32"><var>rs</var></bits>             <power index="32"><bit index="31"> <var>rs</var></bit></power>     </eq></assume>       <assume><eq>             <bits end="63" start="32"><var>rt</var></bits>             <power index="32"><bit index="31"> <var>rt</var></bit></power>     </eq></assume>       <let name="temp"><sum>                 <concat> <bit index="31"><var>rs</var></bit>                     <bits end="31" start="0"> <var>rs</var></bits>                 </concat>                 <concat>                      <bit index="31"><var>rt</var></bit>                      <bits end="31" start="0"> <var>rt</var></bits>                  </concat></sum></let>     <assume><neq>             <bit index="32"><var>temp </var></bit>             <bit index="31"><var>temp </var></bit>     </neq></assume> </situation> арифметическое переполнение ADD rd, rs, rt


Слайд 33

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


Слайд 34

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


×

HTML:





Ссылка: