[sv-ac] RE: 1683

Hi Doron,

 

Please, see my comments below. I uploaded an updated version to Mantis.

 

Thanks,

Dmitry

 

________________________________

From: Bustan, Doron 
Sent: Wednesday, December 05, 2007 10:42 AM
To: Korchemny, Dmitry
Cc: sv-ac@eda.org
Subject: 1683

 

Hi Dmitry,

 

More comments:

 

*	I would rewrite this

           "This subclause defines a notion of the set of semantic
leading clocks for 

                 a multiclocked sequence or property."

 

      With

 

           This subclause gives a more precise treatment of the
restrictions of a unique leading clock. The present treatment depends on
the notion of the set of semantic

        leading clocks for a multiclocked sequence or property.

 

[Korchemny, Dmitry] Having a unique semantic leading clock is not the
only purpose of this subclause. E.g., Mantis 1668 (Local variable
initialization) also requires a definition of the leading clock.

 

*	I think that the last part of 16.15.1 starting 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."

 

                Should be removed

 

[Korchemny, Dmitry] There is a note to delete this text in the proposal.
See my answer to Yaniv.

 

*	I would add a sentence saying what does it mean that the top
level property has a unique leading clock. Without

such description, 16.15.1 does not have a purpose. This is not entirely
trivial, because you may have a set of two

leading clocks when one of them is inherited. In this case the inferred
clock must be equal to the other clock in the set.

 

[Korchemny, Dmitry] I added the following text at the end of the
subclause:

 

INSERT at the end of the subclause.

A multiclocked property has a unique semantic leading clock in case when
all its leading clocks are identical. Consider the following example:

wire clk1, clk2;

logic a, b;

...

assign clk2 = clk1;

a1: assert property (@(clk1) a and @(clk2) b); // Illegal

a2: assert property (@(clk1) a and @(clk1) b); // OK

always @(posedge clk1) begin

   a3: assert property(a and @(posedge clk2)); //Illegal

   a4: assert property(a and @(posedge clk1)); // OK

end

The assertions a2 and a4 are legal, while the assertions a1 and a3 are
not. Though both clocks of a1 have the same value, they are not
identical, therefore a1 does not have a unique semantic leading clock.
The assertions a3 and a4 have @(posedge clk1) as their inferred clock.
This clock is not identical to @(posedge clk2) therefore a3 does not
have a unique semantic leading clock.

 

Will it do?

 

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, and is
believed to be clean.