How to simplified the following SVA?

[yuanpin318]

I am newer for SVA:

I wrote the code:

always @(posedge CLK)
if (a == 1)
begin
if (cnt <3)
begin
cnt ++;
end
else
begin
check_en <= 1;
end
end
else
begin
cnt <= 0;
check_en = 0;
end

assert property @(posedge clk) (check_en |-> b == 0);

I felt it's very tedious for the verilog code, anyone cany simplified this SVA?

 

[ljxpjpjljx]

what do you want to verify?

 

[yuanpin318]

I'm going to check if signal a is asserted for 3 cycles, then in continuous cycles, if a == 1, expect b == 0