'

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

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





Слайд 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

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


Слайд 6

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


Слайд 7

8 Неэффективность существующих методов построения тестов форма ситуации – шаблон теста шаблон задает набор условий, в тесте эти условия должны быть выполнены рандомизированные методы построения тестов неэффективны для шаблонов длиннее 3 инструкций условия 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 тестовая программа


Слайд 8

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


Слайд 9

10 Неэффективность существующих методов построения тестов методы на основе сведения к системам уравнений (~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 тестовая программа


Слайд 10

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


Слайд 11

Общее описание подхода 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


Слайд 12

Общее описание подхода DIV x, y, z <деление на 0> LOAD y, x, c <промах в L1> шаблон теста варианты исполнения инструкции система уравнений/неравенств тестовая программа 13 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}


Слайд 13

Детальное описание подхода Описание вариантов исполнения инструкций, описание блоков 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 и памяти 14


Слайд 14

Детальное описание подхода Построение системы уравнений 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 15 методы построения уравнений для hit/miss


Слайд 15

Детальное описание подхода Решение уравнений, построение текстов программ система уравнений 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 тестовая программа 16


Слайд 16

Разработаны модели «модель состояния» «модель инструкции» 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]; 17


Слайд 17

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


Слайд 18

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


Слайд 19

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


Слайд 20

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


Слайд 21

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


Слайд 22

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


Слайд 23

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


Слайд 24

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


Слайд 25

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


Слайд 26

Примеры описаний инструкций <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


Слайд 27

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


Слайд 28

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


×

HTML:





Ссылка: