SymbiYosysで半加算器の形式検証をする話
ハードウェア設計の文脈で、形式検証を使って設計した回路の正しさを保証することができます。この記事では、SymbiYosys を使って半加算回路を形式検証してみます。この記事の成果物はここから入手できます。
SymbiYosys について
SymbiYosys ( sby とも略されます) は、オープンソースの論理合成ツールである Yosys に基づいた、形式検証のためのフロントエンドです。例えば以下のようなことができるようです。
- 安全性仕様 (safety property) の有界モデル検査 (bounded model checking) に基づく形式検証
- 安全性仕様の (有界ではない) モデル検査に基づく形式検証
- カバレッジに基づくテストベンチ生成
- 活性 (liveness) の形式検証
検証に用いられる仕様は、System Verilog Assertion (SVA) で記述されます。検証プロセスの設定は .sby ファイルに記述されます。
半加算器の検証
まずは正しく動作する半加算器を検証してみます。
回路設計 (Verilog/.v)
以下が Verilog による半加算器の設計になります。 always_comb assert ({carry, sum} == A + B); の部分では、 A と B の和が carry と sum の 2bit と等しいという、半加算器の仕様を記述しています。
module half_adder (input A, input B, output wire carry, output wire sum);
assign carry = A & B;
assign sum = A ^ B;
always_comb assert ({carry, sum} == A + B);
endmodule
検証の設定 (.sby)
以下が検証の設定を記述している .sby ファイルになります。ここでは検証対象のファイル (half_adder_with_assertion.v) や検証対象のモジュール名 (half_adder)、検証の方式などを記述しています。
[options]
mode prove
[engines]
smtbmc
[script]
read -formal half_adder_with_assertion.v
prep -top half_adder
[files]
half_adder_with_assertion.v
検証の結果
.sby ファイルを sby half_adder.sby と指定することで、Symbiyosys を用いた検証ができます。検証結果のログの以下の部分が、検証が成功した、つまり実装した半加算器が仕様を充たしていることを示しています。
SBY 13:55:35 [half_adder] summary: successful proof by k-induction.
(間違った)半加算器の検証
次に間違った半加算器を検証してみることで、正しくバグが検出できることを見ていきます。
回路設計 (Verilog/.v)
以下が間違った半加算器の設計になります。仕様の部分は以前のものと同じですが、 sum の部分で XOR ではなく OR を使っている点が誤りになります。
module half_adder (input A, input B, output wire carry, output wire sum);
assign carry = A & B;
assign sum = A | B;
always_comb assert ({carry, sum} == A + B);
endmodule
検証の結果
先程と同様に Symbiyosys で検証をすると、以下のような部分を含むログが出てきます。これは、 wrong_half_adder_with_assertion.v の4行目のassertionが失敗していて、仕様を充たしていないことを示しています。また、反例の実行結果が engine_0/trace.vcd に出力されます。他にも Verilog のテストベンチなどとしても出力されます。
SBY 13:55:35 [wrong_half_adder] engine_0.basecase: ## 0:00:00 BMC failed!
SBY 13:55:35 [wrong_half_adder] engine_0.basecase: ## 0:00:00 Assert failed in half_adder: wrong_half_adder_with_assertion.v:4.13-4.44
SBY 13:55:35 [wrong_half_adder] engine_0.basecase: ## 0:00:00 Writing trace to VCD file: engine_0/trace.vcd
SBY 13:55:35 [wrong_half_adder] engine_0.basecase: ## 0:00:00 Writing trace to Verilog testbench: engine_0/trace_tb.v
SBY 13:55:35 [wrong_half_adder] engine_0.basecase: ## 0:00:00 Writing trace to constraints file: engine_0/trace.smtc
生成された trace.vcd を GTKWave で表示してみると以下のようになります。この例では A=1 かつ B=1 なのに sum=1 となっているので、確かに仕様を違反していることがわかります。
まとめ
SymbiYosys を使うと回路設計の正しさを形式的に証明したり、バグを発見できることを、半加算器の例を通して見ていきました。今回は半加算器の検証のみを行いましたが、 SymbiYosys はより大きい回路設計でも、例えば 16bit の加算器程度の複雑さであればかなり高速に検証できるようです。今回は試していませんが、順序回路を検証する場合は、回路が内部に状態を持つので恐らく検証にかかる時間もそれなりに長くなると思いますし、そもそも仕様の記述が結構大変になりそうです。