Re: [sv-ac] Sampled value functions

>I am not sure that it is clear when an evaluation attempt should occur. 
>For example
>
>always @(c1) begin
>if (a) assert property (@(c2) b);
>end
>
>Now, suppose that c2 is 3 times faster than c1, and that in the first 
>occurrence of c1, "a" holds.
>should there be 3 attempts of "b"? or just one ?
>Should "a" be evaluated according to c2, and c1 should be ignored?
>
>  
>
[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