[sv-ac] RE: 1932 comments

Thanks,

Dmitry

 

________________________________

From: Bustan, Doron 
Sent: Monday, January 28, 2008 2:21 PM
To: Korchemny, Dmitry; 'sv-ac@server.eda.org'
Subject: RE: 1932 comments

 

Hi Dmitry,

 

I have fixed the typo

 

Page 8.
"Since the sequential property a ##1 b is used in an assertion, it is
weak. This means that if a holds at the last tick of the assertion's
clock in a simulation, the weak sequential property a ##1 b will also
hold beginning at that tick, and so the assertion a1 will fail. In this
case it is more reasonable to use:"

	*	Need to introduce a clock, say @clk in these examples.

[[DB:]] I add it

	*	I prefer the explanation which would cover both
simulation and formal verification: "This means that if clk stops
ticking and a holds at the last tick of clk, the weak sequential
property a ##1 b will also hold beginning at that tick, and so the
assertion a1 will fail. In this case it is more reasonable to use:"

[[DB:]] I think that in the informal part, the old text should remain.
In my opinion, talking about a clock that stops to tick, is too much of
a corner case for this example.

[Korchemny, Dmitry] I don't think that it is worth to mention simulation
here, since in the simulation the assertion will have status "pending",
and not "fails" in your example. It would be cleaner to talk about the
clock to stop ticking, it will also cover the simulation semantics
automatically.

 

[[DB:]] ok I am convinced, I have changed it

 

---------------------------------------------------------------------
Intel Israel (74) Limited

This e-mail and any attachments may contain confidential material for
the sole use of the intended recipient(s). Any review or distribution
by others is strictly prohibited. If you are not the intended
recipient, please contact the sender and delete all copies.

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.