Re: [sv-ac] 16.12.10 Nexttime property // clarification question

Dana,
Thanks. I am still not clear. For

ap_acd: *assert property*(*a* |-> *s_nexttime [2] (c ##3 d)* );****

Assume for simplicity, that a==c==d==1 at all cycles, an for the purpose of
discussion, we'll address a single attempt of *ap_acd.* ****

Also assume that there are many many cycles after that one attempt where
"a==1". Again, for this analysis, I am only looking at that one attempt of
the assertion *ap_acd*. ****

In (a |-> nexttime [2] (c ##3 d))

Given that there are enough cycles, what would a simulator give me for the
attempt of the assertion that started at cycle 10?

A failure at cycle 12?

A success at cycle 13 ?

Thanks,

Ben
On Mon, Jan 30, 2012 at 9:20 AM, Dana Fisman Ofek
<Dana.Fisman@synopsys.com>wrote:

> ap_acd: *assert property*(*a* |-> *s_nexttime [2] (c ##3 d)* );****
>
> Assume for simplicity, that a==c==d==1 at all cycles, an for the purpose
> of discussion, we'll address a single attempt of *ap_acd.* ****
>
> Also assume that there are many many cycles after that one attempt where
> "a==1". Again, for this analysis, I am only looking at that one attempt of
> the assertion *ap_acd*. ****
>
> In (a |-> nexttime [2] (c ##3 d))
>

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.