How to assert a property is false at every clock cycle?

Question

Is there a way to assert whether a already declared property is false at every clock cycle?

For example,

status[idx] should be high only if both req[idx] and enable[idx] is high.

What I would like to have is a negative scenario checker for the above. i.e. the status should never go high when either req or enable is low.

I tried below but vcs gives me below compilation error

sequence seq_a (int idx);
  !(req[idx] & enable[idx])
endsequence

sequence seq_b (int idx)
  status[idx] == 1
endsequence

property ppty_ab (int idx)
  disable iff (f_req[idx] & f_enable[idx])
  seq_a(idx) |=> seq_b(idx)
endproperty

generate
  for (idx=0; idx<5; idx++) begin
    a_ab : assert property (@(posedge clk) (not ppty_ab(idx)))
           else $display("ppty_ab [%0d] failed at %t",idx,$time)
  end
endgenerate

Error-[PIWDOAACS] Incorrectly used 'disable iff'

Property instances with 'disable iff' are only allowed in "assert" "assume" and "cover" statements. Property p_RiseIntDischeck may not be instantiated in this context.

seq_a and seq_b is already declared and being used for some other assertion. What is the best/recommended way to reuse these sequences and create a negative scenario checker for the above case?

Answer 1

Try putting the clocking and the not into the property itself.

That is:

property ppty_ab (int idx)
  @(posedge clk)
  disable iff (f_req[idx] && f_enable[idx])
  not seq_a(idx) ##1 seq_b(idx)
endproperty

generate
  for (idx=0; idx<5; idx++) begin
    a_ab : assert property (ppty_ab(idx))
           else $display("ppty_ab [%0d] failed at %t",idx,$time)
  end
endgenerate

Where not seq_a(idx) ##1 seq_b(idx) is not the same as !seq_a(idx) |=> seq_b(idx), but the not will make the property evaluate to true when the statement is false.

I am assuming that disable iff requires that the property is clocked, although I am not sure why.