Re: [sv-ac] Mantis 2168 - Formal semantics for edge-sensitive clocks

Hi Dmitry, John, all,


Is the semantics of 

assert property @(clk) P;

clear from the LRM?

All examples of direct property clocking in the LRM seem to be of the
form @(posedge clk) or @(negedge clk), which seems compatible with a
level sensitive semantics for the clocking expression.

At the moment in our implementation also the clocking in

assert property @(clk) P;

is interpreted as level sensitive, i.e. the property (if it doesn't
contain other clocking) P is updated on every system clock tick when clk
is true.

Is this interpretation wrong in view of the LRM?

Best Regards,

Johan M


On Thu, Nov 01, 2007 at 11:49:21AM +0200, Korchemny, Dmitry wrote:
> Hi all,
> 
>  
> 
> I filed a new mantis item on edge and level sensitive clocks. The
> problem is that in SystemVerilog the clocks are edge sensitive, e.g.,
> @clk means that clk is going to change, while in the formal semantics
> description in Annex F the clocks are level-sensitive and @clk means
> that clk is high. The rules of converting edge sensitive clocks to level
> sensitive clocks are lacking in Annex F, and they are a subject of this
> proposal. Please, have a look.
> 
>  
> 
> Thanks,
> 
> Dmitry
> 
> ---------------------------------------------------------------------
> Intel Israel (74) Limited
> 
> This e-mail and any attachments may contain confidential material for
> the sole use of the intended recipient(s). Any review or distribution
> by others is strictly prohibited. If you are not the intended
> recipient, please contact the sender and delete all copies.
> 
> -- 
> This message has been scanned for viruses and
> dangerous content by MailScanner, and is
> believed to be clean.
> 



-- 
------------------------------------------------------------
Johan Mårtensson                 Office: +46 31 7451913
Jasper Design Automation         Mobile: +46 703749681 
Arvid Hedvalls backe 4           Fax: +46 31 7451939
411 33 Gothenburg, Sweden        Skype ID: johanmartensson
------------------------------------------------------------

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.