Метод автоматизации имитационной верификации цифровой аппаратуры на основе формальных спецификаций разного уровня абстракции Михаил Чупилко Институт системного программирования РАН

Процесс создания аппаратуры 2 of 27 RTL Net List Hardware

Примеры ошибок в вычислительных системах – ARIANE 501 Причина: Ошибка целочисленного округления Потери: 10 лет разработки, 500 млн. $ 3 of 27

Примеры ошибок в вычислительных системах – PATRIOT Причина: Накопление погрешности результата округления Потери: 28 убитых, около 100 человек раненых 4 of 27

Примеры ошибок в вычислительных системах – Pentium Bug Причина: Ошибка в таблице поиска результата деления Потери: > 400 млн $ на замену продукции 5 of 27

Особенности моделей аппаратуры Полностью описывают функциональность будущих устройств Разрабатываются на HDL языках (Verilog, VHDL) и, реже, языках системного проектирования (SystemVerilog, SystemC) Могут быть проинтерпретированы симуляторами (Icarus Verilog, ModelSIM etc), которые поддерживают программные интерфейсы для языков C/C++ (VPI, DPI и т.д.) 6 of 27

Трудности верификации Выраженный параллелизм моделей Итерационные изменения в моделях в процессе проектирования Постоянное увеличение сложности аппаратуры Время проведения верификации ограничено 7 of 27

Цель работы Разработка универсального метода верификации цифровой аппаратуры применимого для сложных систем промышленного масштаба на разных этапах проектирования 8 of 27

Поставленные задачи Провести анализ существующих методов верификации цифровой аппаратуры, использующихся на разных этапах проектирования Разработать универсальный метод верификации моделей аппаратуры на основе формальных спецификаций, поддерживающий различные уровни абстракции, композицию тестовых сложных систем из их составных частей для проведения интеграционного тестирования Провести апробацию полученного метода в промышленных проектах по разработке современной цифровой аппаратуры 9 of 27

Существующие методы Имитационная верификация Генерация тестовой последовательности на основе разрешения ограничений (Constraint-Driven Verification) Проверка корректности на основе утверждений (Assertions), эталонной модели (Co-Simulation) Оценка полноты тестирования на основе покрытия кода и комбинаций событий Формальная верификация Проверка эквивалентности (Equivalence checking) Автоматическое доказательство теорем (Theorem Proving) Проверка моделей (Model Checking) 10 of 27

Предлагаемый метод верификации Имитационная верификация Генерация тестовой последовательности с помощью обходчика конечных автоматов (в том числе извлекаемых автоматически) либо рандимизированным образом Проверка корректности на основе утверждений исполнимой формальной модели, построенной в соответствии с определенной архитектурой Оценка полноты тестирования на основе покрытия функциональности 11 of 27

Архитектура тестовой системы – общий вид 12 of 27

Архитектура тестового оракула 13 of 27

Функциональная модель Является набором параллельно выполняющихся процессов STIMULUS (тестовое воздействие) REACTION (реакция) PROCESS (не порождающий стимулы или реакции процесс) Моделирование времени происходит с помощью макроса CYCLE(), находящегося в коде процессов Моделирование передачи данных осуществляется с помощью объектов класса сообщений Message Моделирование интерфейсов аппаратуры (наборов входных или выходных сигналов) происходит с помощью объектов класса Iface 14 of 27

Пример кода: эталонная модель CPPTESK_MODEL(Counter) { public:... DECLARE_INPUT(iface1); DECLARE_OUTPUT(iface2); DECLARE_STIMULUS(inc); DECLARE_REACTION(readres);... void inc_counter(void); int get_value(void); protected: int counter; }; DEFINE_STIMULUS(Counter::inc) { InputData data = CAST_MESSAGE(InputData); START_STIMULUS(PARALLEL); OutputData odata = OutputData(get_value()); inc_counter(); CYCLE(); read_result(process, iface2, odata); STOP_STIMULUS(); } 15 of 27

Адаптер эталонной модели Является набором адаптеров интерфейсов: входных – сериализаторы выходных – десериализаторы Включает сопоставители реакций – объекты класса Arbiter, позволяющие установить порядок сообщений Включает прослушиватели неожиданных реакций на интерфейсах – встроенные в десериализаторы или являющиеся их аналогами Расширяется тестовым оракулом, компонентом, выносящим вердикт о корректности пришедших реакций реализации 16 of 27

Пример кода: адаптер модели 17 of 27 DEFINE_PROCESS (CounterMediator::serialize_iface1) { InputData msg = CAST_MESSAGE(InputData); START_PROCESS(); CAPTURE_IFACE(); inputs.inc = 1; RELEASE_IFACE(); CYCLE(); STOP_PROCESS(); } DEFINE_REACTION (CounterMediator::deserialize_iface2) { OutputData &msg = CAST_MESSAGE(OutputData); START_PROCESS(); WAIT_REACTION(true); msg.set_data(outputs.data); NEXT_REACTION(); STOP_PROCESS(); }

Преимущества использования архитектуры Моделирование множества параллельных процессов Вычислительная часть отделена от коммутационной Унифицированный интерфейс компонентов Возможность реализовывать проверки: без учета времени, с учетом порядка, потактовые Возможность автоматического отлова неожиданных реакций при наличии десериализаторов Известны точки доступа к общим выходных ресурсам (условия ожидания реакций в десериализаторах) Возможность перегрузки адаптеров интерфейсов для объединения нескольких тестовых систем 18 of 27

Извлечение функции получения текущего состояния конечного автомата из эталонной модели Используется информация обо всех WAIT_REACTION и CYCLE в эталонной модели Строится модель времени (потактовая, событийная) и модель состояний (фильтр параметров, влияющих на текущее состояние) Первым результатом является тест, охватывающий доступ к общим ресурсам – выходным интерфейсам через описание доступа к WAIT_REACTION 19 of 27

Объединение тестовых оракулов 20 of 27

Научная новизна Метод формальной спецификации цифровой аппаратуры (метод создания эталонных моделей), подходящий для использования на разных уровнях абстракции Метод сопоставления реакций цифровой аппаратуры и реакций эталонной модели, позволяющий автоматизировать процедуру проверки цифровой аппаратуры Метод извлечения абстрактной автоматной модели цифровой аппаратуры из ее эталонной модели, позволяющий автоматически генерировать тесты, проверяющие конфликты доступа к общим ресурсам 21 of 27

Практическая значимость На основе предложенного метода верификации была разработана библиотека классов C++ для создания эталонных моделей и тестовых систем на их основе Библиотека классов была применена в 7 проектах верификации модулей микропроцессоров в течение В процессе верификации в среднем обнаруживалось 3-5 серьезных ошибок в модулях, прошедших верификацию другими методами Использование средств позволило, не увеличивая времени начала получения первых тестов, иметь возможность получать автоматные тесты за короткий промежуток времени 22 of 27

23 of 27 Применение подхода на практике L2 cache (НИИСИ) Data switch (МЦСТ) Interrupt controller (МЦСТ) Memory access unit (МЦСТ) Translation lookaside unit (МЦСТ) L2 Bank Controller (МЦСТ) Instruction buffer (МЦСТ) – в процессе

Апробация и публикации SYRCoSE: Spring Young Researches Colloquium on Software Engineering, г. Нижний Новгород, 2010 г. и г. Екатеринбург, 2011 г.); EWDTS: East-West Design & Test Symposium, г. Санкт-Петербург, 2010 г. и г. Севастополь, 2011 г.; Baltic Electronics Conference, г. Таллинн, 2010 г.; Семинарах Института системного программирования РАН (г. Москва, гг.); По теме диссертации автором опубликовано 11 работ (из них 3 в изданиях по перечню ВАК). 24 of 27

Заключение - 1 Предложен метод верификации моделей аппаратуры, включающий архитектуру тестовых систем, масштабируемую на разные уровни абстракции и построенную на основе формальных спецификаций особого вида, поддерживающих композицию На основе метода была разработана программная библиотека классов на языке C++, которая была использована для верификации ряда модулей микропроцессоров, разрабатываемых в НИИСИ РАН и ЗАО «МЦСТ» 25 of 27

Заключение - 2 Разработанные тестовые системы позволили выявить ряд критических ошибок, ранее не обнаруженных при использовании других методов верификации Тестовые системы использовались для модулей, находящихся на разных уровнях абстракции, а также дорабатывающихся; трудозатраты были относительно небольшими Часто использовалась возможность первоначального создания рандомизированных тестовых последовательностей, а затем автоматных на основе практически тех же самых эталонных моделей 26 of 27

Спасибо Вопросы?