SVA : How to call a function ?

[RSGUPTA]

Hello,
I wanted to know how to call a function from property:
For Example if i have a function as described below:

// Function to calculate the next address for a burst transfers.

function logic [31:0] next_addr (logic [31:0] burst_addr);

case (HSIZE)

BYTE : return burst_haddr+1;
HALFWORD : return burst_haddr+2;
WORD : return burst_haddr+4;

endcase

endfunction // next_addr

How can call this function in a property?
Else someone can give me a simple example to demonstrate a function
call.

Thanks.

 

[Jonathan Bromley]

On Thu, 22 Jan 2009 00:25:32 -0800 (PST), RSGUPTA
<rsgupta.gupta@gmail.com> wrote:

Hello,
I wanted to know how to call a function from property:
For Example if i have a function as described below:

// Function to calculate the next address for a burst transfers.

function logic [31:0] next_addr (logic [31:0] burst_addr);

case (HSIZE)

BYTE : return burst_haddr+1;
HALFWORD : return burst_haddr+2;
WORD : return burst_haddr+4;

endcase

endfunction // next_addr

How can call this function in a property?

I guess you're using this function to compute, from
one beat's address, the expected address of the next
beat of the burst.

What do you plan to do with the function's return value?
If you call the function from within a property, the only
reasonable thing to do with its result is to put it into
a local variable of the property. I don't have the AHB
spec to hand so the protocol will be wrong here, but
I hope this will give the right idea:

property correct_incrementing addresses;

// Local variable of the property, to hold
// the expected next-beat address:
bit unsigned [31:0] next_beat_addr;

// The burst begins when something happens...
starting_condition |->

// on the first beat, capture the start address...
(hvalid, next_beat_addr = next_addr(haddr)) ##1

// and on future beats, expect the correct address:
(hvalid && (haddr == next_beat_addr),
next_beat_addr = next_addr(haddr)) [*NUM_BEATS-1];

endproperty

You can see that I'm assuming each beat takes only one clock;
of course that will be wrong.

The point is that at any step of a sequence or property,
you can take that step's Boolean condition and add a
"sequence_match_item":

##1 condition ##1 // condition matches at that step

##1 (condition, ACTION) ##1 // at the end of the step when
// condition matches, do ACTION

There are some limits on what you can do for ACTION:
you can assign to a property local variable, you can
increment or decrement a property local variable using ++ or --,
or you can call a task or void function.
--
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.