Subject: Re: FW: Minutes of Assertion meeting 3/21/02
From: Adam Krolnik (krolnik@lsil.com)
Date: Fri Mar 29 2002 - 07:15:49 PST
HI Erich;
I think this is a very worthwhile conversation about the differences
between this group and the formal group.
In this first section:
> assert never {a^b; 1; a==b};
>
>It also allows you to say things like
>
> assert eventually {a^b; 1; a==b};
I like the first statement as this is a common assertion I see
designers write. "You can't have this combination and that
combination in the past", or vice versa.
I agree that eventually is generally too long. My preference is
bounded windows (and sometimes bounded by events -- until a).
This is more useful for simulations when you'd rather see that
a transaction not be serviced in a reasonable time period
rather than see a simulation reach a maximum cycle limit and
get a report that a transaction did not complete.
You say, "But Sugar does support the zero-delay implication you
want here.", this is referring to the difference between the
operator |-> and |=>, correct.
BTW, is there a bidirectional implication, "a implies b; b iff prev
a" One can write an equivalent form with implication when only
one outstanding 'a' is allowed, but when multiple are allowed
it is difficult.
Lastly I speculated a syntax for forward and backward value
references:
| Then one could write
|
| a<-2> & b<-1> & c
| or
| a & b<1> & c<2>
You mentioned that efficiency is necessary for implementation.
I had implemented a tool that handled this by converting the
second to the first and adjusting the consequent sequence
times. Thus the notation of forward or backward is a convenience
for the user. Since some think in the past "If I got this and I
created that, then I have a problem" and some think in the future
"If I created that and this occurred and then that occurred, we
have a problem".
Thus either sequeuce would result in the same error message at
the same time - one may argue that "hey, the designer said time 0
was 2 cycles earlier!" I didn't get many arguments about the time
being reported. They were happy that the event/bug was found...
Regardless of whether forward referencing is supported, does any
of this create interest in the ability to reference signal values
from another time/cycle? I do have a harder time convincing designers
that writing code like this is easy:
reg assert0015_delay[1:0];
always @(posedge clk) // hopefully
begin
...
assert_forbid (assert0015_delay[1] & a == b);
//synthesis translate_off
assert0015_delay = {assert0015_delay[0], a^b};
//synthesis translate_on
...
vs.
//forbid (delay(a^b),2) & (a==b));
Adam Krolnik
Verification Mgr.
LSI Logic Corp.
Plano TX. 75074
This archive was generated by hypermail 2b28 : Fri Mar 29 2002 - 07:17:49 PST