SystemVerilog Sequence Coverage Problem?

[Shenli]

Hi all,

I am reading some FIFO code by SystemVerilog. But there is a part of
code confused me. It seems to count push and pop pair appear times.

But if I have "push1 -> push2 -> pop1 -> pop2", coverage result will
give out 4 times or only 2 times theoretically? And why count this
number?

//--- Code start
property p_push_pop_sequencing;
@ (posedge clk) fifo_if.push |=> ##[0:$] fifo_if.pop;
endproperty : p_push_pop_sequencing

// coverage of sequences
cp_push_pop_sequencing : cover property (p_push_pop_sequencing);
//--- Code end

Any suggestions are welcome!
Best regards,
Shenli

 

[Jonathan Bromley]

On 26 Dec 2006 21:38:48 -0800, "Shenli" <zhushenli@gmail.com> wrote:

I am reading some FIFO code by SystemVerilog. But there is a part of
code confused me. It seems to count push and pop pair appear times.

But if I have "push1 -> push2 -> pop1 -> pop2", coverage result will
give out 4 times or only 2 times theoretically? And why count this
number?

//--- Code start
property p_push_pop_sequencing;
@ (posedge clk) fifo_if.push |=> ##[0:$] fifo_if.pop;
endproperty : p_push_pop_sequencing

This property is not very useful, is it?

If you can have overlapping push/pop, like your example
push1 -> push2 -> pop1 -> pop2
then the property will fire twice - once for "push1" and once
for "push2" - but both executions of the property are satisfied
by "pop1". So (as I understand it) you will see two coverage
hits:

push1 -> pop1
push2 -> pop1

Iit's clear that the second hit is NOT correct! Somehow we
must modify the property so that it keeps track of which push
is associated with which pop. Typically we do this with some
piece of auxiliary code that maintains two variables, a push count
and a pop count...

int push_count, pop_count;
always @(posedge clk) begin
if (fifo_if.push) push_count++;
if (fifo_if.pop) pop_count++;
end

And then we modify the property so it makes use of the count
values, and requires that each push has a MATCHING pop:

property JB_push_pop_sequencing;
int count;
@(posedge clk)
(fifo_if.push, count=push_count)
|=>
##[0:$] (fifo_if.pop && (count==pop_count));
endproperty

(NOTE: This is approximately right, but it will probably need
modification to take account of resetting the FIFO, and other
factors.)

You can now enjoy yourself adding assertions to check that
each pop operation must have a previous matching push,
and other useful tests.
--
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.

 

[Shenli]

Hi Jonathan,

Happy New Year! And thanks a lot for the assertion suggestion.

Best regards,
Shenli

Jonathan Bromley wrote:

On 26 Dec 2006 21:38:48 -0800, "Shenli" <zhushenli@gmail.com> wrote:

I am reading some FIFO code by SystemVerilog. But there is a part of
code confused me. It seems to count push and pop pair appear times.

But if I have "push1 -> push2 -> pop1 -> pop2", coverage result will
give out 4 times or only 2 times theoretically? And why count this
number?

//--- Code start
property p_push_pop_sequencing;
@ (posedge clk) fifo_if.push |=> ##[0:$] fifo_if.pop;
endproperty : p_push_pop_sequencing

This property is not very useful, is it?

If you can have overlapping push/pop, like your example
push1 -> push2 -> pop1 -> pop2
then the property will fire twice - once for "push1" and once
for "push2" - but both executions of the property are satisfied
by "pop1". So (as I understand it) you will see two coverage
hits:

push1 -> pop1
push2 -> pop1

Iit's clear that the second hit is NOT correct! Somehow we
must modify the property so that it keeps track of which push
is associated with which pop. Typically we do this with some
piece of auxiliary code that maintains two variables, a push count
and a pop count...

int push_count, pop_count;
always @(posedge clk) begin
if (fifo_if.push) push_count++;
if (fifo_if.pop) pop_count++;
end

And then we modify the property so it makes use of the count
values, and requires that each push has a MATCHING pop:

property JB_push_pop_sequencing;
int count;
@(posedge clk)
(fifo_if.push, count=push_count)
|=
##[0:$] (fifo_if.pop && (count==pop_count));
endproperty

(NOTE: This is approximately right, but it will probably need
modification to take account of resetting the FIFO, and other
factors.)

You can now enjoy yourself adding assertions to check that
each pop operation must have a previous matching push,
and other useful tests.
--
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.