Subject: Re: Final Assertion Spec -- problem noted.
From: Bassam Tabbara (bassam@novas.com)
Date: Fri Apr 05 2002 - 17:31:11 PST
Hey Adam,
Finally, I can manage to sneak in some work :-)!
Thanks again for raising this issue ... let me clarify my thinking a
bit. In summary, I think writing a few lines of SystemVerilog + few more
asserts in DAS seems like a small price to pay for being precise. Let me
explain ...
Reading your comments below,.many times you mention "consume", and
"hardware" that implements this model ... The word "consume" is
overloaded with semantics, and requires a good degree of modelling.
Please note that the assertions of DAS are concurrent processes that run
-without mutual interaction- merely observing the state of the design.
The word "consume" (and "hardware" that implements this consumption)
suggests that you are thinking of a model where the assertions are
interacting (composed somehow to form a model of computation, they never
disturb the design, but they DO affect one another).
For example in the req ... req ... done, we want a req to be associated
with a done. Well I ask, what is the semantics of the composed machine
(For example say our 2 spawned assertions created at the first req and
at the 2nd req communicating somehow) .... does it consume based on:
req (req ...done) ? or is it -req- .... req .... -done- ?
Of course, probably this can be resolved, since every time it spawns a
new assert it can create some well-defined dependency on the old one (a
la what Erich covered), so may be a keyword in the assert here can do
this upgrade.
But I ask you a deeper question: What if some other checker in the
system depends on "done" ? e.g.
req -> done
a -> b -> c -> done
If we go by "consuming" things, then any assertion that shares some
signal support with another assertion there is a dependency i.e. -global
state- of assertion system... and how do we resolve this ? Well we will
need a model of computation (say processes with queues and some read
policy ....). The policy we build may or may not be how the design
behaves, or we need to ask for guidance again on how to do (:-)!!).
So again, "localized" checkers that have a small view of the design
world are not intended for
such abstract concept. The context of providing assertions inlined in
code does not give much room for more powerful constructs. Yes to
address a more general concept we will need all of sequences,
composition of sequences, ADTs .... As you can tell by my comments (and
your word of "hardware") this would require even some mixing of
modelling/checking. This is more of vfv type of spec (which when mapped
to assertions would in general create both SystemVerilog for modelling
and "localized" assertions ...).
All that said, again, a small price of some SystemVerilog for modelling
(i.e. to resolve dependencies etc...) is more to the point -in the DAS
context-. Please, I am not saying what's useful or not, needed or not,
or even easy/hard.... but rather what "fits" and what does not (and not
worthwhile to make fit...). I would say the issue you raise falls under
"composition" of sequences (i.e. merging), I am not sure there is a
clean way to do this (quickly...), right now SystemVerilog has to be the
conduit of things.
Thx.
-Bassam.
Adam Krolnik wrote:
>
> 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
-- Dr. Bassam Tabbara Technical Manager, R&DNovas Software, Inc. bassam@novas.com (408) 467-7893
This archive was generated by hypermail 2b28 : Fri Apr 05 2002 - 17:36:39 PST