Subject: Re: Final Assertion Spec -- problem noted.
From: Adam Krolnik (krolnik@lsil.com)
Date: Fri Apr 05 2002 - 13:11:31 PST
Good afternoon Dr Bassam;
It is good to hear input from others on this important topic.
BTW, would someone like to write up an equivalent assertion to check
the case I have provided - I would like to understand how to do
this at the least in this model so I can teach other...
I also would like to see a real example where the nonconsuming method
is necessary.
You write:
>So, I think since assertions will be incorporated in a -design-
> (i.e. (one possible) implementation of the spec) "simple" semantics
> as above asserts a req should be followed by a done... are in order.
I have worked on projects at two different companies that have
used and understood the model that consumes events. I have
concrete examples where a consuming model is simpler to comprehend
since it operates with principles similar to the hardware being
examined.
I think your example shows how this 'easier' model will in the end
be more difficult for the designer to use.
If a user wants to check the additional requirement of "Each req has
a unique done" they would have to state this abstract notion in
"implementation terms" which could vary from:
"No 2 requests can follow without an intermediate done" for some
implementations
"..." some other implementation may have adequate handshake and
thus more accurately control the check spawning (if req && ...)
... done && ...
...
With a consuming model, the assertion
if (req) assert ([1:10];done);
Is safer and simple than trying to teach a designer
if (req)
begin
req_counter = req_counter + 1;
assert (req_counter != 2);
assert (!req*[1:10]; done) req_counter = req_counter - 1;
end
This may be a simpler model, but is this the more common (and
expected case?) I would suggest that for a designer this is not
what they want to be doing.
If they write the above simple assert, it may work for them
for a while until they get a more aggressive design (which is
when bugs tend to occur - go figure...) which brings the requests
closer together and then there is no corresponding done. It is
an unsafe model!
If this is the model for simplicity then I would like to understand
how the assertion spec could grow in 3.1, 4.0, etc. to include
the consuming model. I would then recommend that the variable
repeat count (min, max) capability be removed due to its unsafe
nature.
I would like to understand what the other people with assertion
or formal proving tools do for this case?
Thanks Dr Bassam for contributing to an interesting discussion.
Adam Krolnik
Verification Mgr.
LSI Logic Corp.
Plano TX. 75074
This archive was generated by hypermail 2b28 : Fri Apr 05 2002 - 13:12:50 PST