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.