Generate your way through the Verification quagmire

P

paddy3118

Does anyone write 'generatable IP' e.g. n-bit UARTS then verify the
UART for small values of n; but more thoroughly, then instantiate a
version of the IP with a much larger version of n?

I would like to start a discussion on if this might ease the
Verification bottleneck that we have at present.

I expand on the idea here:
http://paddy3118.blogspot.com/

Thanks, Paddy.
 
M

Mike Treseler

Does anyone write 'generatable IP' e.g. n-bit UARTS then verify the
UART for small values of n; but more thoroughly, then instantiate a
version of the IP with a much larger version of n?

The reference design here:
http://home.comcast.net/~mike_treseler/
just happens to be uart with character length
set by the generic constant char_len_c.

See also the procedural component RETIME in the same file.

-- Mike Treseler
 
P

paddy3118

Mike said:
The reference design here:
http://home.comcast.net/~mike_treseler/
just happens to be uart with character length
set by the generic constant char_len_c.

Mike,
To verify your block using my methodology, I would change your
testbench test_uart.vhd to bring the generic char_len_c to its top, and
make appropriate changes to any internal constants etc.
With this, or another testbench I would then define functional coverage
points and try and achieve a very high functional coverage but with say
a char_len_c of 2 or 1. The big question would then be if high
functional coverage of the smaller design would equate to high
'quality' of any generatable variant, or not.

- Paddy.
 
P

Paul Johnson

Does anyone write 'generatable IP' e.g. n-bit UARTS then verify the
UART for small values of n; but more thoroughly, then instantiate a
version of the IP with a much larger version of n?

I would like to start a discussion on if this might ease the
Verification bottleneck that we have at present.

I expand on the idea here:
http://paddy3118.blogspot.com/

After 5 minutes of half-baked thought :)

I haven't heard of anyone doing this. The problem is too complex to
think of in generalities. You need specific examples of IP which might
benefit from this. I suspect that there are few.
It is very hard to verify todays chip designs, but they are already quite regular.

The regular designs aren't the problem. But how many designs are
'regular' anyway? None that I deal with; they're all fiendishly
complex.
If the design of the UART has no 'corner cases' for increasing values of n, i.e. the internal architectural algorithm doesn't change for increasing n,

How do you prove this? Formally, or do you guess? I suspect that the
subset of IP for which is true is small.

This looks like a verification version of a simple proof by induction.
But, for induction, you need 2 steps:

1) 'prove' for case n, which you've discussed

2) prove that a proof for case 'n' also holds for case 'n+1'

For many mathematical problems, step 2 is easy enough. But how do you
do this for a complex real-world circuit? I can see how you might do
this for an adder, for example. But even a multiplier sounds
difficult, and anything more complex could be next to impossible.

Paul
 
P

paddy3118

After 5 minutes of half-baked thought :)

I haven't heard of anyone doing this. The problem is too complex to
think of in generalities. You need specific examples of IP which might
benefit from this. I suspect that there are few.

But hold on, don't a lot of people think of 'control and datapath'
surely
the datapath width in a lot of such IP could be parameterized?
The regular designs aren't the problem. But how many designs are
'regular' anyway? None that I deal with; they're all fiendishly
complex.

But think, how many times when dealing with such complexity do you just
look at the spec and if it says: "handle N things", or "of size M",
just go right ahead and code something that handles the hard coded
sizes of N and M?
Why not code for a generatable range of values for N and M, to include
smaller values of those generics then more thoroughly test the
generatable IP?
How do you prove this? Formally, or do you guess? I suspect that the
subset of IP for which is true is small.

By corner case I mean something like hard coding a switch in the type
of multiplyer when n gets 'large'. I would think that changes of
architecture in the source would be just a matter of knowing when you
are writing it.

I don't expect existing IP to be written this way though. It is an idea
for new IP or for modification of existing IP (maybe).
This looks like a verification version of a simple proof by induction.
But, for induction, you need 2 steps:

1) 'prove' for case n, which you've discussed

2) prove that a proof for case 'n' also holds for case 'n+1'

For many mathematical problems, step 2 is easy enough. But how do you
do this for a complex real-world circuit? I can see how you might do
this for an adder, for example. But even a multiplier sounds
difficult, and anything more complex could be next to impossible.

The pragmatic, engineers version might be:

1) Verify the quality for case n, n+1, n+2...

2) Plot a graph.

3) If it is a straight line and you can afford case N where N > n
... then go ahead and build it :)

- Paddy.
 
M

Mike Treseler

Mike,
To verify your block using my methodology, I would change your
testbench test_uart.vhd to bring the generic char_len_c to its top,

The testbench generics are defaulted,
but you could easily map them per
the design generic map.
I would then define functional coverage
points and try and achieve a very high functional coverage but with say
a char_len_c of 2 or 1. The big question would then be if high
functional coverage of the smaller design would equate to high
'quality' of any generatable variant, or not.

Have at it. Let us know what you find.

-- Mike Treseler
 

Ask a Question

Want to reply to this thread or ask your own question?

You'll need to choose a username for the site, which only take a couple of moments. After that, you can post your question and our members will help you out.

Ask a Question

Members online

Forum statistics

Threads
473,744
Messages
2,569,482
Members
44,901
Latest member
Noble71S45

Latest Threads

Top