SVA property question

I have defined a couple of generic properties to detect fifo overflow
or underflow (see below).

property no_overflow(clock, reset, signal, watermark);
@(posedge clock) disable iff(!reset)
((signal == (watermark-1)) |=> ((signal <= (watermark-1)) &&
(signal > 0)));
endproperty : no_overflow

property no_underflow(clock, reset, signal, watermark);
@(posedge clock) disable iff(!reset)
((signal == 0) |=> ((signal < (watermark-1)) && (signal >= 0)));
endproperty : no_underflow

I use these properties as follows:

assert_ingress_desc_a_fifo_no_ofl:
assert property (no_overflow(clk, ring_rst_n[0],
ingress_desc_fifo_a_usedw, 128));

assert_ingress_desc_a_fifo_no_ufl:
assert property (no_underflow(clk, ring_rst_n[0],
ingress_desc_fifo_a_usedw, 128));

I would like to have one copy of the property definitions located in
one file. It can be one of my existing rtl modules or a separate file
with just the property definitions and I would like to put the
assertions in whichever modules contain fifos. Is there a way to do
this? When I tried putting the definitions in my top level module and
the assertions in a lower level module I got an error message that the
"clk must be explicit".

Thanks.

Brian

 

[Jonathan Bromley]

On Fri, 5 Sep 2008 06:51:46 -0700 (PDT), bmyrick8724@gmail.com wrote:

I have defined a couple of generic properties
[...]
property no_overflow(clock, reset, signal, watermark);
@(posedge clock) disable iff(!reset)
((signal == (watermark-1)) |=> ((signal <= (watermark-1)) &&
(signal > 0)));
endproperty : no_overflow

[...]

I use these properties as follows:

assert_ingress_desc_a_fifo_no_ofl:
assert property (no_overflow(clk, ring_rst_n[0],
ingress_desc_fifo_a_usedw, 128));

I would like to have one copy of the property definitions located in
one file. It can be one of my existing rtl modules or a separate file
with just the property definitions and I would like to put the
assertions in whichever modules contain fifos. Is there a way to do
this? When I tried putting the definitions in my top level module and
the assertions in a lower level module I got an error message that the
"clk must be explicit".

I need to check the details of what is and isn't
allowed for clocking a property, but what you're doing
looks OK to me. Is it possibly a tool limitation?
Which tool are you using?

Obviously it would be fairly easy to make the clock
part of the assert statement rather than the property,
but that's much less elegant.

Have you tried putting the properties in a package
rather than in a module?

Time for me to go and check the fine print.
Interesting question.
--
Jonathan Bromley, Consultant

DOULOS - Developing Design Know-how
VHDL * Verilog * SystemC * e * Perl * Tcl/Tk * Project Services

Doulos Ltd., 22 Market Place, Ringwood, BH24 1AW, UK
jonathan.bromley@MYCOMPANY.com
http://www.MYCOMPANY.com

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