[sv-ac] Re: [sv-sc] Re: ConcurrentAssertNewProposal

From: Gordon Vreugdenhil <gordonv_at_.....>
Date: Mon May 05 2008 - 13:48:18 PDT
Lisa Piper wrote:
> 
> 
> Another question. In the example provided, do the variables in r3 impact
> when the "always @(*)" process is executed?  


For @(*) I think the answer is pretty clearly "no" unless you want to
appeal to the inlining as a real effect rather than a conceptual one.

For always_comb the answer would also currently be "no" since it only
includes functions and not assertions.

In addition, since the values being "read" are the sampled values,
what would it mean to have *event* sensitivity?  An event on the
change in the sampled value from one clock to the next?  How would
that work with the rest of the process semantics?

Does going down that path even really make sense?

For both "always @(*)" and always_comb, for real designs I hope the
real answer would be "it doesn't matter" since if it did matter, that
would imply that the existence of events on values the *assertion* reads
have an impact on the real design behavior.

Gord



> 
> Lisa
> 
> 
>> property r3;
>>          @(posedge mclk)(q != d);
>>      endproperty
>>
>> always @(*)
>>   begin
>>   if (a)
>>     begin
>>     d2 = d1;
>>     assert property (r3);
>>     ...
>>     end
>>   end
> 
> 
> 
> -----Original Message-----
> From: owner-sv-sc@eda.org [mailto:owner-sv-sc@eda.org] On Behalf Of
> Seligman, Erik
> Sent: Monday, May 05, 2008 4:29 PM
> To: Gordon Vreugdenhil; Adam Krolnik
> Cc: sv-sc@eda.org; sv-ac@eda.org
> Subject: RE: [sv-sc] Re: ConcurrentAssertNewProposal
> 
> 
> Don't forget that we may see this code in a module that has default
> clocking defined-- so in that case, I think Adam's code would be fine.
> (Not to mention the fact that with the new procedural triggering method,
> we may want to relax the requirement that concurrent asserts need a
> triggering clock.)   So I think he's right, we need to think about this
> situation. 
> 
> In our verbal discussions last week, I believe we briefly suggested
> treating concurrent asserts in multiply-trigggered procedures like the
> new deferred assertions (see proposal 2005):  if the same procedure is
> triggered again in the same time step, it flushes any current
> triggerings of assertions in that procedure.
> 
> 
> -----Original Message-----
> From: owner-sv-sc@server.eda.org [mailto:owner-sv-sc@server.eda.org] On
> Behalf Of Gordon Vreugdenhil
> Sent: Monday, May 05, 2008 1:18 PM
> To: Adam Krolnik
> Cc: sv-sc@server.eda.org; sv-ac@server.eda.org
> Subject: Re: [sv-sc] Re: ConcurrentAssertNewProposal
> 
> Adam,
> 
> Is this actually legal code as is?  I thought that the clock inference
> rules of 16.14.5 (P1800 Draft 5) would make this illegal since there is
> no "clock" event control on the always block.
> 
> Gord.
> 
> 
> 
> Adam Krolnik wrote:
>> Good morning;
>>
>> As part of this discussion, don't forget assertions in combinatorial 
>> procedural logic. E.g.
>>
>> property r3;
>>          @(posedge mclk)(q != d);
>>      endproperty
>>
>> always @(*)
>>   begin
>>   if (a)
>>     begin
>>     d2 = d1;
>>     assert property (r3);
>>     ...
>>     end
>>   end
>>
>> Since the process above may run more than once, the assertion may need
> 
>> to be stopped due to the presence of new values that cause it to no
> longer be triggered.
>>
>>
>>   Thanks.
>>
>> -- 
>>     Soli Deo Gloria
>>     Adam Krolnik
>>     Director of Design Verification
>>     VeriSilicon Inc.
>>     Plano TX. 75074
>>     Co-author "Assertion-Based Design", "Creating Assertion-Based IP"
>>
>>
>> --
>> This message has been scanned for viruses and dangerous content by 
>> *MailScanner* <http://www.mailscanner.info/>, and is believed to be 
>> clean.
> 
> --
> --------------------------------------------------------------------
> Gordon Vreugdenhil                                503-685-0808
> Model Technology (Mentor Graphics)                gordonv@model.com
> 
> 

-- 
--------------------------------------------------------------------
Gordon Vreugdenhil                                503-685-0808
Model Technology (Mentor Graphics)                gordonv@model.com


-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.
Received on Mon May 5 13:48:56 2008

This archive was generated by hypermail 2.1.8 : Mon May 05 2008 - 13:49:06 PDT