RE: [sv-ac] Sampled value functions

I agree with Doron's comment that it looks unintuitive that 'a' is
sampled based on c2. If the intention is really to sample 'a' at c2, why
not write the assertion outside.

Thanks.
Manisha
 
[Ed Cerny]

With regards to that, I think that the interpretation is that the normal
clock flow would still keep c2 as the clock of the property and the
condition a would be (syntactically) extracted and inserted in the
assertion. The effective code after extraction would look like this:

always @(c1) begin
end

assert property (@(c2) a |-> b);



>[Korchemny, Dmitry]
>It is a matter of definition. Since we don't allow clock change within 
>the overlapping implication, we have to define it as a standalone 
>assertion assert property (@(c2) a |-> b);
>
>  
>
It looks like I am in a minority here. It looks un intuitive to me that
"a" is sampled according to c2. I would like it to be

assert property (@(c2) a |-> b); 

if c1 and c2 are syntactically the same, and 

assert property (@(c1) a |=> @(c2)b);

otherwise


Doron