Hi Doron, In addition to the font issues I just sent, I am still troubled with the following: I understood the description and examples, but not the equivalency expressions to |-> and |=>. I am having trouble following what happens at a specific clock tick when the sequence on the LHS is false - does that attempt pass or fail? There is something missing here. [[DB:]] For a specific attempt, if there is no match of the sequence on the LHS, then the property evaluates to false. Comparing to |->,|=> the universal quantifier (for every match) is replaced with an existential quantifier (exists a match). Lisa: So if there is no match of the antecedant, it fails? Let's say the sequence is matched at t=1000. How many attempts pass and how many attempts fail? For example, at time t=100, does an attempt start at t=100 and end at t=1000? Do all attempts from 0 to 1000 end at 1000? Let's say that no attempts match after t=1000. What about the attempt that starts at t=2000? The problem I have is understanding what to do with the counters and error messages? And when do I decide the assertion fails? If the antecedant never happens, then do all attempts fail at the end of simulation? Lisa -----Original Message----- From: John Havlicek [mailto:john.havlicek@freescale.com] Sent: Wednesday, January 30, 2008 10:12 AM To: doron.bustan@intel.com; eduard.cerny@synopsys.com; yaniv.fais@freescale.com; john.havlicek@freescale.com; dmitry.korchemny@intel.com; Manisha_Kulshrestha@mentor.com; johan.martensson@jasper-da.com; Lisa Piper; erik.seligman@intel.com; bassam.tabbara@synopsys.com; thomas.thatcher@sun.com Cc: sv-ac@eda.org Subject: review friendly amendments for 1932 Hi All: This is a reminder that the review of the friendly amendments for 1932 is due. People who sent friendly amendments on 1932 should provide feedback on their implementation in LTL.1932.080129.pdf LTL_Formal.080128.pdf or send mail that no revisions are required. J.H. -- This message has been scanned for viruses and dangerous content by MailScanner, and is believed to be clean.Received on Wed Jan 30 08:06:11 2008
This archive was generated by hypermail 2.1.8 : Wed Jan 30 2008 - 08:06:42 PST