Asserion help

Its an assertion for iic protocol .
there are two signals - Data , clk .
Start condition - $fell on data , and clk remains stable at 1.
stop condition - $rose on data, and clk remains stable at 1.
At all other times, data can only change when clk is low.

I wrote an assertion -
property sda_tgl_chk();
@(CLK)
!$stable(iic.Sda) |-> $stable(iic.Scl) && !iic.Scl;
endproperty

BUT i have to block this for start and stop condition. I can make an internal signal which detects start and stop and use disable iff with that variable. can it be written in a different way in the assertion body only.

In reply to ashish_banga:

Not being familiar with the protocol, it is hard for me to really guide you. A timing diagram would help. However, as a general commens, it is OK to add supporting logic to an assertion.
Ben

Hi Ben,
its self explanatory in my description. Try to understand it. Data line can only toggle when clk is low, besides a START (negedge on data and clk is high)condition and a STOP (posedge on data and clk is high) condition.
In my assertion i want to chk , between a START and STOP condition,data should toggle when clk is low.

In reply to ashish_banga:
Assertions work with clocking events. Thus, when you say “between a START and STOP condition,data should toggle when clk is low.”, do you mean at the negedge of clock, it can toggle? can it toggle at any time within the clock is low? Do you want to check that it is stable at posedge of clk? If data is a vector, can it toggle to the same value? What is the sampling clock?
SVA assertions were not indented for analog kind of stuff, and that is an unusual application. You should try a SystemVerilog procedural solution, with possibly an immediate assertions within the procedural block.
Is this more of what you want? I did not test it.

 int data; 
// save data @ posedge of clk 
// check for no change @ negedge 
// check for change @ posedge 
// repeat until STOP
property sda_tgl_chk();
	int v; 
	@(posedge clk)(start, v=data) |-> 
(@(negedge clk) v==data ##0 @(posedge clk (1, v !=data, v=data) ) [*1:$] ##1 STOP; 
endproperty

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