PSL stmts in VHDL: how to describe asynchronous dependencies?

Hi,

could someone post some piece of code illustrating the use of the PSL
syntax to describe asynchronous dependencies between signals? Any
attempt to describe async. dependencies and to veriy the assertions w/
ModelSim failed miserabely w/ the comment that the clock was missing.

Eric

Eric DELAGE

On Tue, 05 Apr 2005 18:10:32 +0200, Eric DELAGE <"eric UNDERSCORE
delage AT yahoo DOT fr"> wrote:

>could someone post some piece of code illustrating the use of the PSL
>syntax to describe asynchronous dependencies between signals? Any
>attempt to describe async. dependencies and to veriy the assertions w/
>ModelSim failed miserabely w/ the comment that the clock was missing.

PSL properties must be sampled.

Unclocked properties are, in principle, sampled every time the
simulator wakes up - i.e. every active delta. This is of course
impractical. Consequently, all the tools I'm aware of simply
forbid unclocked properties.

You can, of course, have multiple-clocked properties to
represent behaviours that cover more than one clock domain.
--
Jonathan Bromley, Consultant

DOULOS - Developing Design Know-how
VHDL, Verilog, SystemC, Perl, Tcl/Tk, Verification, Project Services

Doulos Ltd. Church Hatch, 22 Market Place, Ringwood, BH24 1AW, UK
Tel: +44 (0)1425 471223 mail:
Fax: +44 (0)1425 471573 Web: http://www.doulos.com

The contents of this message may contain personal views which
are not the views of Doulos Ltd., unless specifically stated.

Jonathan Bromley

I believe modelsim still dosent support unclocked properties.

Neo