求助：sva的问题？

yuanpin318

谁能简化下面的sva?

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);

总想第一个always可以用sva简化，但不知怎么做，高手请指教。

nangua001

不知道，帮顶

whxqq

assert property @(posedge clk)  a  ##3  check_en;

hi_johnson

assert property @(posedge clk)  (!a) |=> (check_en == 0 && cnt == 0);
assert property @(posedge clk)  (a && cnt == 3) |=> check_en;