PSL syntax help

[niv]

Hi, I'm trying to get a PSL vunit to work, but having some trouble (as usual)!
(I'm using Modelsim 10.1d)

The vunit is as follows:


vunit interface_check (iface(struct))

{
default clock is clk;

assert never {wren AND fifo_full}; -- works OK.
assert never {rden AND fifo_empty}; -- works OK.

assert always (req -> next[2](gnt)); -- works OK.
assert always (req -> next[3](gnt)); -- works OK.
assert always (req -> next[4](gnt)); -- works OK.
assert always (req -> next[5](gnt)); -- works OK.

-- BUT, I should be able to replace above 4 lines with something like:

assert always (req -> next[*2..5](gnt)); -- which does not compile.

-- OR

assert always (req -> next[*2:5](gnt)); -- which does not compile.

}


Could someone please explain what I'm doing wrong?
I've tried all sorts of minor variations, but can't get the composite assertion to compile.

Regards, Niv.

 

[niv]

Figured out I was using the Verilog syntax...
[*2..5] should be [*2 to 5] for VHDL. (Doh!)

However, I get assertion fails with:

assert always (req -> next[*2 to 5](gnt)); -- compiles OK but gets assertion error

or even with:

assert always (req -> next gnt[*2 to 5]);

Not sure which is the correct syntax for what I need to combine the 4 working assertions into a single one??

Any help most welcome.

 

[niv]

assert always (req -> next_a[2 to 5](gnt));

This does thejob. (Phew)!