System verilog assertion

HI,

Assertion Query :

Spec :

DLL_RESET_SELECT[1:0] #PCS TXCLK cycles
00 ------------------- 10
01 ------------------- 12
10 ------------------- 16
11 ------------------- 25

For the above table, based on select == 00 ,and FSM_STATE == reset in reset mode. reset_sig should be 10 clock cycles low.

I have coded the assertion.but i have a problem with the signal it is not synchronous with the clock.It has a delay of 100ps.see the below diagram

clock - |-1-||-2-||-3-||-4-||-5-||-6-||-7-||-8-||-9-||-10-||-11-||-12-|
reset_sig —|
_________________________________________________________|----------------------------

→ Because of the delay 100ps, The fell and rose is sampled on the next clock edge.So assertion is failing for 10 clock cycles.if i put11 clock cycles the assertion works/Passing.

  • My question is ::: 1) how to handle the delay of 100ps and check for the rose/fell of the reset_signal check ?
    2) Is there any way to handle it in assertion?
    3) Should be in designers point of view…?

Assertion Code :

property DLLFSM_reset_timer_1(int dll_duration);
@(posedge TXCLK)
disable iff(pcs_fsm_ps !== PCS_NORESET)
if(dll_duration == 0)
($fell(reset_signal) |-> ##10 $rose(reset_signal))
else if(dll_duration == 1)
($fell(reset_signal) |-> ##12 $rose(reset_signal))
else if(dll_duration == 2)
($fell(reset_signal) |-> ##16 $rose(reset_signal))
else if(dll_duration == 3)
($fell(reset_signal) |-> ##25 $rose(reset_signal))
else 1’b0;
endproperty : DLLFSM_reset_timer_1

In reply to sraja:

Are you saying that relative to your TXCLK, reset_signal has a 100ps hold time, and of course TXCLK has a period > 100ps?
From your diagram above, ($fell(reset_signal)at the posedge of tick 2.
Then $rose(reset_signal)) should occur on the posedge of tick 12.
So this ($fell(reset_signal) |-> ##10 $rose(reset_signal)) should have worked.
Am I missing something?
If the 100ps is asynchronous, then it’s a different story.

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

  • SystemVerilog Assertions Handbook 3rd Edition, 2013 ISBN 878-0-9705394-3-6
  • 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

In reply to ben@SystemVerilog.us:

HI BEN,

sorry for the delay in replying.

comments to your queries…

Are you saying that relative to your TXCLK, reset_signal has a 100ps hold time, and of course TXCLK has a period > 100ps?

  1. txclk >>100ps
  2. Reset signal is toggling for exactly 10clock cycles.But w.r.t to the edge of the clock there is a delay of 100ps. If I check the duration between rise and fall its exactly 10 clock cycles.

From your diagram above, ($fell(reset_signal)at the posedge of tick 2.
Then $rose(reset_signal)) should occur on the posedge of tick 12.
So this ($fell(reset_signal) |-> ##10 $rose(reset_signal)) should have worked.

  1. I have put 10 clock cycles, so evaluation starts from 2 and until 11.The value at (11th posedge) is still 0.so assertion fails at 12.
  2. Completion of 10 clock cycles is done at 11th clk, by the time reset signal value is still… this is what i observed.
  3. Delay in the signal is 100ps. Instead of starting form clock 1.It starts at clock 2
  4. And the same delay is applicable to the rising edge.

Am I missing something?
7)Still its not so clear i will change the way I explain and let you know.

If the 100ps is asynchronous, then it’s a different story.
8)Its not asynchronous.
9)Its synchronous to clock.

Thanks for the reply.

-Regards,
-Sravan.

The 100ps is a hold time, and has no effect on the assertion.
What you have as an assertion is correct. Below is a simple model, with a hold time (though not needed) along with the simulation results. It works as expected.

module risefall; 
	bit clk, a=1'b1; 
	ap_rf: assert property(@(posedge clk) $fell(a) |-> ##2 $rose(a) ); 
	
	initial forever #5 clk=!clk; 
	
	initial begin 
		@(posedge clk);
		repeat(200) begin 	
			@(posedge clk);
			#1;
			if (!randomize(a)) $error();  
		end 
	end
endmodule


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

  • SystemVerilog Assertions Handbook 3rd Edition, 2013 ISBN 878-0-9705394-3-6
  • 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

In reply to ben@SystemVerilog.us:

H Ben,

Thank you.I want to know the assertion coding is correct or not.

Thanks for validating and confirming it.

-Regards,
-Sravan.