Cross coverage of assertion property

I’m trying to make a cross coverage from covergroup with assertions as the below.
for example, If I make 2 assertion properties, how do I make a cross coverage of assertion properties ?

property reset_assertion_check;
	@(posedge clk) (!reset_n |=> (pulse_out ==0));
endproperty

reset_assertion_check_1 : assert property (reset_assertion_check)
cover_assert_reset : cover assert property(reset_assertion_check);



property pulse_out_check;
	@(posedge clk) (!o_en => pulse_out==0)
endproperty

pulse_out_check_1 : assert property(pulse_out_check);
cover_pulse_out_check : cover assert property(pulse_out_check);

As I undersatnd cross coverage concept is exist in systemverilog for normal RTL. But I don’t know whether I can use the cross coverage concept of assertion or not.

There is no need to use both assert and cover directives on the same property. Passing actions on both directives is considered functionally covered.

A covergroup cross ties multiple coverpoints to common sampling event. And if the coverpoints have multiple bins for different values, the cross creates combinations for the different values.

An assertion property is either true or false and there is only one corresponding bin for a passing assert or cover directive. So crossing assertions for coverage does not make a lot of sense. You need to give us a better description of the requirements you are trying to create coverage for.

1 Like