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

А.К.Петренко

@ (posedge sm_cl) begin    if (reset == 1'b1) c <= 2'b00;    else c <= next_state; end
...

проектные документы

design на Verilog

микропроцессор

тестирование design’а

s1,0x27
ori s1,s1,0xc8
lui s3,0x4e
ori s3,s3,0xf7 ...

проводится «сравнением с эталоном»

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

задача – построение теста для данной ситуации

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

конвейерных микропроцессорах

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

системам уравнений (RAVEN, Genesys-Pro)

уравнения

4. составить текст тестовой программы

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 <- x + (64)c; assume: phys[1:0]=0^2
miss(phys) {replace(y)};
hit(phys)
{load(y)};

<деление на 0>
LOAD y, x, c <промах в L1>

ситуация в виде
шаблона программы

DIV – деление на 0 (x,y,z) {
…
}

LOAD – промах в L1 (y,x,c) {
…
... L1 ...
}

1. формализация поведения

2. формализация состояния

кэш L1 {
…
}

блоке1

. . .

. . .

phys = x + (64)c

phys[1:0] = 0^2

. . .

условия на значения регистров, адресов, других промежуточных значений

…, pi; pi+1) = ( pi+1 ∈{p1,…,pi} Λ ¬Ev(p1, …, pi; pi+1) )

Miss(p1, …, pi; pi+1) = ( pi+1 ∈{p1,…,pi} Λ Ev(p1, …, pi; pi+1) )

Load(qi, di) = ( if qi = qi-1 then di=di-1 elsif qi = qi-2 then di=di-2 else … endif )

phys[1:0] = 0^2 …

это новые методы

для шаблона совместна, то ее решение «удовлетворяет» шаблону

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

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

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

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

 
но и тестирование, нацеленное на эти особенности, надо проводить иначе

1-30с.
решатель уравнений внешний (Z3)

microTLB 4 строки
обнаружено несколько новых критичных ошибок
?????

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

и программировании»
3-4. статьи на SYRCoSE-2008 и 2009
5. статья на EWDTS-2009
6-7. статьи в сборниках трудов ИСП РАН (тт.15, 17)

status="readonly" />                     rs            
rs    
 
    
            rt
            
rt
    
 
    
                
rs
                    
rs
                
                
                     rt
                     
rt 
                

    
            temp

            temp

    

арифметическое переполнение
ADD rd, rs, rt

(n + 2w)

для LRU: m ≤ n · w + M

n – количество промахов/попаданий (~ длина шаблона)
M – количество промахов
w – ассоциативность блока

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