МЭС 2012 Моделирование и верификация коммуникационных фабрик при проектировании систем на кристалле Александр Готманов (Intel Corp.), Михаил Кишиневский (Intel Corp.), Сатраджит Чэттерджи (Two Sigma Investments)

Коммуникационная фабрика Решает задачу взаимодействия устройств на кристалле Ядра, кэши, IP блоки, память и т.д. Разнообразие микроархитектур и топологий. Intel® Atom® processor CE4100 2

Трудности проектирования Распределенные алгоритмы –разделение ресурсов –зависания –нарушения упорядочения Модульный подход не работает Позднее обнаружение проблем –на этапе сборки системы –RTL, Si Как обнаруживать ошибки в начале проектирования? 3

Решение Построение абстрактных микроархитектурных моделей на раннем этапе проектирования Формальное доказательство корректности на модели Моделирование Верификация Результаты Исправление ошибок АрхитектураМодель 4

5 Язык моделирования xMAS Модель = синхронная сеть передачи пакетов, построенная из простых примитивов Примитивы соединяются каналами источник цель канал

6 Семантика обозначает Примитив = синхронный модуль (ср. модель Verilog с одним тактовым сигналом) Канал реализует простой протокол типа запрос-ответ канал (источник, initiator) (цель, target) Очередь размера k

7 Пример x цикл 1 x цикл 4 … цикл 5цикл 6 закрытый сток x x цикл 2 x x x цикл 3 x

Разнообразие моделей Компоненты –FSM (автоматы) –Логика упорядочения –Таблицы –Конвейеры –Переключатели пакетов –Кэши –… Топологии –Шины –Кольца –Решетки Агенты –Протокольные зависимости –IP блоки, ядра –Контроллеры памяти 8

9 Инварианты / 1 44 (очередь 1)(очередь 2) Доказательство может представлять серьезную трудность для стандартных алгоритмов верификации На практике модели содержат десятки/сотни очередей и примитивов Обозначения LTL, F = однажды, G = всегда

10 Инварианты / 2 44 (очередь 1)(очередь 2) Структурный анализ модели позволяет усилить инвариант Шаг 1: Шаг 2: Шаг 3: Всякий пакет в очереди 2 имеет значение 0 Совокупность построенных инвариантов индуктивна.

11 Инварианты / 3 Посылка запроса возможна только при наличии доступного кредита, что гарантирует место в очереди входящих запросов.

12 Инварианты / 4 num i num c num o Запишем уравнения сохранения пакетов в окрестности каждого примитива (ср. уравнения Кирхгофа для тока)

Краткий вывод Модель строится из примитивов с известными свойствами Структурный анализ для автоматической генерации и усиления инвариантов Быстрая и надежная верификация больших моделей Chatterjee S., Kishinevsky M., Automatic generation of inductive invariants from high level microarchitectural models of communication fabrics, CAV

14 Зависание Зависание определяется для отдельного канала irdy data trdy

15 Ограничения справедливости Ограничения для справедливого стока:

16 Методы решения задачи Верификация моделей –Поиск циклического пути в пространстве состояний, обладающего определенными свойствами –Плохо масштабируется; не применима к моделям xMAS с 10-ми очередей Доказательство теорем –Трудоемкая задача, требует специалиста по формальной верификации Структурный анализ –Опирается на известные свойства примитивов xMAS, хорошо масштабируется Пример Модель обмена сообщениями с упорядочением 75 примитивов (24 очереди) Верификация моделей (ABC) Ограниченное док-во, 29 тактов за 1 час. Структурный анализ Полное док-во за 4 сек.

17 Стационарные переменные Состояние модели на бесконечности задается значениями стационарных переменных.

18 Стационарные уравнения Idle(u) Block(u) Idle(v) Block(v) Full(q) Empty(q) u.trdy = (q.num < k) v.irdy = (q.num > 0) … Каждый примитив ограничивает возможные значения стационарных переменных в своей окрестности.

19 Ход доказательства Для доказательства пригоден любой SAT-солвер (алгоритм проверки выполнимости формул).

20 Обзор метода стационарные уравнения, отражающие семантику примитивов UNSAT = Зависаний нет (доказательство) SAT = Контрпример + + Для применения на практике также требуются Дополнительные инварианты, ограничивающие значения стац-х переменных (порождаются автоматически) Дополнительные переменные для описания зависимости от данных (подробности в статье)

21 Эксперименты (доказательство) МодельNPrims / NQueues Время (ABC) Время (структурный анализ) Две очереди4 / 2

22 Заключение Моделирование микроархитектуры путем композиции примитивов Методы структурного анализа для быстрой верификации Автоматизированное доказательство отсутствия зависаний для моделей с 100-ми очередей