Познакомимся с формальной верификацией — строгим математическим методом проверки соответствия вашего продукта требованиям спецификации. Если классический функциональный подход проверяет лишь отдельные сценарии, то формальная проверка алгоритмически доказывает отсутствие ошибок. Покажем, что этот метод требует иных усилий, но даёт уверенность в корректности логики, переводя поведенческое описание схемы и требования спецификации в общую формальную модель.
Разберём, как «под капотом» работают САПРы: как требования транслируются в предикатную логику и темпоральные утверждения (SystemVerilog Assertions), а затем сводятся к задачам для SAT/SMT-решателей. Своими руками проведём «формальное доказательство» на простом примере: шаг за шагом самостоятельно преобразуем схему и требования в математическое описание, запустим решатель (Z3) и интерпретируем полученные результаты. Увидим, как решатель ищет контрпример к нарушению спецификации, перебирая состояния системы.
Поняв принципы, перейдём к Open Source тулчейну SymbiYosys, который автоматизирует рутинные операции преобразования, синтеза и проверки, которые мы сделали своими руками, — тем самым проводит процесс формальной верификации под ключ. Итог — исчезновение страха перед чёрным ящиком формальных методов. Встреча будет полезна всем: новичкам она даст понимание сути формального подхода, а для профильных коллег станет первым шагом к внедрению формальных методов в маршруты разработки.
Для всех
Средний
RTL-инженер, руководитель группы разработки, работал в Syntacore, сейчас — в YADRO. Разрабатывает высокопроизводительные RISC-V процессоры; лид STEM-курса по электронике в Центральном университете.