Semiformal verification for pipelined digital designs based on Algorithmic State Machines

Статья описывает методы и средства использования Алгоритмических машин состояний (ASM) для высокоуровневой спецификации проектов сложных цифровых систем и их верификации методом Проверки моделей (Model Checking). Данный подход использует иерархическое описание проектов на алгоритмическом уровне абстракции и возможность построения конечно-автоматных моделей по ASM-диаграммам алгоритмов. Для автоматической генерации программ Проверки моделей на языке SMV (Symbolic Modes Verifier) по ASM-диаграмме проектируемого устройства была разработана специальная программа. Способ применения данного подхода и программы демонстрируется на примере верификации проекта конвейерного микропроцессора.