Автоматическое построение тестов для аппаратного обеспечения с использованием разрешения ограничений проф. А.Петренко, Е.Корныхин

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

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 отдельного модуля через входные и выходные сигналы

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

5 Генерация тестов на основе моделей моделишаблоны тестовтесты структурные: модели внутреннего состояния микропроцессора (кэши, таблицы страниц) функциональные: модели инструкций (варианты исполнения) 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 DIV x, y, divbyzero LOAD y, x, l1hit

6 Этап 1: модели шаблоны 1)цепочка инструкций 2)зависимости 3)варианты исполнения инструкций DIV LOAD divbyzero … l 1-miss … модель ADD norm … DIV LOAD x,y, x, z l 1-miss тестовый шаблон

7 Этап 2: шаблоны тесты шаблон уравнения тест «ограничение» – «уравнение» «разрешение» ограничений – в смысле не «allow», а «satisfy» уравнения решает внешний инструмент ( Z3 )

8 Пример --- сделать сложнее? ADD x, y, norm CMP x, equal ADD norm (a,b,c) : a = b+c CMP equal (a,b) : a = b 0x 0,x 1,y 0,z 0

9 Применения MIPS-совместимый микропроцессор ( какие конвейеры, какие кэши?) целочисленная арифметика механизмы памяти

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

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

12 Эксперименты кол-во инструкций размеры моделей кол-во тестов кол-во шаблонов кол-во обнаружен ных ошибок