[sv-ac] RE: 1932 comments

Hi Doron,

 

Please, see my comments below.

 

Thanks,

Dmitry

 

________________________________

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

 

Hi Dmitry, 

 

Thanks for the review

 

I have implemented most of your remarks. I have some comments see below.

I will send the fixed version once I implement Yaniv's commens

 

Doron

 

*	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.

 

*	Page 13. "Implicit_always: assert property(p);" -->
"implicit_always".

[[DB:]] I don't understand this comment

[Korchemny, Dmitry] "implicit_always" should be in the lower case.

 

*	Page 25. 4). Insert values for accept_on and reject_on from
1751. Also in M.2 (page 26).

[[DB:]] Should be at 2250

[Korchemny, Dmitry] OK


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