Диагностика ошибочного поведения аппаратуры при динамической верификации на основе моделей Докладчик: Проценко Александр

Процесс создания аппаратуры Документация HDL-описание аппаратуры Микросхема Разработка 2 Используются языки описания аппаратуры (Hardware Description Language): Verilog; VHDL; …

Ошибки имеют большую цену Цена ошибки в микропроцессоре очень высока, поскольку исправление ошибки в уже изготовленной микросхеме невозможно. Ошибка TLB в процессорах AMD Phenom x4 Ошибка Pentium FDIV (ошибка в модуле операций с плавающей запятой) 3

Верификация аппаратуры Документация HDL-описание аппаратуры Микросхема Верификация HDL- симулятор Тестовая система Системный симулятор Системный симулятор Разработка 4

Архитектура тестовой системы (C++TESK) 5

6 Фрагмент трассы тестовой системы

Фрагмент диаграммы сигналов 7

Сложность диагностики Сложные причинно-следственные связи между стимулами и реакциями Большие объемы данных в трассах Высокий уровень параллелизма аппаратуры 8

Постановка задачи Цель: Требуется разработать компонент C++TESK для автоматизации анализа результатов, получаемых при динамической верификации на основе моделей, с целью упрощения поиска ошибок. Задачи: Согласовать интерфейсы с сопоставителем реакций Разработать метод и средства анализа реакций полученных при верификации Испытать полученный компонент на реальных примерах 9

Диагностика в тестовой системе (C++TESK) 10

Входные данные 11 Входные данные подсистемы диагностики: Реакции реализации: Реакции эталонной модели:

Типы пар реакций NORMAL эталонная и реализационная реакции совпали MISSING отсутствует реализационная реакция UNEXPECTED отсутствует эталонная реакция INCORRECT данные эталонной и реализационной реакций имеют расхождения 12

Тип NORMAL 13

Тип MISSING 14

Тип UNEXPECTED 15

Тип INCORRECT 16

Механизм диагностирования. Базовые правила 1. (null, null) Ø 2. (a impl, a spec ) (null, null) 3. {(a impl, b spec ), (b impl, a spec )} {(a impl, a spec ), (b impl, b spec )} 4. {(a impl, null), (null, a spec )} (a impl, a spec ) 5. {(a impl, b spec ), (b impl, null)} {(a impl, null), (b impl, b spec )} 6. {(a impl, b spec ), (null, a spec )} {(a impl, a spec ), (null, b spec )} 7. {(a impl, c spec ), (b impl, a spec )} {(a impl, a spec ), (b impl, c spec )} 17 Набор правил «схлопывания». Базовые правила:

Метрики близости Количество полностью совпавших полей Расстояние Хэмминга 18

Механизм диагностирования. Нечеткие правила Набор правил «схлопывания». Нечеткие правила (с использованием метрик): 9. {(a impl, b spec ), (b` impl, a` spec )} {(a impl, a` spec ), (b` impl, b spec )} 10. {(a impl, null), (null, a` spec )} (a impl, a` spec ) 11. {(a impl, b` spec ), (b impl, null)} {(a impl, null), (b impl, b` spec )} 12. {(a impl, b spec ), (null, a` spec )} {(a impl, a` spec ), (null, b spec )} 13. (a impl, a` spec ) (null, null) 19

Вывод диагностики в командной строке 20

Анализ результатов верификации 21

Испытания Испытана на отдельных модулях микропроцессора Эльбрус 22

Спасибо! 23

24