形式検証

ハードウェア設計の文脈で、形式検証を使って設計した回路の正しさを保証することができます。この記事では、SymbiYosys を使って半加算回路

夏なので自動かき氷機の「正しさ」を数学的に検証する話を書きます。 (この記事は以下のツイートから始まるスレッドの内容をまとめ直したものです。)