SymbiYosysによるデザイン検証の続き：FIFOの検証で、検証が失敗するケースをデバッグする。
練習問題
[script] nofullskip: read -define NO_FULL_SKIP=1 noverific: read -noverific read -formal fifo.sv hierarchy -check -top fifo -chparam MAX_DATA 17 prep -top fifo
追加したhierarchyコマンドは、トップ・モジュールのMAX_DATAパラメーターを17に変更する。basicタスクを実行し、何が起こるか見てみよう。Assert failed in fifo: a_count_diff のようなエラーが出るはず。すべてのテストに合格しながら、MAX_DATAのより大きな値で動作するようにverilogコードを修正しましょう。
実行すると以下のようにエラーが生成された：
$ sby fifo.sby -f basic
SBY 16:41:32 [fifo_basic] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0) SBY 16:41:32 [fifo_basic] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0) SBY 16:41:32 [fifo_basic] summary: engine_0 (smtbmc boolector) returned FAIL SBY 16:41:32 [fifo_basic] summary: counterexample trace: fifo_basic/engine_0/trace.vcd SBY 16:41:32 [fifo_basic] summary: failed assertion fifo.a_count_diff at fifo.sv:106.13-107.71 in step 17 SBY 16:41:32 [fifo_basic] DONE (FAIL, rc=2) SBY 16:41:32 The following tasks failed: ['basic']
このエラーは、アドレスの差分と、現在のデータ個数がマッチしていない、ということだな。
// count should be equal to the difference between writer and reader address
a_count_diff: assert (count == addr_diff
|| count == MAX_DATA && addr_diff == 0);
以下のような感じ。 waddr と raddr は4ビットでカウントしているのだが、 MAX_DATAが17になっているので、計算がおかしくなっている。
という訳で、アドレスに関する部分をすべてパラメタライズすればいいということになる。
diff --git a/docs/examples/fifo/fifo.sv b/docs/examples/fifo/fifo.sv index ba4d8e7..2058831 100644 --- a/docs/examples/fifo/fifo.sv +++ b/docs/examples/fifo/fifo.sv @@ -2,7 +2,7 @@ module addr_gen #( parameter MAX_DATA=16 ) ( input en, clk, rst, - output reg [3:0] addr + output reg [$clog2(MAX_DATA)-1:0] addr ); initial addr <= 0; @@ -25,15 +25,15 @@ module fifo ) ( input wen, ren, clk, rst, input [7:0] wdata, output [7:0] rdata, - output [4:0] count, + output [$clog2(MAX_DATA):0] count, output full, empty ); wire wskip, rskip; - reg [4:0] data_count; + reg [$clog2(MAX_DATA):0] data_count; // fifo storage // async read, sync write - wire [3:0] waddr, raddr; + wire [$clog2(MAX_DATA)-1:0] waddr, raddr; reg [7:0] data [MAX_DATA-1:0]; always @(posedge clk) if (wen) @@ -87,7 +87,7 @@ module fifo `ifdef FORMAL // observers - wire [4:0] addr_diff; + wire [$clog2(MAX_DATA):0] addr_diff; assign addr_diff = waddr >= raddr ? waddr - raddr : waddr + MAX_DATA - raddr;
これで正しく動作した：
SBY 16:49:12 [fifo_basic] engine_0: ## 0:00:00 Checking assertions in step 18.. SBY 16:49:12 [fifo_basic] engine_0: ## 0:00:00 Checking assumptions in step 19.. SBY 16:49:12 [fifo_basic] engine_0: ## 0:00:01 Checking assertions in step 19.. SBY 16:49:12 [fifo_basic] engine_0: ## 0:00:01 Status: passed SBY 16:49:12 [fifo_basic] engine_0: finished (returncode=0) SBY 16:49:12 [fifo_basic] engine_0: Status returned by engine: pass SBY 16:49:12 [fifo_basic] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:01 (1) SBY 16:49:12 [fifo_basic] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:01 (1) SBY 16:49:12 [fifo_basic] summary: engine_0 (smtbmc boolector) returned pass SBY 16:49:12 [fifo_basic] summary: engine_0 did not produce any traces SBY 16:49:12 [fifo_basic] DONE (PASS, rc=0)
