YADRO исследует open source альтернативы для формальной верификации аппаратного дизайна

Обычное тестирование аппаратного дизайна часто не гарантирует отсутствия ошибок, а лишь сигнализирует, что их не нашли. На этом фоне формальная верификация, метод, проверяющий все состояния системы, становится критически важным для обеспечения надежности. Однако ведущие промышленные решения — VC Formal от Synopsys, JasperGold от Cadence и коммерческая часть Yosys — остаются проприетарными, проверенными, но финансово недоступными для многих команд и проектов.

Борис Новосёлов, младший инженер по верификации в компании YADRO, провел анализ открытых альтернатив, чтобы найти инструменты «для бедных». В его исследовании фигурируют такие проекты с открытым исходным кодом, как CIRCT, Slang и Synlig. Цель — понять их архитектуру, принципы работы и оценить применимость в реальных проектах по разработке аппаратного обеспечения, где бюджет часто ограничен.

Этот поиск альтернатив подчеркивает растущее давление на индустрию: необходимость в надежных методах верификации сталкивается с высокой стоимостью проприетарных инструментов. Успех или провал open source решений в этой нише может повлиять на доступность высококачественной верификации для стартапов, академических проектов и небольших инженерных команд, потенциально меняя ландшафт инструментов для разработки аппаратного обеспечения.