RE: [sv-ac] Sampled value functions

I think the main use of such "change of clock" can be in instrumenting
certain styles of RTL coding. For example:

always @(posedge clk)
  if (!rst)
    state <= start_value;
else
    state <= nstate;
// The next state value is computed in a combinational always block. For
example,
always_comb
  if (x) 
    nstate = v1;
  else 
    nstate = v2;

In such a style, it would be natural to isnert asserstion inside the
combinational block and have them sampled by posedge clk. That is, e.g.,

always_comb
  if (x) begin
    nstate = v1;
    aa: assert property (@(posedge clk) bool_fn(nstate, state, etc...));
  end
  else 
    nstate = v2;

----
ed

> -----Original Message-----
> From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On 
> Behalf Of Doron Bustan
> Sent: Wednesday, May 10, 2006 8:26 AM
> To: Korchemny, Dmitry
> Cc: sv-ac@eda.org
> Subject: 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
> 
>