アサーションを試してみる(SVA編)
アサーションって結構重要そうってことはovl_assertionでも書いたとおりですが、今回はSystem Verilogの1つの機能であるSVA(System Verilog Assertion)を触ってみようと思います。
SVAはSystem Verilogの機能ですが、構文もまるで違うし、System Verilog対応をうたっているシミュレータでもSVAには非対応というものが存在するので、自分のシミュレータで使用できるかどうか予め確認が必要です。
このページでは、Riviera-PROでSVAを使ってみるまでをまとめています。
Riviera-PROでSVAアサーション
SVAはSystem Verilogの機能なので、対応しているシミュレータを使えば特にlibraryをインクルードせずに使用可能です。ovl_assertionと同じRTLと、テストベンチを使い、アサーション部分だけSVAに書き換えてみました。
テストベンチ
`define CYCLE 20 //50MHz `default_nettype none module sva_example_test; parameter N = 8; parameter STOP = 8'hf0; reg iCLOCK; reg inRESET; reg iCORECT; wire [N-1:0] oCOUNT; sva_example #( N, STOP )TARGET( .iCLOCK(iCLOCK), .inRESET(inRESET), .iCORECT(iCORECT), .oCOUNT(oCOUNT) ); initial begin #0 begin iCLOCK = 1'b0; iCORECT = 1'b0; inRESET = 1'b0; end #1 begin inRESET = 1'b1; end #(`CYCLE * 2000000)begin $finish; end end //initial always#(`CYCLE /2)begin iCLOCK = !iCLOCK; end endmodule //test bench `default_nettype wire
ターゲットRTL
`default_nettype none module sva_example #( parameter N = 8, parameter STOP = 8'hf0 )( input wire iCLOCK, input wire inRESET, input wire iCORECT, output wire [N-1:0] oCOUNT ); //Counter reg [N-1:0] b_counter; always@(posedge iCLOCK or negedge inRESET)begin if(!inRESET)begin b_counter <= {N{1'b0}}; end else begin if(iCORECT)begin if(b_counter < STOP-{{N-1{1'b0}}, 1'b1})begin b_counter <= b_counter + {{N-1{1'b0}}, 1'b1}; end else begin b_counter <= {N{1'b0}}; end end else begin b_counter <= b_counter + {{N-1{1'b0}}, 1'b1}; end end end //end always : counter /*****Assertion(SVA)*****/ //Property property PRPTY_CNT_0_STOP; @(posedge iCLOCK)( (b_counter >= {N{1'b0}} && b_counter < STOP) ); endproperty //Assert ast_cnt_0_stop : assert property(PRPTY_CNT_0_STOP) else $error("[Error][SVA][%m] : range over error"); //ast_cnt_0_stop : assert property(PRPTY_CNT_0_STOP); assign oCOUNT = b_counter; endmodule `default_nettype wire
Riviera-PROでSVAを用いる場合、simulation後にproperty違反があったところを表示してくれるので少し嬉しいですね。