Subject: Action items for Rajeev Ranjan
From: Rajeev Ranjan (rajeev@realintent.com)
Date: Sun Aug 18 2002 - 09:54:15 PDT
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 : Sun Aug 18 2002 - 09:55:52 PDT