Complex asssertion sequence PSL

[Shail]

Hi,

I have requirement as follows and I wrote a assertion thinking that it
should work, but somehow it is failing ( to catch deliberately
introduced error).. Can anybody help ?

-ok Rules are
I have two set of data i and q which are fed to block. When the i or q
starts toggling from 0 to 1, my input is said to have started.

IF at anytime, I and Q both remain 0 for continous 5 cycles , then in
next 15 cycles, module must generate one and only one pulse of int
signal. There must no int pulse generated again until new seq starts
again (ie i and q starts putting put 1s and 0s)..

There must be no int pulse when I and Q are non-zero.

I wrote assertion this way :

vunit txchip_checks (txchip_tb(test))
{

default clock is rising_edge(clk);

--stop condition -five continuous cycles of 0 for i and q
sequence tx_iq_stopped is { {txchip_i = '0' and txchip_q = '0'}[*5]};

--start condition
-- nonzero combination of i&q after reset
-- or
-- nonzero combination of i&q after stop condition

sequence tx_iq_started is { {rst = '1'; (rst = '0')[+];(txchip_i or
txchip_q)[*1]} |
{(tx_iq_stopped)[+];(txchip_i or
txchip_q)[*1]}
};

--check that once data started,
-- no interrupt till data stops
-- then just one interrupt in next 15 clocks
-- no interrup then on
-- teminate check when new data starts.

property single_int is always { tx_iq_started } |=>
{ (txchip_int = '0')[*]; tx_iq_stopped;[*0 to 15];(txchip_int =
'1');
(txchip_int = '0')[+]; tx_iq_started
};

assert single_int;
}


Then I wrote vhdl code such that Int is of two clocks. still asssertion
said to have Passed.

What is wrong here ?

Again, Is there any way if I want to debug Assertion step-by-step?

Thanks,
Shailesh