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

Применительно к сегодняшним крупномасштабным проектам сложных аппаратных средств весьма актуальной проблемой становится сокращение времени выполнения вычислений и требуемого объема памяти при проведении формального доказательства правильности их функционирования. Проектируемые устройства обычно представляются описаниями на уровне межрегистровых передач, тогда как большинство инструментальных средств верификации аппаратных решений основывается на использовании спецификаций разрядного уровня. Однако проектируемые устройства (например, АЛУ и шинные интерфейсы) часто имеют регулярную структуру, которая может быть легко описана на языке более высокого уровня абстракции. На разрядном (битовом) уровне эта полезная информация теряется, вследствие чего ее невозможно использовать в процедурах верификации, ориентированных на разрядные представления. Поэтому в последнее время было предложено несколько новых методов формальной верификации логических схем (ЛС); эти методы основаны на использовании информации о регулярных структурах и работают с описаниями многобитового уровня, поскольку они доступны на уровне межрегистровых передач. В статье вводятся основные понятия формальной верификации на уровне межрегистровых передач (МРП) и дается краткий обзор существующих методов ее реализации. Рассматриваются в общих чертах последние достижения в этой области, и на реальных примерах показываются преимущества использования информации многобитового уровня для проверки функциональных свойств ЛС и контроля их соответствия спецификациям.