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