Assertion having multiple clocks

SystemVerilog
1

Hi, I am implementing the below problem statement need some help!!! In Fig1, when sig_a becomes 1, after 6 cycle out becomes high.

Note: sig_a & out will be always a 1 clock cycle pulse reference to clk1

Fig_1
Fig_11894×265 12.4 KB

In Fig_2, when sig_a becomes high after 5 cycles out becomes high.

Fig 2
Fig 21897×226 12.1 KB

This can be implemented using 2 assertions :

property sig_a_out_check_1:
   $rose(sig_a) ##0 clk2 |-> ##6 $rose(out) ##1 $fell(out);
endproperty

property sig_a_out_check_2:
   $rose(sig_a) ##0 !clk2 |-> ##5 $rose(out) ##1 $fell(out);
endproperty

assert property (@ (negedge clk1) (disable iff rst) sig_a_out_check_1);
assert property (@ (negedge clk1) (disable iff rst) sig_a_out_check_2);

But i want to know can we implement using a single assertion?
2

You are beter off keeping those as 2 separate assertions;
It’s easier to debug.
If you really MUST have one assertion, you can always
AND the 2 properties in one assertion