Re: [sv-ac] P1800-2009 : Bad example in 16.14.2 Multiclocked properties

Ed,
You're correct .  The intersect in the other example  is the sequence
operator.
Thanks,
Ben


On 3/6/09, Eduard Cerny <Eduard.Cerny@synopsys.com> wrote:
>
>  Ben, I do not see anything wrong with
>
> @(posedge clk0) s0 |=> *(@(posedge clk1) s1) and (@(posedge clk2) s2)*
>
> This is a property “and” operator, and the property is legal.
>
>
>
> ed
>
>
>
>
>
> *From:* owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] *On Behalf Of *ben
> cohen
> *Sent:* Thursday, March 05, 2009 11:20 PM
> *To:* sv-ac@eda.org
> *Subject:* [sv-ac] P1800-2009 : Bad example in 16.14.2 Multiclocked
> properties
>
>
>
> page 378  shows:  The following example shows a combination of differently
> clocked properties using both implication and
>
> boolean property operators:
>
> @(posedge clk0) s0 |=> *(@(posedge clk1) s1) and (@(posedge clk2) s2)*
>
>
>
> The sequence "*(@(posedge clk1) s1) and (@(posedge clk2) s2)" *is illegal
> per Page 377: *Differently clocked or multiclocked sequence operands
> cannot be combined with any sequence operators*
>
> *other than ##1 and ##0.* For example, if clk1 and clk2 are not identical,
> then the* following are illegal:*
>
> @(posedge clk1) s1 ##2 @(posedge clk2) s2
>
> *@(posedge clk1) s1 intersect @(posedge clk2) s2*
>
>
>
> I suggest that the example be changed to:
>
> @(posedge clk0) s0 |=> *(@(posedge clk1) s1) ##1 (@(posedge clk2) s2)*
>
>
> --
> This message has been scanned for viruses and
> dangerous content by *MailScanner* <http://www.mailscanner.info/>, and is
> believed to be clean.
>

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