Буренков Владимир Сергеевич

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

Рассматривается применимость метода model checking и инструмента Spin, в котором реализованы алгоритмы model checking, к верификации протоколов когерентности памяти. Предлагается инструмент верификации протокола когерентности памяти. Определяется ограничение на количество процессорных узлов системы, которая может быть проверена с помощью Spin.

 Улучшение результатов верификации аппаратных и программных систем связывается с применением формальных методов, среди которых авторы выделяют метод model checking, обеспечивающий автоматизированное рассмотрение всех возможных «траекторий функционирования» системы. Анализируется проблема «взрыва числа состояний», свойственная верификации методом model checking, и рассматриваются различные методы борьбы с этой проблемой. Особое внимание уделяется верификации протоколов когерентности памяти и излагаются возможные подходы к решению данной задачи.

В статье рассматриваются причины возникновения метастабильности при взаимодействии устройств, управляемых несвязанными друг с другом синхросигналами. Обсуждаются различные варианты решения проблемы метастабильности и предлагается использование одного из вариантов FIFO-буфера для обеспечения корректной работы цифровых устройств.