RE: [sv-ac] RE: review 1681 (global clocking)

Hi Neil,

Automata for both properties have 3 states: s1, s2 and s3. s1 is an
initial state, and it is also active at each primary phase, because of
the always operator. From the state s1, the automata may transition to
the state s2 when they see a. From the state s2 there is a transition to
s3 under !b which corresponds to the assertion failure.

The key point is that the global clock is considered to be a primary
clock in formal verification, therefore the automaton for the property
p1 has two direct transitions: s1 -> s2 and s2 -> s3, and it actually
does not depend on any clock. As for the property p2, each transition is
enabled on the posedge clk only. When in the state s2, the automaton
will remain there until it sees posedge clk. This explains why there is
a self loop s2 -> s2 in the second automaton.

When p1 fails, the counterexample will contain values of a and b only,
while for p2 it will also contain the value of clk. 

To be able to check the "unclocked" properties in simulation a mapping
is needed from the primary clock to a real signal (event). The global
clocking just defines this mapping.

Regards,
Dmitry

-----Original Message-----
From: Neil.Korpusik@Sun.COM [mailto:Neil.Korpusik@Sun.COM] 
Sent: Tuesday, June 26, 2007 11:20 PM
To: sv-ac@eda.org
Cc: Korchemny, Dmitry
Subject: Re: [sv-ac] RE: review 1681 (global clocking)

Hi Dmitry,

I must be missing something obvious here. Could you
explain why the following two assertions are producing such
different state diagrams?

I don't see anything in the actual proposal that would explain this.

   always p1: assert property (@$global_clock a |=> b);
   always p2: assert property (@(posedge clk) a |=> b);

   "The first automaton is simpler: it does not have clocking conditions
   along its edges, and it does not have an extra idle edge for awaiting
   the clock."

Neil


> -------- Original Message --------
> Subject: [sv-ac] RE: review 1681 (global clocking)
> Date: Tue, 26 Jun 2007 14:10:50 +0300
> From: Korchemny, Dmitry <dmitry.korchemny@intel.com>
> To: Doron Bustan <dbustan@freescale.com>, Eduard Cerny
<Eduard.Cerny@synopsys.com>
> CC: sv-ac@eda.org
> 
> Hi all,
> 
> I updated the document (attached here for convenience) according to
> Doron's comments and adjusted the numeration according to the Draft
D3a.
> 
> See my comments in the original mail body below.
> 
> Thanks,
> Dmitry
> 

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.