オープンソース形式検証ツールSymbiYosysを用いて形式検証に入門する (1. SymbiYosysのインストールと基本的な動作確認)

オープンソース・ツールを用いた形式検証を行いたくて、いろいろチュートリアルを読んでいる。

例えば、以下の記事で書いてあるようなBRAMの形式検証を行ってみたい。

zipcpu.com

デザインとしては以下をそのまま利用してみる：

github.com

• デザインの本体：

    always @(posedge w_clk) begin
        if(w_en)
            bram[w_addr] <= w_data;
    end

    always @(posedge r_clk) begin
        if(r_en)
            r_data <= bram[r_addr];
    end

• Formalのassertionの部分

assume()によって、探索の範囲を小さくする：

symbiyosys.readthedocs.io

    // set data variable to whats in the bram
    initial begin
        assume(f_data == bram[f_addr]);
    end

assert()の書き方：読み込みリクエストが発生し、アドレスがf_addrと一致している場合、f_dataが返されなければならないというアサーションを作成する。

    always @(posedge r_clk) 
        if ((f_past_valid)
            // if a read  
            &&($past(r_en))
            // and at the special address
            &&($past(r_addr == f_addr)))
        // assert the read gives correct answer
        assert(r_data == $past(f_data));

さらに、書き込みが発生し、アドレスがf_addrと一致している場合、f_dataがそれに応じて更新されるという仮定を作成する。

    always @(posedge w_clk)
            // if a write  
            if((w_en)
            // and at the special address
            &&(w_addr == f_addr))
        // update the data
        f_data <= w_data;

検証環境を作成する

SymbiYosysをインストールするのは、oss-cad-env環境をそのままインストールする：

github.com

SymbiYosysの環境のためのスクリプトを用意する。この辺のスクリプトの意味は正直まだわかっていない。

• bram_bmc.sby

[options]
mode bmc
depth 40

[engines]
smtbmc z3

[script]
read -sv -formal bram.v
prep -top bram

[files]
bram.v

• `bram_cov.sby

[options]
mode cover
depth 100

[engines]
smtbmc z3

[script]
read -sv -formal bram.v
prep -top bram

[files]
bram.v

• Makefile

all:
        sby -f bram_bmc.sby
        sby -f bram_cov.sby

検証の実行

makeを実行すると、動作することが確認できた。とりあえずまずは第一歩だな。

SBY  0:24:27 [bram_bmc] engine_0: ##   0:00:20  Checking assertions in step 39..
SBY  0:24:27 [bram_bmc] engine_0: ##   0:00:20  Status: passed
SBY  0:24:27 [bram_bmc] engine_0: finished (returncode=0)
SBY  0:24:27 [bram_bmc] engine_0: Status returned by engine: pass
SBY  0:24:27 [bram_bmc] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:20 (20)
SBY  0:24:27 [bram_bmc] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:20 (20)
SBY  0:24:27 [bram_bmc] summary: engine_0 (smtbmc z3) returned pass
SBY  0:24:27 [bram_bmc] summary: engine_0 did not produce any traces
SBY  0:24:27 [bram_bmc] DONE (PASS, rc=0)

SBY  0:24:27 [bram_cov] engine_0: ##   0:00:00  Status: passed
SBY  0:24:27 [bram_cov] engine_0: finished (returncode=0)
SBY  0:24:27 [bram_cov] engine_0: Status returned by engine: pass
SBY  0:24:27 [bram_cov] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY  0:24:27 [bram_cov] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY  0:24:27 [bram_cov] summary: engine_0 (smtbmc z3) returned pass
SBY  0:24:27 [bram_cov] summary: engine_0 did not produce any traces
SBY  0:24:27 [bram_cov] DONE (PASS, rc=0)