Subject: RE: [sv-ac] Zero/Non-zero delay model (is it same as synchronous vs asynchronous)
From: Harry Foster (harry@verplex.com)
Date: Thu Sep 19 2002 - 21:51:45 PDT
Hi Rajeev,
> I would seek feedback from the end users/managers like Adam Krolnik
> and Harry Foster who have had extensive experience with assertion
> methodology as to a) whether the "delay independent" specification
> could limit any of their assertion b) if not, what training/guidelines
> they used to ensure that the designers/assertion writers do not make
> such mistakes.
Maybe you are asking the wrong person here... ;-) One of the big points
Lionel Bening and I were promoting in our book was the complete elimination
of #delays when coding RTL models (with very, very, very rare exceptions).
We know from experience that
you can successfully model (and then build) complex multi-million gate
designs without a single delay in the RTL model (and again, I want to
emphasize that there are a few exceptions), and without all the headaches
and nightmares typically experienced with #delays.
Concerning assertions: On the previous projects I worked on, we restricted
assertions to synchronous semantics. Related to assertion adoption, I agree
with you that nothing will "poison the water sooner" than having the
designer waste time tracking down problems that ultimately are *not* bugs.
Tony Hoare once said that there are two ways to do a design. One way is to
make it so simple--that there are OBVIOUSLY no errors. The other way, is to
make it so complicated--that there are NO obvious errors. I hope we
remember this as we develop our assertion language....
Best regards,
-Harry
---------------------------------------------------------
Harry Foster Tel 972-423-3186
Chief Architect Cell 408-234-7637
Verplex Systems, Inc. mailto:harry@verplex.com
300 Montague Expwy, Suite 100 www.verplex.com
Milpitas, CA 95035 www.verifiableRTL.com
-----Original Message-----
From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org]On
Behalf Of Rajeev Ranjan
Sent: Thursday, September 19, 2002 5:25 PM
To: sv-ac@server.eda.org
Subject: [sv-ac] Zero/Non-zero delay model (is it same as synchronous vs
asynchronous)
Hello folks --
I guess we can take a short break from the issue of "to mandate or not
to mandate" the check names. I wanted to bring up another
controversial issue of synchronous vs asynchronous semantics and
support.
As I recall, with our discussion over the phone and via emails, we
still did not get to the same page on our understanding about what we
mean when we use the terms "synchronous" and "asynchronous". I will
refer to the mails sent earlier by Adam Krolnik and Ambar Sarkar.
Let me begin with elaborating on what my basic concern is:
Consider the following piece of Verilog code:
assign c = a ^ b;
always @(d) begin
a <= #10 d;
b <= #20 d;
end
Assume for a moment that the signal "d" changes every 100th time unit
(e.g. wrt a clock) and has been properly initialized. Now consider the
assertion which states that "c" is always "0". Any verification
technology which builds a zero-delay model of the design will come
back with a "YES"/"PASS" answer for that assertion. However, the
signal "c", if implemented in hardware with the given delay
specification will have a glitch. And an event driven simulator which
has sufficient enough granularity of time instants at which it
evaluates the design will FAIL the assertion (i.e. will identify a
glitch).
And that's my fundamental concern. If the analysis of the assertions
within the design is contingent upon evaluating the design at discrete
points which are determined by the explicit delays specified, then we
are going to run into mismatch in results.
I think either Erich or Ambar pointed out that by providing a
sufficiently fine grained clock one could expect even a zero-delay
model analysis to produce the same result. That is not true. What
needs to happen is that the computation model needs to take the
individual gate delays into account. And now we are getting in the
territory of higher complexity analysis than the formal analysis of
zero-delay models. I don't intend to go into the details of relative
analysis complexity of a "timed automata" vs "regular DFA". It
suffices to say that formal/semi-formal tools need to build an FSM
model and their capacity of dealing with models with delays will be
highly limited.
To some extent (or to a large extent, depending upon the optimization
put into the simulation tools), similar observations are made between
a simulation tool leveraging the cycle-based semantics vs one which is
completely event-driven.
So what's the bottomline?
I will re-emphasize a point that Adam had made in one of his emails --
we as a committee should create a set of guidelines on using the
assertion constructs -- the scenarios where they work best, scenarios
which could lead to very poor performance, perhaps a difference in
analysis results between tools, etc.
And I would propose that one of the item in the guideline should be
assertions should be written to check functionality which are
independent of the gate delays in the RTL.
Why is it important/necessary: I could write a whole sermon here --
but the summary is: we are in the very early phase of assertion based
verification methodology and we must do our best to avoid potential
pitfalls that users may get into and avoid situations where their
performance expectations could take a major hit.
I would seek feedback from the end users/managers like Adam Krolnik
and Harry Foster who have had extensive experience with assertion
methodology as to a) whether the "delay independent" specification
could limit any of their assertion b) if not, what training/guidelines
they used to ensure that the designers/assertion writers do not make
such mistakes.
Thanks for your attention...
-rajeev
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Rajeev K. Ranjan Tel: (408) 982-5418
Director, R&D Fax: (408) 982-5443
Real Intent
3910 Freedom Circle, Suite 102A rajeev@realintent.com
Santa Clara, CA 95054 http://www.realintent.com
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
This archive was generated by hypermail 2b28 : Thu Sep 19 2002 - 21:52:02 PDT