RE: [sv-ac] RE: 1683

Hi Yaniv,

 

Please, see my comments.

 

Thanks,

Dmitry

 

________________________________

From: Fais Yaniv [mailto:yaniv.fais@freescale.com] 
Sent: Tuesday, December 04, 2007 7:56 PM
To: Korchemny, Dmitry; sv-ac@eda.org
Subject: RE: [sv-ac] RE: 1683

 

 

Hi Dmitry,

 

I have reviewed this again and found some other places in section
16.15.1 which should also be changed,

 

this section in page 376 (draft 4) should also be removed:

 

The rules for using multiclocked overlapping implication and if/if-else
in the presence of an incoming

outer clock can now be stated more precisely.

a) Multiclocked overlapping implication.

Let c be the incoming outer clock. Then the clocking of m |-> q is
equivalent to the clocking of

@(c) m |-> q

In the presence of the incoming outer clock, m has a well-defined ending
clock, and there is a welldefined

clock that flows across |->. The multiclocked overlapped implication m
|-> q is legal for

incoming clock c if, and only if, the following two conditions are met:

1) Every explicit semantic leading clock of q is identical to the ending
clock of m.

2) If inherited is a semantic leading clock of q, then the ending clock
of m is equal to the clock

that flows across |->.

For example:

@(c) s |-> p1 or @(c2) p2

is not legal because the ending clock of the antecedent is c, while the
consequent has c2 as an

explicit semantic leading clock.

Also,

@(c) s ##1 (@(c1) s1) |-> p

is not legal because the set of semantic leading clocks of p is
{inherited}, the ending clock of the

antecedent is c1, and the clock that flows across |-> and is inherited
by p is c.

On the other hand,

@(c) s |-> p1 or @(c) p2

and

@(c) s ##1 @(c1) s1 |-> p1 or @(c1) p2

 both legal.

The boolean condition b is clocked by c; therefore, the multiclocked
if/if-else if (b) q1

[ else q2 ] is legal for incoming clock c if, and only if, the following
condition is met:

- Every explicit semantic leading clock of q1 [ or q2 ] is identical to
c.

For example:

@(c) if (b) p1 else @(c) p2

is legal, but

@(c) if (b) @(c) (p1 and @(c2) p2)

is not.

[Korchemny, Dmitry] This section has already been removed from the
proposal. There is the following statement at the end of my proposal:

DELETE from "The rules for using multiclocked overlapping implication
and if/if-else in the presence of an incoming outer clock can now be
stated more precisely." until the end of the subclause.

I'm also not sure but I think the section which defines the semantic
leading clock of sequences and properties (page 375) :

A multiclocked sequence has a unique semantic leading clock, defined
inductively as follows:

...

The set of semantic leading clocks of a multiclocked property is defined
inductively as follows:

...

 

is not needed anymore since it was only used for the previous
restrictions, it is not necessarily bad to keep it.

[Korchemny, Dmitry] John mentioned several reasons why to keep the
semantic leading clock definition. I remember exactly the following one:
the semantic leading clock is used in the definition of local variable
initialization (Mantis 1668). We could discuss this issue with John. 

Regards,

Yaniv

 

________________________________

From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of
Korchemny, Dmitry
Sent: Monday, December 03, 2007 18:17
To: Bustan, Doron; sv-ac@eda.org
Subject: [sv-ac] RE: 1683

HI Doron,

 

Please, see my comments below. I am attaching a new version (also
uploaded into Mantis).

 

Thanks,

Dmitry

 

________________________________

From: Bustan, Doron 
Sent: Wednesday, November 28, 2007 4:51 PM
To: sv-ac@eda.org; Korchemny, Dmitry
Subject: 1683

 

I have reviewed 1683. Here are my remarks:

 

*	End of page 2, 

 

       "The zero delay indicated by ##0 is understood to be from the end
point of the first sequence, 

         which occurs at a tick of the first clock, to the nearest,
non-strictly subsequent tick of the second 

         clock, where the second sequence begins."

   

         I would replace  "non-strictly" by "possibly overlapping".

[Korchemny, Dmitry] I rewrote it as: "... occurs at a tick of the first
clock, to the nearest, possibly overlapping tick of the second 

         clock..." (deleted "subsequent" as well). Made this change in
all similar cases.

 

*	At the end og page 3, I would add: 

 

                If clk1 and clk2 are not identical, then the sequence

                @(posedge clk0) sig0 ##1 @(posedge clk1) sig1[*0:1]

                is illegal because of the possibility of an empty match
of sig1[*0:1], which would make ambiguous

whether the ending clocking event is @(posedge clk0) or @(posedge clk1).
Like in a singly clocked sequence, the operands of ##0 shall not admit
empty matches. 

 

[Korchemny, Dmitry] In singly clocked sequences the operands of ##0 may
admit empty matches, e.g., a[*0:2] ##0 b[*0:2] is legal and it is
equivalent to a[*1:2] ##0 b[*1:2]. As for the multiclocked sequences
there is already a sentence in the original text: "When concatenating
differently clocked sequences, the maximal singly clocked subsequences
are required to admit only nonempty matches."

 

*	Need to modify 16.15.1 (a lot of work) 

[Korchemny, Dmitry] Done.

 

Doron

---------------------------------------------------------------------
Intel Israel (74) Limited
 
This e-mail and any attachments may contain confidential material for
the sole use of the intended recipient(s). Any review or distribution
by others is strictly prohibited. If you are not the intended
recipient, please contact the sender and delete all copies.


-- 
This message has been scanned for viruses and 
dangerous content by MailScanner <http://www.mailscanner.info/> , and is

believed to be clean. 

---------------------------------------------------------------------
Intel Israel (74) Limited

This e-mail and any attachments may contain confidential material for
the sole use of the intended recipient(s). Any review or distribution
by others is strictly prohibited. If you are not the intended
recipient, please contact the sender and delete all copies.

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