Subject: [sv-ac] Re: Action items for Rajeev Ranjan
From: Ambar Sarkar (ambar.sarkar@paradigm-works.com)
Date: Thu Aug 22 2002 - 04:49:09 PDT
Resending(trouble with email carrier!)..
Regards,
-Ambar
----- Original Message -----
From: "Ambar Sarkar" <ambar.sarkar@paradigm-works.com>
To: "Rajeev Ranjan" <rajeev@realintent.com>; <sv-ac@eda.org>
Sent: Thursday, August 22, 2002 7:45 AM
Subject: Re: Action items for Rajeev Ranjan
> Rajeev,
>
> My question is not about allowing #delay in our basic computation model,
> though I don't see why a time delay cannot be handled by assuming a
sampling
> clock that is ticking at the appropriate timescale frequency.
>
> My question, to make it hopefully clearer, is this:
>
> Can we put a constraint that says "do not glich" on a signal that is
sampled
> at a clock edge? Note that the glitch can occur between any two sample
> points, and that the glitch may not consume any time (only consumes
> simulation delta time) at all.
>
> For example, can we create a property saying "no glitch on sampled_signal"
> as shown below?
>
> assign sampled_signal = a ^ b;
>
> always (a2)
> a <= a2;
> always (a1)
> a2 <= a1;
>
> always (b1)
> b <= b1;
>
> Notice that even if a1 and b1 are sampled at the same design clock, a will
> get its final value one delta time later than b.
> A glitch will be seen when a1 and b1 both start as 1, and then both change
> to 0.
>
> I hope this makes my question clearer. And I apologize in advance if I
> misunderstood/misinterpreted anything.
>
> Regards,
> -Ambar
>
> ----- Original Message -----
> From: "Rajeev Ranjan" <rajeev@realintent.com>
> To: <sv-ac@eda.org>
> Sent: Sunday, August 18, 2002 12:54 PM
> Subject: Action items for Rajeev Ranjan
>
>
> > Folks,
> >
> > My apologies for the delay in reponding to my action items. Attached
below
> > are my responses. Feedback, discussions welcome.
> >
> > -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
> > +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
> >
> >
> > Action: RR to clarify the future value requirement
> > Action: RR to provide an example of a future reference and what should
> > happen in simulation and formal analysis.
> > ----------------------------------------------------------------
> >
> > For the purposes of explanation and illustration, I would use the
> > notation "s(k, trigger)" to represent value of a signal "s", "k"
> > positive edges of "trigger" signal from a reference time -- where
> > reference time is the time when the assertion is encountered in the
> > procedural block. "k" could be positive (negative) indicating
> > reference to a future(past) value of "s". "k" itself should be compile
> > time constant.
> >
> > Various usages:
> >
> > if (req)
> > assert(ack(10,clk) == 1'b1); // ack is high at the 10th clock cycle
> >
> >
> > assert(result(5, clk)==operand1+operand2);
> >
> > // The addition of current value of operands is available
> > // in "result" 5 cycles later
> >
> >
> > if (state == READY)
> > assert(prepare(-4,clk) && grant(-2,clk));
> >
> > // If I am in READY state, prepare and grant must have happened 4 and 2
> clock
> > // cycles ago respectively.
> >
> >
> >
> > Behavior in simulation and formal analysis:
> >
> > The lifetime of an assertion involving future reference is until the
> > future time is reached or its truth/falsity is determined. In case
> > the expression involves references to multiple future values -- the
> > maximum future time will be taken. The truth/falsity of the assertion
> > can possibly be determined before the future time is reached -- e.g.
> >
> > assert((foo == bar(3,clk)) || (foo2 == bar2(5,clk)));
> >
> > If the value of "bar" at the 3rd clock cycle is equal to the current
> > value of "foo", the assertion will pass and the corresponding
> > statement will be executed. In the same way:
> >
> > assert((foo == bar(3,clk)) && (foo2 == bar2(5,clk)));
> >
> > If the value of "bar" at the 3rd clock cycle is NOT equal to the
> > current value of "foo", the assertion will fail and the corresponding
> > statement will be executed.
> >
> > The reported time of pass/fail should be the time when the
> > truth/falsity of the assertion is determined and should be identical
> > in formal and simulation tools.
> >
> >
> >
> >
> > Action: RR to write explanation how to refer to asynchronous events.
> > ----------------------------------------------------------------
> >
> > Action Response:
> >
> > I will reproduce Erich's elaboration on synchronous semantics:
> >
> > Cycle based semantics Semantics should be based upon an underlying
> > computational model that involves a succession of times during at
> > which the design and assertions are evaluated. This base case is
> > independent of clocks, and is therefore "asynchronous". The succession
> > of times may be determined by event-driven scheduling, for
> > example. For synchronous modeling, the semantics should be defined in
> > terms of evaluation at time points at which some boolean condition is
> > true (e.g., a clock edge occurs, or an enable is true). The semantics
> > should NOT be defined in terms of time delays.
> >
> >
> > Since we don't yet quite speak in the same terminology, lots of
> > discussions took place in the previous two meetings and it emerged
> > that the primary concern that people have with so called "synchronous
> > semantics" is the ability to refer to a a change in value of a primary
> > input. I pointed out that the even the primary inputs are not changing
> > at arbitrary time points -- either they are changing wrt a design
> > clock or one can define a virtual clock to capture the frequency with
> > which these inputs can change. Just to reiterate, I am trying to
> > eliminate the need to support computation models which are based on
> > time delays.
> >
> > Amber Sarkar pointed out that having to define a virtual clock (if
> > necessary) is an implementation detail of a specific tool - i.e.,
> > reference to change in the primary input values could possibly be made
> > without specifying the real/virtual clock.
> >
> > But in every verification technology, you ARE providing the input
> > stimuli wrt some real/virtual clocks -- when they are not changing
> > with arbitrary time delays. These input stimuli are read in from a
> > file at uniform interval, or are created from a high level description
> > wrt to design/verification clock.
> >
> > Hence the question that needs to be answered is that -- should
> > assertion analysis support computation models which are based on time
> > delays?
> >
> > A yes to this question could mean technologies with higher analysis
> > complexity a) would not support these types of assertions or b) would
> > ignore such time delays and go with the real/virtual clock based
> > computation model leading to differences in analysis results.
> >
> >
> > Action item: List of shorthand for common relationship
> > specification:
> > ----------------------------------------------------------------
> > o exactly one of the element in a set of signals is high
> > o at most one of the element in a set of signals is high
> > o value of a bus is contained in a compile time constant set
> > (equivalent of inset)
> > o detection of a posedge/negedge/any-edge on a signal wrt some clock
> > o detection of stability on a signal/bus for certain number of clock
> > cycles
> >
> >
> > Action item: Similarity of style requirement on SQ9 and SQ10
> > ----------------------------------------------------------------
> >
> > The syntactical form for expressing an event sequence for assertion,
> > coverage, and for trigger usage should be identical.
> >
>
This archive was generated by hypermail 2b28 : Thu Aug 22 2002 - 04:56:20 PDT