Subject: Re: FW: Minutes of Assertion meeting 3/21/02
From: Adam Krolnik (krolnik@lsil.com)
Date: Thu Mar 28 2002 - 13:18:47 PST
Hi Erich;
Thanks for the explanations.
What about a range where the minimum can be the same cycle?
{ a |-> { {0 to 9}; b} } -- Sugar ?
A implies B in (the current cycle) 0..10 cycles later.
I am also curious about references to values in the past or future
|
| delay(signal, 1) == signal
Is this?
prev(signal) == signal -- Sugar?
Hmmmm,
I just read your second mail, it is not there. This concerns me
because this then requires one to write additional code (potentially
in a different part of the file) to support an assertion. This code
also shouldn't be synthesized.
I don't understand your though that this shouldn't be part of the
formal language. When you have very complex, large pipelined designs
the need for a feature like this is fundamental to motivating
designers to use assertions. This is due to the ease of writing
assertions with this capability and the difficulty in maintaining
the assertions without them.
Maybe this is a place where the assertion committee can recommend
this feature to the formal committee. I thought one of the points we
are trying to make with the assertion construct is that you don't have
to construct state machines and other complex structures to write
some basic correctness checks. Without a simple ability to access
previous values (or future based on your outlook) you are forced
to construct these complex structures.
Adam Krolnik
Verification Mgr.
LSI Logic Corp.
Plano TX. 75074
This archive was generated by hypermail 2b28 : Thu Mar 28 2002 - 13:20:23 PST