[sv-ac] RE: 1932 comments

From: Bustan, Doron <doron.bustan_at_.....>
Date: Mon Jan 28 2008 - 01:35:33 PST
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.

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

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

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

[[DB:]] Should be at 2250


-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.
Received on Mon Jan 28 01:56:57 2008

This archive was generated by hypermail 2.1.8 : Mon Jan 28 2008 - 01:59:14 PST