Subject: Re: Final Assertion Spec -- problem noted.
From: Adam Krolnik (krolnik@lsil.com)
Date: Fri Apr 05 2002 - 12:26:30 PST
Hello Erich;
Thank you for the background on the various semantics. I have
not had a study in material like this...
So you say that there are equally valid cases for either
first-match or all-match semantics. The current assertion spec
calling for first-match semantics, correct? I didn't quite understand
which model is being implemented in the assertion spec.
As it stands, the model now has problems for multiple threads
when used in a combinatorial block (due to potential #delay
signals arriving at various time) and when used in a clocked
block (due to the nonconsuming model for overlapped threads.)
I see these problems as a serious detractor to temporal assertions.
How do I explain to designers about the first-match vs. all-match
semantics when they are asking how to check a pipeline or a
handshaked interface? There is a big difference between the
assertions that a designer of logic writes and a property /
constraint that a skilled formal verification person will write.
What do we do? I don't see this model as fixable. The assertion
model I have (I would tend to call first-match) consumes events,
keeps them ordered is implementable in a fixed set of resources
is a synthesizable representation, etc.
What do others on this committee have?
How do you then write an assertion to ensure
the protocol in my example (pipelined request/acknowledge)
is proper?
Erich, you did bring up the question about intepreting 2 cycle
(or multiple cycle events as only 1 event.) This is an example of
why I proposed posedge() semantics (as a solution to this) but
there is probably more background as to why this is insufficient.
You also noted that the association of req to the proper ack may
not be necessary. But it will be if one wants to say.
if (req) assert ([1:10]; done)
begin // the passing
print "Got this data for the req %h.", data);
...
A designer would use the inorder (expected) characteristics to
examine data associated with the event. This expectation can't
be violated.
Is it possible to have both? Or are we asking too much? If we don't
have both, what do you do when you need the other model?
Adam Krolnik
Verification Mgr.
LSI Logic Corp.
Plano TX. 75074
This archive was generated by hypermail 2b28 : Fri Apr 05 2002 - 12:27:49 PST