17 января: Моделирование и формальная верификация микроархитектуры

Александр Готманов

Александр Готманов

Александр Готманов – научный сотрудник Московского отделения лаборатории САПР (Strategic CAD Labs, Intel Corporation (Москва). В 2005 году закончил факультет ВМК МГУ имени М.В. Ломоносова. Область деятельности - моделирование, анализ и оптимизация микроархитектуры СБИС (в частности, формальная верификация транспортной логики, т.н. коммуникационных фабрик, сетей и систем на кристалле).

В докладе речь пойдет о задаче моделирования микроархитектуры коммуникационных фабрик (транспортной логики, уровня передачи пакетов) в современных системах на кристалле (СнК). Будет рассмотрена среда моделирования и верификации xMAS, разработанная в лаборатории SCL. Используя язык xMAS, можно быстро создавать компактные, графические модели (диаграммы) микроархитектурных блоков и проводить формальную проверку их правильности. Методы верификации моделей xMAS ориентированы на конкретные типы свойств (разные виды свойств safety, свойство отсутствия зависаний). Процесс верификации автоматизирован и, как правило, не требует вмешательства со стороны пользователя. Среда xMAS применялась для анализа микроархитектуры промышленных СнК на ранних этапах проектирования (до появления первой версии спецификации).

Добавить комментарий

Ваш e-mail не будет опубликован. Обязательные поля помечены *

*

Можно использовать следующие HTML-теги и атрибуты: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <strike> <strong>