SVA 再了解(一)

這是一個簡單的 SVA測試例
關於sequence 及property的用法

module test;

reg clk, rst_n;

wire ph1, ph2, ph3;

reg [1:0] ph_fsm;

reg vsync, vsync_d, vsync_start;

reg [9:0] ph1_cnt, ph2_cnt, ph3_cnt;

reg [7:0] phase_loop_cnt;
wire phase_loop_end;

parameter ph1_value =10;
parameter ph2_value =15;
parameter ph3_value =35;

always #5 clk = ~clk;

initial begin
clk =0;
vsync = 0;
rst_n =1;
#100;
rst_n =0;
#100;
rst_n =1;

@(posedge phase_loop_end)
vsync =1;

@(posedge phase_loop_end)
vsync =0;

end

always @(posedge clk or negedge rst_n) begin
if (~rst_n)
ph_fsm <=0;
else begin
if (ph_fsm ==0)
ph_fsm = 1;
else if (ph_fsm == 1 && ph1_cnt == ph1_value)
ph_fsm =2;
else if (ph_fsm == 2 && ph2_cnt == ph2_value)
ph_fsm =3;
else if (ph_fsm == 3 && ph3_cnt == ph3_value)
ph_fsm =1;
else
ph_fsm = ph_fsm;

end
end

assign phase_loop_end = (ph_fsm ==3 && ph3_cnt==ph3_value);

always @(posedge clk or negedge rst_n) begin
if (~rst_n)
ph1_cnt <= 1'b0;
else if(ph_fsm == 2'b01)
ph1_cnt ++;
else
ph1_cnt <= 1'b0;
end

always @(posedge clk or negedge rst_n) begin
if (~rst_n)
ph2_cnt <= 1'b0;
else if(ph_fsm == 2'b10)
ph2_cnt ++;
else
ph2_cnt <= 1'b0;
end

always @(posedge clk or negedge rst_n) begin
if (~rst_n)
ph3_cnt <= 1'b0;
else if(ph_fsm == 2'b11)
ph3_cnt ++;
else
ph3_cnt <= 1'b0;
end

assign ph1 = (ph_fsm == 2'b01);
assign ph2 = (ph_fsm == 2'b10);
assign ph3 = (ph_fsm == 2'b11);

initial begin
$fsdbDumpfile("./test.fsdb");
$fsdbDumpvars(0, test);
$fsdbDumpSVA(0, test);
end

initial begin
#1ms;
$finish;
end

sequence s_ph12_chk_seq;
@(posedge clk) ph1 [->ph1_value] ##1 ph2;
endsequence

sequence s_ph23_chk_seq;
@(posedge clk) ph2 [->ph2_value] ##1 ph3;
endsequence

sequence s_ph31_chk_seq;
@(posedge clk) ph3 [->ph3_value] ##1 ph1;
endsequence

property p_ph1231_chk1;
@(posedge clk) $rose(ph1) |-> ##ph1_value $rose(ph2) |-> ##ph2_value
$rose(ph3) |-> ##ph3_value ph1;
endproperty

property p_ph1231_chk2;
@(posedge clk) s_ph12_chk_seq |-> s_ph23_chk_seq |-> s_ph31_chk_seq;
endproperty

ph1231_chk_sva1: assert property (p_ph1231_chk1)
else begin
$display("\n Fail in ph1231 sva1\n");
#1000;
$finish;
end

ph1231_chk_sva2: assert property (p_ph1231_chk2)
else begin
$display("\n Fail in ph1231 sva2\n");
#1000;
$finish;
end

endmodule