アサーションを試してみる(SVA編)

アサーションって結構重要そうってことはovl_assertionでも書いたとおりですが、今回はSystem Verilogの１つの機能であるSVA(System Verilog Assertion)を触ってみようと思います。

SVAはSystem Verilogの機能ですが、構文もまるで違うし、System Verilog対応をうたっているシミュレータでも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違反があったところを表示してくれるので少し嬉しいですね。