近年、EDAツールの分野でもオープンソース化が進み、フォーマル検証にも無償で利用できる環境が登場しています。
本講演ではSymbiYosysを使った論理回路レベルのフォーマル検証に挑戦し、その有効性や限界を実例と共に紹介します。 さらにCPU設計への応用としてriscv-formalとRVFIを用いたISA準拠性検証の事例も取り上げ、オープンソースでどこまで可能かを探ります。
