[sv-ac] RE: review friendly amendments for 1932

From: Lisa Piper <piper_at_.....>
Date: Wed Jan 30 2008 - 08:05:40 PST
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