Динамическая проверка HDL-описаний на основе исполнимых моделей Александр Камкин, Михаил Чупилко Институт системного программирования РАН (ИСП РАН) Семинар «Технологии разработки и анализа программ» 20 декабря 2012, Москва, ВМиК МГУ 1

Содержание Цифровая аппаратура Динамическая проверка поведения Формализация отношения соответствия Заключение 2 of 35

Цифровая аппаратура Аппаратура проектируется на языках описания аппаратуры (HDL), например, Verilog или VHDL Результат проектирования – программа, которую можно выполнять в HDL-симуляторе Основной подход к верификации аппаратуры – тестирование HDL-описания Для автоматизации тестирования применяются исполнимые модели (C/C++) 3 of 35

HDL-описание аппаратуры input S; output R1, R2; void design() { while(true) { wait(S); delay(6); R1 = 1; delay(1); R1 = 0; R2 = 1; delay(1); R2 = 0; } 4 of 35 CLK 6 тактов S R1 R2 Параллельные присваивания

Поведение цифровой аппаратуры 5 of 35

Модели уровня транзакций (TLM) Разделение блоков обработки и передачи данных 6 of 35 Дискретные сигналы во времени Data Соединения/контакты Package Data Каналы/порты Пакет данных (сообщение) Инкапсуляция деталей передачи данных

7 Преобразование интерфейсов HDL Входной интерфейс #1 Входной интерфейс #N Data Выходной интерфейс #1 Выходной интерфейс #M Оракул Адаптер входного интерфейса Адаптер выходного интерфейса Эталонная модель input in; output out;... assert(i < MAX_SIZE); fifo[i++] = recv(in);... send(out, i == MAX_SIZE);... 7 of 35

Содержание Цифровая аппаратура Динамическая проверка поведения Формализация отношения соответствия Заключение 8 of 35

Проверка корректности поведения Множество реакций корректно Каждая реакция корректна Порядок реакций корректен Задержки между реакциями корректны 9 of 35 Временные ограничения Функциональные свойства

Потактовая проверка поведения 10 of 35 R1 Реакции HDL-модели Эталонные реакции send(R1); send(R2); delay(3) R1 R2 Сравнение R2 3 такта

Неоднозначность порядка реакций 11 of 35 S R2R1 Выполнение HDL-модели recv(in_iface, S); Выполнение эталонной модели send(out_iface, R1); send(out_iface, R2);... Ошибка: R2 R1 Обратный порядок Очередь реакций R1R2 Допустимо: R2 Очередь

Арбитраж реакций Арбитр реакций находит эталонную реакцию, соответствующую реакции HDL-модели Проверка поведения зависит не только от эталонной модели, но и от арбитража реакций Каждый выходной интерфейс имеет свою очередь реакций и свой арбитр реакций Арбитры реакций инкапсулируют все детали оракула, связанные с проверкой порядка реакций 12 of 35

Оракул на основе эталонной модели 13 of 35 HDL Оракул Компараторы реакций Эталонная модель Арбитры реакций Адаптеры входных интерфейсов Адаптеры выходных интерфейсов Стимулы Реакции HDL-модели Эталонные реакции Вердикт

Типы арбитров реакций Детерминированный арбитр на основе модели arbiter: 2 Reaction Reaction {fail} Адаптивный арбитр arbiter: 2 Reaction Reaction Reaction {fail} Двухуровневый арбитр arbiter(reactions) arbiter 2 (arbiter 1 (reactions), reaction) – Недетерминированный арбитр – Адаптивный арбитр 14 of 35

Детерминированный арбитр 15 of 35 R1 Реакции HDL-модели Эталонные реакции send(R1); send(R2);... R1R2 Арбитр реакций R1 R2 FIFO Сравнение SR Известный порядок

Адаптивный арбитр 16 of 35 R1 Реакции HDL-модели Эталонные реакции send(R1); send(R2);... R1 R2 Арбитр реакций R1 R2 Get(R1) Сравнение SR Неизвестный порядок Подсказка

Двухуровневый арбитр 17 of 35 R1 Реакции HDL-модели Эталонные реакции send(R1); send(R2);... R1 R2 Арбитр #1 R1 R2 Get(R1) Сравнение SR Частично известный порядок Арбитр #2 Подсказка Кандидаты

Содержание Цифровая аппаратура Динамическая проверка поведения Формализация отношения соответствия Заключение 18 of 35

Временная последовательность (Timed word – Alur & Dill, 1994) – алфавит событий T – временная область ( R 0 или N ) w = (a 0, t 0 )(a 1, t 1 ), … ( T) (*) i. t i < t i+1 (t i t i+1 ) – монотонность T i. t i > T – прогресс (если |w| = ) 19 of 35

Трасса Мазуркевича (Trace – Mazurkiewicz, 1977) – алфавит событий I – отношение независимости Эквивалент. : u v u получается из v путем перестановки соседних независимых событий Трасса – класс эквивалентности цепочек событий по отношению эквивалентности 20 of 35

Трасса Мазуркевича (Trace – Mazurkiewicz, 1977) : пример = { a,b,c,d } I = { (a,b), (c,d) + симметрия } [ab] = { ab, ba } [bc] = { bc } [abcd] = { abcd, bacd, abdc, badc } 21 of 35

Частично упорядоченное мультимножество (Pomset – Pratt, 1982) – алфавит событий Pomset – тройка V,, V – множество вершин V V – частичный порядок : V – функция разметки 22 of 35

Частично упорядоченное мультимножество (Pomset – Pratt, 1982): примеры 23 of 35

Временная трасса (Timed trace – Chieu & Hung, 2012) – алфавит событий, T – временная область Временная трасса – V,,, [, ] V – множество вершин V V – частичный порядок : V – функция разметки : V T – время события : V T – допустимый интервал 24 of 35

Временная трасса (Timed trace – Chieu & Hung, 2012): пример { abcd, bacd, abdc, badc } { abcd, bacd } – временные ограничения 25 of 35

Поведение реализации и спецификации Поведение реализации V I,, I, I Поведение спецификации V S,, S, S, S Допустимый временной интервал S (x) = [ S (x)- t(x), S (x)+ t(x)] Соответствие событий match(x, y) = ( I (y) = S (x) ) & ( I (y) S (x) ) 26 of 35

Отношение соответствия I ~ S t T. M { (x, y) past S (t) past I (t) | match(x, y) } M – взаимно однозначное отношение x past S (t- t) y past I (t). (x, y) M y past I (t- t) x past S (t). (x, y) M (x, y), (x, y) M. x x (y) (y) 27 of 35

Отношение соответствия: пример 28 of 35

Арбитры реакций 29 of 35

Содержание Цифровая аппаратура Динамическая проверка поведения Формализация отношения соответствия Заключение 30 of 35

Резюме: сигналы 31 of 35

Резюме: сообщения 32 of 35

Резюме: соответствие 33 of 35

Инструмент C++TESK 34 of 35 Web:

Спасибо!