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

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/properties and create a negative scenario checker for the above case?

In reply to vvs3693:
In general, assertions should be expressed in a ‘positive’ direction,
meaning “if trigger_conditions then expected_resuls”. Thus, for


// the status should never go high @ next cycle when either req or enable is low
ap_reqenb: assert property(
 !req || !enb |=> status==0);  

You should also use Binary logical operators (e.g., && ||) instead of Binary bitwise operators (e.g., & | ), as they have different meanings.
Below is updated code that compiles and elaborates OK. Your code has lots of errors; I am surprised that it compiled.


module top; 
	bit clk, a;  
	default clocking @(posedge clk); endclocking
		initial forever #10 clk=!clk; 
		int idx; 
		logic[0:7] req, enable, status, f_enable, f_req; 

		/* 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]); // !(a&&b)  !a || !b
	endsequence
 
	sequence seq_b (int idx);
		status[idx] == 0;  // the status should never go high when either req or enable is low 
	endsequence
 
	property ppty_ab (int idx);
		disable iff (f_req[idx] & f_enable[idx])
			seq_a(idx) |=> seq_b(idx);
	endproperty
 
	generate
		for  (genvar  idx=0; idx<5; idx++) begin
			a_ab : assert property (@(posedge clk) ( ppty_ab(idx)))
			else $display("ppty_ab [%0d] failed at %t",idx,$time);
	   end
	endgenerate	
endmodule 

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us

  • SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
  • A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
  • Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
  • Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 0-9705394-2-8
  • Component Design by Example ", 2001 ISBN 0-9705394-0-1
  • VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
  • VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115