先日、Cadence SMVによるモデル検査を扱う機会があった。アルゴリズムの検証で有用だと感じたので 復習がてら簡単に使ってみたい。 検査 今回は、並行コンピューティング技法で紹介されているスピンロックのバグの実装例をモデル検査で検証する。 その検査対…