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

Hi Lisa,

Lets look at a specific example:

A1: assert property(@(posedge clk) a[->] #-# b);
A2: assert property(@(posedge clk) a #=# b);

Suppose that in a computation of 2000 clk ticks, "a" holds only at tick
1000 and "b" holds at every tick. 

Then there 2000 attempts for both assertions. For A1, there is a match
of the antecedent in the first 1000 attempts, after which "b" holds, so
it succeeds at the first 1000 attempts and fails at the last 1000. For
A2, there is only one attempt with a match (number 1000), so it fails
1999 times and succeeds only once.

Hoe that helps.

Doron

>>-----Original Message-----
>>From: Lisa Piper [mailto:piper@cadence.com]
>>Sent: Wednesday, January 30, 2008 6:06 PM
>>To: john.havlicek@freescale.com; Bustan, Doron;
eduard.cerny@synopsys.com;
>>yaniv.fais@freescale.com; Korchemny, Dmitry;
>>Manisha_Kulshrestha@mentor.com; johan.martensson@jasper-da.com;
Seligman,
>>Erik; bassam.tabbara@synopsys.com; thomas.thatcher@sun.com
>>Cc: sv-ac@eda.org
>>Subject: RE: review friendly amendments for 1932
>>
>>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.