[sv-ac] Issue #1296

Hi all,

 

If I understand the attached document correctly, it says (among the
other) that the antecedent and the consequent of a property may have
different clocks. I.e.,

@(clk1) A |->@(clk2) B

is legal for any clk1 and clk2. And the meaning of this formula is: at
the moment of the tight satisfaction of A wait for the nearest tick of
clk2 (this includes the case when clk2 ticks at the same time as clk1)
and then check B controlled by clk2.

 

I definitely support this approach since it eliminates a redundant
restriction on the consequent clock and makes property semantics
cleaner. But there are several sentences in the LRM that should be fixed
accordingly. E.g. Section 17.12.2:

 

---

Because |-> overlaps the end of its antecedent with the beginning of its
consequent, the clock for the end of the antecedent must be the same as
the clock for the beginning of the consequent. For example, if clk0 and
clk1 are not identical and s0, s1, and s2 are sequences with no clocking
events, then

@(posedge clk0) s0 |-> @(posedge clk1) s1 ##1 @(posedge clk2) s2

is illegal, but

@(posedge clk0) s0 |-> @(posedge clk0) s1 ##1 @(posedge clk2) s2

is legal.

---

 

Thanks,

Dmitry