Question on muti-thread and single-thread sequences

SystemVerilog
11

Hi Ben,
thanks a lot for immediate reply.

  1. Now the property for clk2 has been written as :

drclk1: assert property (
   disable iff (reset) @ (negedge clk) clk2==0 |-> ##1 clk2==0 ##1 clk2==1[*2]);

Since clk2 is clk divided by 4, we could also have written this as :


drclk1: assert property (
   disable iff (reset) @ (negedge clk) clk2==0 |-> ##2 clk2==1);
drclk1_1: assert property (
   disable iff (reset) @ (negedge clk) clk2==1 |-> ##2 clk2==0);

Though this will not check the clk2 at intermediate clocks. It will not ensure a 50% duty cycle clk2. Have you written it to ensure 50% duty cycle.

  1. Can this property also be written using @rose and $fell, since for clk2, referring to the waveform you have given, after a posedge is detected for clk2, clk2 will be 0 after two clks and after clk2 falling edge, it will be 1 after two clks again:

drclk1: assert property (
   disable iff (reset) @ (negedge clk) $rose(clk2) |-> ##2 clk2==0);
drclk1_1: assert property (
   disable iff (reset) @ (negedge clk) $fell(clk2) |-> ##2 clk2==1);

Though this does not check for 50% duty cycle. Is this correct?

thanks and regards,
-sunil