Понравилась презентация – покажи это...
Слайд 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
Системное тестирование (core testing)
Генерация тестов
эталонная
реализация
микропроцессора
( на Си )
cравнение трасс
Возникла ошибка
Успешный прогон
cимуляция design’а (на Verilog)
тестовые
программы
проводится «сравнением с эталоном»
Слайд 4
5
Систематическое построение тестов
Генерация тестов
ситуации
факторизация пространства ситуаций
нацеленные на класс ситуаций тесты
пример «ситуации»: «1-я инструкция даёт кэш-промах, 2-я – NOP, 3-я – безусловный переход по загруженному из памяти адресу»
Слайд 5
6
Современная практика
Генерация тестов
ситуации
нацеленных тестов надо много (ситуаций порядка 104-106)
современная практика: ситуации из 2-3 инструкций
но не все ситуации выражаются в 2-3 инструкциях
Слайд 6
7
Неэффективность существующих методов построения тестов
форма ситуации – шаблон теста
шаблон задает набор условий, в тесте эти условия должны быть выполнены
методы типа монте-карло неэффективны при построении тестов длиннее 3-4 инструкций
DIV
LOAD
x,
y,
y,
x,
z
c
@ divby0
@ l1-miss
ситуация (шаблон теста)
условия
Слайд 7
8
Систематическое построение тестовых шаблонов
выполняется на основе классификации поведения микропроцессора (модели)
цепочка инструкций
аргументы
варианты исполнения инструкций
DIV
LOAD
divby0
…
l1-miss
…
ADD
norm
…
DIV
LOAD
x,
y,
y,
x,
z
c
@ divby0
@ l1-miss
ситуация (шаблон теста)
...
instruction set specification
Слайд 8
9
Неэффективность существующих методов построения тестов
методы на основе сведения к системам уравнений (~SAT)
сведение в виде изменений состояния даёт громоздкие уравнения (104-106 переменных)
собственные решатели - это является нетривиальной задачей
DIV
LOAD
x,
y,
y,
x,
z
c
@ divby0
@ l1-miss
ситуация (шаблон теста)
условия
Слайд 9
10
Актуальность и задача
Актуальность:
необходимы методы построения эффективных тестов, нацеленных на верификацию MMU
современные доступные методы не позволяют целенаправленно строить тесты для ситуаций длиной более 3-4 инструкций, на практике требуется порядка 10 инструкций
Задача: разработать метод построения нацеленных тестов, пригодный для ситуаций из 10-12 инструкций
Слайд 10
Общее описание подхода
DIV x, y, z <деление на 0>
LOAD y, x, c <промах в кэше первого уровня>
тестовый шаблон
варианты исполнения инструкции
система уравнений
MOV x,0 MOV y,0
STORE x,x,1
STORE x,x,2 STORE x,x,3 STORE x,x,4
MOV z,0
DIV x,y,z
LOAD y,x,0
тестовая программа
Слайд 11
Детальное описание подхода
Описание вариантов исполнения инструкций, описание кэшей, таблиц страниц и т.п.
DIV x, y, z <деление на 0>
LOAD y, x, c <промах в кэше первого уровня>
var x:10, y:10, z:10;
assume: z = 0^10;
var a:10, b:10, ofs:4;
phys <- b + (10)ofs;
miss<L1>(phys){replace(a)};
hit<Mem>(phys){load(a)};
тестовый шаблон
вариант исполнения «деление на ноль»
вариант исполнения «промах в кэше первого уровня»
L1 {
policy:LRU
… }
Mem {
policy:none
… }
описания кэша и памяти
Слайд 12
Детальное описание подхода
Построение системы уравнений
var x:10, y:10, z:10, c:4;
assume: z = 0^10;
phys <- x + (10)c;
miss<L1>(phys){replace(y)};
hit<Mem>(phys){load(y)};
цепочка вариантов исполнения инструкций
система уравнений
L1 {
policy:LRU
… }
Mem {
policy:none
… }
модели кэшей, памяти
переменные x0, y0, z0, c
переменные phys,t1,t2,t3,t4
Слайд 13
Детальное описание подхода
Решение уравнений, построение текстов программ
система уравнений
x0 = 0 y0 = 0 z0 = 0
c = 0 t1 = 1 t2 = 2 t3 = 3 t4 = 4
решатель уравнений
MOV x,0 MOV y,0
STORE x,x,1
STORE x,x,2 STORE x,x,3 STORE x,x,4
MOV z,0
DIV x,y,z
LOAD y,x,0
тестовая программа
Слайд 14
это скрытый слайд
Слайд 15
16
Апробация
увеличили допустимый размер шаблонов (было 2-3, стало 8-10)
Слайд 16
17
Апробация
увеличили допустимый размер шаблонов (было 2-3, стало 8-10)
Слайд 17
18
Апробация
увеличение допустимого размера шаблонов (было 2-3, стало 8-10)
среднее время построения одного теста – 1-30с.
решатель уравнений внешний (Z3)
Слайд 18
19
Апробация
существующая среда
MicroTESK
(генерирует
шаблоны)
описания инструкций
(xml)
синт.анал.xml, генер.ур-ний (ruby)
связь с MicroTESK, конструктор текстов asm (Java)
ур-ния (smt)
тесты
(asm)
~100стр. на инструкцию
~2000стр.
~1000стр.
100-500стр.
Слайд 19
20
Где предложенные методы работают
многоуровневая кэш-память
обращение в память с / без виртуальной памяти
сквозная запись / отложенная запись
доп.условия на строки кэш-памяти
virtually indexed кэш-память
virtually tagged кэш-память
Слайд 20
21
Где эти методы НЕ работают
псевдослучайное вытеснение
псевдослучайный выбор таблиц в инструкции
временные ограничения (длительности, зависимости от скорости выполнения)
циклические действия (например, sqrt)
кэш-память инструкций
«совместная» кэш-память
но и тестирование, нацеленное на эти особенности, надо проводить иначе
Слайд 21
22
Результаты
модель состояния, описывающая характеристики блоков MMU в едином виде («таблицы»)
модель описания инструкций в виде соотношений битовых строк и обращений к «таблицам»
методы построения разрешаемых ограничений, сводящие шаблон к уравнениям над битовыми строками, без описания изменений состояния MMU
методы описания стратегий вытеснения c помощью уравнений над битовыми строками и ограничениями сумм бит
Слайд 22
23
Публикации
1. статья в «Программировании» [из списка ВАК]
2. статья в «Вычислительных методах и программировании»
3-4. статьи на SYRCoSE-2008 и 2009
5. статья на EWDTS-2009
6-7. статьи в сборниках трудов ИСП РАН (тт.15, 17)
