Generate your way through the Verification quagmire

Discussion in 'VHDL' started by paddy3118@netscape.net, Jan 29, 2006.

  1. Guest

    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.
    , Jan 29, 2006
    #1
    1. Advertising

  2. wrote:
    > 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
    Mike Treseler, Jan 29, 2006
    #2
    1. Advertising

  3. Guest

    Mike wrote:
    > 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.
    , Jan 29, 2006
    #3
  4. Paul Johnson Guest

    On 29 Jan 2006 03:50:08 -0800, wrote:

    >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
    Paul Johnson, Jan 29, 2006
    #4
  5. Guest

    On: Sun, 29 Jan 2006 22:06:04 Paul Johnson wrote:

    > On 29 Jan 2006 03:50:08 -0800, wrote:
    >
    > >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.


    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?

    >
    > >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.


    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?

    >
    > >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.


    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.
    , Jan 30, 2006
    #5
  6. wrote:

    > 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
    Mike Treseler, Jan 30, 2006
    #6
    1. Advertising

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

It takes just 2 minutes to sign up (and it's free!). Just click the sign up button to choose a username and then you can ask your own questions on the forum.
Similar Threads
  1. Weng Tianxiang
    Replies:
    5
    Views:
    1,298
    Christophe
    Feb 16, 2006
  2. Replies:
    1
    Views:
    271
  3. Paul Rubin
    Replies:
    5
    Views:
    408
    Hendrik van Rooyen
    Aug 6, 2009
  4. wrytat

    Two Way Handshake Verification

    wrytat, Apr 14, 2005, in forum: ASP .Net Security
    Replies:
    0
    Views:
    183
    wrytat
    Apr 14, 2005
  5. py
    Replies:
    1
    Views:
    333
Loading...

Share This Page