Questa Formal

Набор приложений Questa Formal дополняет традиционное моделирование RTL кода формальным анализом поведения объекта для обнаружения возможных состояний, которые могут привести к ошибке. Такой подход позволяет выявить ошибки, которые были пропущены при моделировании, и обеспечить полностью корректную работу блоков управляющей логики.

Questa Formal может быть использовано для формальной верификации отдельных блоков проекта, как только они будут готовы и еще до их интеграции в SoC и до разработки инфраструктуры (тестбенча) для моделирования. Анализируя одно и тоже RTL описание, что и система моделирования, а также полную интеграцию с унифицированной базой данных покрытия (USDB Unified Coverage Database), Questa Formal является превосходным инструментом для поиска и исправления ошибок и, в конечном счете, для ускорения полноты функционального покрытия.

Как работает формальная верификация

Questa Formal анализирует поведение тестируемого объекта и идентифицирует все состояния, в которые объект может попасть из текущего состояния. Данный подход позволяет исследовать всю “ширину” множества состояний, в отличие от традиционного моделирования, которое анализирует “глубину” продвижения объекта из текущего состояния под действием подаваемых тестовых векторов.

Таким образом Questa Formal позволяет обнаружить все ошибки, возникающие при переключении текущего состояния во все возможные смежные состояния без использования тестовых воздействий для обнаружения этих ошибок. Это обеспечивает проверку безошибочного функционирования объекта при всех возможных сочетаниях входных воздействий. В то же время такой подход по существу позволяет обнаружить труднодостижимые при моделировании состояния, ускоряя достижение полноты покрытия.

Автоматическое решение по “нажатию кнопки”

Questa Formal это простой в использовании набор приложений следующего поколения, для верификации сложных “скрытых” ошибок. Например, приложение Questa X-Check использует формальные алгоритмы для исчерпывающего решения проблемы распространения неопределенного состояния сигнала Х для двух вариантов – оптимистического и пессимистического. Эта задача не может быть решена методом традиционного моделирования.