Verification Question

Discussion in 'VHDL' started by Shannon, Sep 18, 2009.

  1. Shannon

    Shannon Guest

    I have the following generate loop:

    SERDES_Scramble :
    for i in 0 to (BUS_WIDTH -1) generate
    begin
    aligned_data(i) <= data((i/DES_FACT) + ((i mod DES_FACT)*NUM_CHAN));
    end generate SERDES_Scramble;

    So for a deserialization factor of 4 and 16 channels (BUS_WIDTH = 64)
    this should produce:

    aligned_data(0) <= data(0);
    aligned_data(1) <= data(16);
    aligned_data(2) <= data(32);
    aligned_data(3) <= data(48);

    aligned_data(4) <= data(1);
    aligned_data(5) <= data(17);
    aligned_data(6) <= data(33);
    aligned_data(7) <= data(49);

    .....

    aligned_data(60) <= data(15);
    aligned_data(61) <= data(61);
    aligned_data(62) <= data(62);
    aligned_data(63) <= data(63);

    I believe this works but how do I verify it strictly? The RTL viewer
    in Quartus creates busses for things like this and I can't see the one
    to one connections.
     
    Shannon, Sep 18, 2009
    #1
    1. Advertising

  2. Shannon

    sleeman Guest

    On Sep 18, 11:25 am, Shannon <> wrote:
    > I have the following generate loop:
    >
    > SERDES_Scramble :
    > for i in 0 to (BUS_WIDTH -1) generate
    > begin
    >         aligned_data(i) <= data((i/DES_FACT) + ((i mod DES_FACT)*NUM_CHAN));
    > end generate SERDES_Scramble;
    >
    > So for a deserialization factor of 4 and 16 channels (BUS_WIDTH = 64)
    > this should produce:
    >
    > aligned_data(0) <= data(0);
    > aligned_data(1) <= data(16);
    > aligned_data(2) <= data(32);
    > aligned_data(3) <= data(48);
    >
    > aligned_data(4) <= data(1);
    > aligned_data(5) <= data(17);
    > aligned_data(6) <= data(33);
    > aligned_data(7) <= data(49);
    >
    > ....
    >
    > aligned_data(60) <= data(15);
    > aligned_data(61) <= data(61);
    > aligned_data(62) <= data(62);
    > aligned_data(63) <= data(63);
    >
    > I believe this works but how do I verify it strictly?  The RTL viewer
    > in Quartus creates busses for things like this and I can't see the one
    > to one connections.


    A couple of things pop into mind off the bat (And please excuse the
    obvious syntax fragmentation and probable typos in advance :):

    (option 1)

    Execute the code in the simulator: write a separate process for
    simulation only (hidden by a synthesis translate off pragma, or inside
    an IF..GENERATE block). Inside this process, write the same code as
    above but print out your mapping explicitly:

    process
    for i in to (BUS_WIDTH -1) loop
    report "aligned(" & integer'image(i) & ") <= data(" &
    integer'image((i/DES_FACT) + ((i mod DES_FACT)*NUM_CHAN))
    & ");"
    end loop;
    wait;
    end process;


    Of course, this only tells you your simulator is right, it doesn't
    tell you that synth matches your sims.

    (option 2)

    In synthesis, write a 64 bit bitmask, initialized to zero. Inside the
    generation loop, set each destination bit as you go through the loop,
    then check that the entire vector is all ones after the loop is done.
    This should be an invariant, so should synthesie out trivially, but if
    your logic is wrong you'll double-point to the same bit twice so
    you'll leave some bits empty (pigeon-hole principle).

    The key idea is that your transform is strictly a *permutation* so
    that you guarantee all 64 bits will be covered exactly once.

    bitmask : std_ulogic_vector(0 to BUS_WiDTH-1) := (others => '0');

    SERDES_Scramble :
    for i in 0 to (BUS_WIDTH -1) generate
    begin
    aligned_data(i) <= data((i/DES_FACT) + ((i mod DES_FACT)
    *NUM_CHAN));
    bitmask((i/DES_FACT) + ((i mod DES_FACT)*NUM_CHAN)) <= '1';
    end generate SERDES_Scramble;

    process(clk)
    begin
    assert (bitmask = (others => '1')) report "oops" severity FAILURE;
    end process;

    ...or equivalently drive a port on the module with the same error
    condition. You should be able to get the synthesizer to do this work
    for you.

    Just a few random thoughts, hope they help.

    - Kenn
     
    sleeman, Sep 18, 2009
    #2
    1. Advertising

  3. sleeman <> writes:

    > On Sep 18, 11:25 am, Shannon <> wrote:
    >> I have the following generate loop:
    >>
    >> SERDES_Scramble :
    >> for i in 0 to (BUS_WIDTH -1) generate
    >> begin
    >>         aligned_data(i) <= data((i/DES_FACT) + ((i mod DES_FACT)*NUM_CHAN));
    >> end generate SERDES_Scramble;
    >>
    >> So for a deserialization factor of 4 and 16 channels (BUS_WIDTH = 64)
    >> this should produce:
    >>
    >> aligned_data(0) <= data(0);
    >> aligned_data(1) <= data(16);
    >> aligned_data(2) <= data(32);
    >> aligned_data(3) <= data(48);
    >>
    >> aligned_data(4) <= data(1);
    >> aligned_data(5) <= data(17);
    >> aligned_data(6) <= data(33);
    >> aligned_data(7) <= data(49);
    >>
    >> ....
    >>
    >> aligned_data(60) <= data(15);
    >> aligned_data(61) <= data(61);
    >> aligned_data(62) <= data(62);
    >> aligned_data(63) <= data(63);
    >>
    >> I believe this works but how do I verify it strictly?  The RTL viewer
    >> in Quartus creates busses for things like this and I can't see the one
    >> to one connections.

    >
    > A couple of things pop into mind off the bat (And please excuse the
    > obvious syntax fragmentation and probable typos in advance :):
    >
    > (option 1)
    >
    > Execute the code in the simulator: write a separate process for
    > simulation only (hidden by a synthesis translate off pragma, or inside
    > an IF..GENERATE block). Inside this process, write the same code as
    > above but print out your mapping explicitly:
    >
    > process
    > for i in to (BUS_WIDTH -1) loop
    > report "aligned(" & integer'image(i) & ") <= data(" &
    > integer'image((i/DES_FACT) + ((i mod DES_FACT)*NUM_CHAN))
    > & ");"
    > end loop;
    > wait;
    > end process;
    >
    >
    > Of course, this only tells you your simulator is right, it doesn't
    > tell you that synth matches your sims.
    >
    > (option 2)
    >
    > In synthesis, write a 64 bit bitmask, initialized to zero. Inside the
    > generation loop, set each destination bit as you go through the loop,
    > then check that the entire vector is all ones after the loop is done.
    > This should be an invariant, so should synthesie out trivially, but if
    > your logic is wrong you'll double-point to the same bit twice so
    > you'll leave some bits empty (pigeon-hole principle).
    >
    > The key idea is that your transform is strictly a *permutation* so
    > that you guarantee all 64 bits will be covered exactly once.
    >
    > bitmask : std_ulogic_vector(0 to BUS_WiDTH-1) := (others => '0');
    >
    > SERDES_Scramble :
    > for i in 0 to (BUS_WIDTH -1) generate
    > begin
    > aligned_data(i) <= data((i/DES_FACT) + ((i mod DES_FACT)
    > *NUM_CHAN));
    > bitmask((i/DES_FACT) + ((i mod DES_FACT)*NUM_CHAN)) <= '1';
    > end generate SERDES_Scramble;
    >
    > process(clk)
    > begin
    > assert (bitmask = (others => '1')) report "oops" severity FAILURE;
    > end process;
    >
    > ..or equivalently drive a port on the module with the same error
    > condition. You should be able to get the synthesizer to do this work
    > for you.
    >
    > Just a few random thoughts, hope they help.
    >
    > - Kenn
    >
    >


    And to make it even more robust, note that you actually have three free
    variables in your code fragment: BUS_WIDTH, DES_FACT, and NUM_CHAN, but
    only two real degrees of freedom (DES_FACT and NUM_CHAN). (Thy're
    presumably GENERICS in VHDL but variables in the mathematical
    sense). Your code implcitly relies on the fact that

    BUS_WIDTH=DES_FACT*NUM_CHAN

    However, you don't assert or verify it. If you want a robust
    paramaterizable solution you should assert this.

    How to verify it "stictly: though is another story... that implies that
    you have a strict spec. If your strict spec is in terms of an equation,
    then you just trace the equation back to VHDL.

    Another way to look at it (although not formal in any sense) is to ask
    yourself if there's another intuitive way to frame the problem so that
    it's consistent with your goal, then see if the two solutions
    match. (The concept of safety through redundancy!)

    Whn you draw out your manual mapping above, it's evident that you're
    just permuting address bits, so that the LHS has index vector iv

    iv(B-1 downto 0),

    while on the RHS you're permuting these to form the address

    iv(B-C-1 downto 0) & iv((B-1) downto (B-C))

    Where for brevity,

    BUS_WIDTH = 2**B; B = 6 here
    NUM_CHAN = 2 ** C; C = 2 here
    iv := to_unsigned(i, B)

    It's clear that by examining the indices that the RHS has the
    appropriate length in bits:

    (B-C) + (C) = B

    Then you could either rewrite your code, or just assert this to be so:

    for i in 0 to (BUS_WIDTH -1) generate
    begin
    aligned_data(i) <= data((i/DES_FACT) + ((i mod DES_FACT)*NUM_CHAN));
    process
    variable iv : unisgned := to_unsigned(i, B)
    begin
    assert (to_integer(iv) = i) report "LHS oops" severity FAILURE;
    assert (to_integer(iv(B-C-1 downto 0) & iv(B-1 downto B-C))
    = ((i/DES_FACT) + ((i mod DES_FACT)*NUM_CHAN)))
    report "RHS oops" severity FAILURE;
    end process;
    end generate SERDES_Scramble;

    Arguably, this is very complex on the surface; this has more to do with
    the fact that it's ugly to express this in VHDL, and little to do with
    the intent.

    As a general principle, if you spend enought time on the problem to get
    at least two methods working, in all their ugly detail, you're probably
    in good shape!

    Of course, the transformation I just described assumes that DES_FACT and
    NUM_CHAN are powers of two, and may have misbehaviour when either is
    zero, so you want to assert that... ad nauseum.

    HTH,

    - Kenn

    --
    ---------------------------------
    Remove NOSPAM from email address.
     
    Kenn Heinrich, Sep 19, 2009
    #3
  4. Shannon

    Shannon Guest

    On Sep 19, 6:50 am, Kenn Heinrich <> wrote:
    > sleeman <> writes:
    > > On Sep 18, 11:25 am, Shannon <> wrote:
    > >> I have the following generate loop:

    >
    > >> SERDES_Scramble :
    > >> for i in 0 to (BUS_WIDTH -1) generate
    > >> begin
    > >>         aligned_data(i) <= data((i/DES_FACT) + ((i mod DES_FACT)*NUM_CHAN));
    > >> end generate SERDES_Scramble;

    >
    > >> So for a deserialization factor of 4 and 16 channels (BUS_WIDTH = 64)
    > >> this should produce:

    >
    > >> aligned_data(0) <= data(0);
    > >> aligned_data(1) <= data(16);
    > >> aligned_data(2) <= data(32);
    > >> aligned_data(3) <= data(48);

    >
    > >> aligned_data(4) <= data(1);
    > >> aligned_data(5) <= data(17);
    > >> aligned_data(6) <= data(33);
    > >> aligned_data(7) <= data(49);

    >
    > >> ....

    >
    > >> aligned_data(60) <= data(15);
    > >> aligned_data(61) <= data(61);
    > >> aligned_data(62) <= data(62);
    > >> aligned_data(63) <= data(63);

    >
    > >> I believe this works but how do I verify it strictly?  The RTL viewer
    > >> in Quartus creates busses for things like this and I can't see the one
    > >> to one connections.

    >
    > > A couple of things pop into mind off the bat (And please excuse the
    > > obvious syntax fragmentation and probable typos in advance :):

    >
    > > (option 1)

    >
    > > Execute the code in the simulator: write a separate process for
    > > simulation only (hidden by a synthesis translate off pragma, or inside
    > > an IF..GENERATE block).  Inside this process, write the same code as
    > > above but print out your mapping explicitly:

    >
    > > process
    > >   for i in  to (BUS_WIDTH -1) loop
    > >     report "aligned(" & integer'image(i) & ") <= data(" &
    > >         integer'image((i/DES_FACT) + ((i mod DES_FACT)*NUM_CHAN))
    > >          & ");"
    > >   end loop;
    > >   wait;
    > > end process;

    >
    > > Of course, this only tells you your simulator is right, it doesn't
    > > tell you that synth matches your sims.

    >
    > > (option 2)

    >
    > > In synthesis, write a 64 bit bitmask, initialized to zero.  Inside the
    > > generation loop, set each destination bit as you go through the loop,
    > > then check that the entire vector is all ones after the loop is done.
    > > This should be an invariant, so should synthesie out trivially, but if
    > > your logic is wrong you'll double-point to the same bit twice so
    > > you'll leave some bits empty (pigeon-hole principle).

    >
    > > The key idea is that your transform is strictly a *permutation* so
    > > that you guarantee all 64 bits will be covered exactly once.

    >
    > > bitmask : std_ulogic_vector(0 to BUS_WiDTH-1) := (others => '0');

    >
    > >  SERDES_Scramble :
    > >  for i in 0 to (BUS_WIDTH -1) generate
    > >  begin
    > >          aligned_data(i) <= data((i/DES_FACT) + ((i mod DES_FACT)
    > > *NUM_CHAN));
    > >          bitmask((i/DES_FACT) + ((i mod DES_FACT)*NUM_CHAN)) <= '1';
    > >  end generate SERDES_Scramble;

    >
    > > process(clk)
    > > begin
    > >   assert (bitmask = (others => '1')) report "oops" severity FAILURE;
    > > end process;

    >
    > > ..or equivalently drive a port on the module with the same error
    > > condition. You should be able to get the synthesizer to do this work
    > > for you.

    >
    > > Just a few random thoughts, hope they help.

    >
    > >  - Kenn

    >
    > And to make it even more robust, note that you actually have three free
    > variables in your code fragment: BUS_WIDTH, DES_FACT, and NUM_CHAN, but
    > only two real degrees of freedom (DES_FACT and NUM_CHAN). (Thy're
    > presumably GENERICS in VHDL but variables in the mathematical
    > sense). Your code implcitly relies on the fact that
    >
    >   BUS_WIDTH=DES_FACT*NUM_CHAN
    >
    > However, you don't assert or verify it. If you want a robust
    > paramaterizable solution you should assert this.
    >
    > How to verify it "stictly: though is another story... that implies that
    > you have a strict spec. If your strict spec is in terms of an equation,
    > then you just trace the equation back to VHDL.
    >
    > Another way to look at it (although not formal in any sense) is to ask
    > yourself if there's another intuitive way to frame the problem so that
    > it's consistent with your goal, then see if the two solutions
    > match. (The concept of safety through redundancy!)
    >
    > Whn you draw out your manual mapping above, it's evident that you're
    > just permuting address bits, so that the LHS has index vector iv
    >
    >   iv(B-1 downto 0),
    >
    > while on the RHS you're permuting these to form the address
    >
    >   iv(B-C-1 downto 0) & iv((B-1) downto (B-C))
    >
    > Where for brevity,
    >
    >   BUS_WIDTH = 2**B; B = 6 here
    >   NUM_CHAN  = 2 ** C; C = 2 here
    >   iv := to_unsigned(i, B)
    >
    > It's clear that by examining the indices that the RHS has the
    > appropriate length in bits:
    >
    >   (B-C) + (C) = B
    >
    > Then you could either rewrite your code, or just assert this to be so:
    >
    > for i in 0 to (BUS_WIDTH -1) generate
    > begin
    >   aligned_data(i) <= data((i/DES_FACT) + ((i mod DES_FACT)*NUM_CHAN));
    >   process
    >      variable iv : unisgned := to_unsigned(i, B)
    >   begin
    >     assert (to_integer(iv) = i) report "LHS oops" severity FAILURE;
    >     assert (to_integer(iv(B-C-1 downto 0) & iv(B-1 downto B-C))
    >           = ((i/DES_FACT) + ((i mod DES_FACT)*NUM_CHAN)))
    >           report "RHS oops" severity FAILURE;
    >   end process;
    > end generate SERDES_Scramble;
    >
    > Arguably, this is very complex on the surface; this has more to do with
    > the fact that it's ugly to express this in VHDL, and little to do with
    > the intent.
    >
    > As a general principle, if you spend enought time on the problem to get
    > at least two methods working, in all their ugly detail, you're probably
    > in good shape!
    >
    > Of course, the transformation I just described assumes that DES_FACT and
    > NUM_CHAN are powers of two, and may have misbehaviour when either is
    > zero, so you want to assert that... ad nauseum.  
    >
    > HTH,
    >
    >  - Kenn
    >
    > --
    > ---------------------------------
    > Remove NOSPAM from email address.


    Thanks Kenn. I've been staring at your solution and I have to admit
    that you completely lost me when it came to your math. I get the
    concept though. Find another solution and assert.

    This assertion I do not think will work however:

    assert (to_integer(iv(B-C-1 downto 0) & iv(B-1 downto B-C))
    > = ((i/DES_FACT) + ((i mod DES_FACT)*NUM_CHAN)))
    > report "RHS oops" severity FAILURE;


    the LHS of the comparison is a constant and the RHS is dependent on
    'i' so this assertion must fail for all but one 'i'.

    iv(3 downto 0) & (5 downto 4)

    Thanks for the help though. I'll keep searching for a way to make
    this work.
     
    Shannon, Sep 21, 2009
    #4
  5. Shannon <> writes:

    > Thanks Kenn. I've been staring at your solution and I have to admit
    > that you completely lost me when it came to your math. I get the
    > concept though. Find another solution and assert.
    >
    > This assertion I do not think will work however:
    >
    > assert (to_integer(iv(B-C-1 downto 0) & iv(B-1 downto B-C))
    >> = ((i/DES_FACT) + ((i mod DES_FACT)*NUM_CHAN)))
    >> report "RHS oops" severity FAILURE;

    >
    > the LHS of the comparison is a constant and the RHS is dependent on
    > 'i' so this assertion must fail for all but one 'i'.


    ...But the left side (iv) is a constant function of i, and is defined
    inside of the for..generate loop, so it actually gets expanded 64 times,
    and so generates 64 different asserts, each of which tries to match a
    unique LHS to a unique RHS.

    On second thought, a process might not be the right vechicle for wrapping
    the assertion; I only did this so I didn't have to write
    to_unsigned(i,B) a whole bunch of times. I thought a constant inside a
    process would be clever. But you might needs some waits in there to make
    it effective.

    I still like the bitmask idea as a way to guarantee bijection
    (one-to-one, non-overlapping correspondence) of your i with your
    transformed i.

    Have fun with this.. I always like to make the language earn its keep
    for these kinds of jobs.

    - Kenn

    --
    ---------------------------------
    Remove NOSPAM from email address.
     
    Kenn Heinrich, Sep 21, 2009
    #5
  6. Shannon

    Shannon Guest

    On Sep 21, 8:41 am, Shannon <> wrote:
    > On Sep 19, 6:50 am, Kenn Heinrich <> wrote:
    >
    >
    >
    > > sleeman <> writes:
    > > > On Sep 18, 11:25 am, Shannon <> wrote:
    > > >> I have the following generate loop:

    >
    > > >> SERDES_Scramble :
    > > >> for i in 0 to (BUS_WIDTH -1) generate
    > > >> begin
    > > >>         aligned_data(i) <= data((i/DES_FACT) + ((i mod DES_FACT)*NUM_CHAN));
    > > >> end generate SERDES_Scramble;

    >
    > > >> So for a deserialization factor of 4 and 16 channels (BUS_WIDTH = 64)
    > > >> this should produce:

    >
    > > >> aligned_data(0) <= data(0);
    > > >> aligned_data(1) <= data(16);
    > > >> aligned_data(2) <= data(32);
    > > >> aligned_data(3) <= data(48);

    >
    > > >> aligned_data(4) <= data(1);
    > > >> aligned_data(5) <= data(17);
    > > >> aligned_data(6) <= data(33);
    > > >> aligned_data(7) <= data(49);

    >
    > > >> ....

    >
    > > >> aligned_data(60) <= data(15);
    > > >> aligned_data(61) <= data(61);
    > > >> aligned_data(62) <= data(62);
    > > >> aligned_data(63) <= data(63);

    >
    > > >> I believe this works but how do I verify it strictly?  The RTL viewer
    > > >> in Quartus creates busses for things like this and I can't see the one
    > > >> to one connections.

    >
    > > > A couple of things pop into mind off the bat (And please excuse the
    > > > obvious syntax fragmentation and probable typos in advance :):

    >
    > > > (option 1)

    >
    > > > Execute the code in the simulator: write a separate process for
    > > > simulation only (hidden by a synthesis translate off pragma, or inside
    > > > an IF..GENERATE block).  Inside this process, write the same code as
    > > > above but print out your mapping explicitly:

    >
    > > > process
    > > >   for i in  to (BUS_WIDTH -1) loop
    > > >     report "aligned(" & integer'image(i) & ") <= data(" &
    > > >         integer'image((i/DES_FACT) + ((i mod DES_FACT)*NUM_CHAN))
    > > >          & ");"
    > > >   end loop;
    > > >   wait;
    > > > end process;

    >
    > > > Of course, this only tells you your simulator is right, it doesn't
    > > > tell you that synth matches your sims.

    >
    > > > (option 2)

    >
    > > > In synthesis, write a 64 bit bitmask, initialized to zero.  Inside the
    > > > generation loop, set each destination bit as you go through the loop,
    > > > then check that the entire vector is all ones after the loop is done.
    > > > This should be an invariant, so should synthesie out trivially, but if
    > > > your logic is wrong you'll double-point to the same bit twice so
    > > > you'll leave some bits empty (pigeon-hole principle).

    >
    > > > The key idea is that your transform is strictly a *permutation* so
    > > > that you guarantee all 64 bits will be covered exactly once.

    >
    > > > bitmask : std_ulogic_vector(0 to BUS_WiDTH-1) := (others => '0');

    >
    > > >  SERDES_Scramble :
    > > >  for i in 0 to (BUS_WIDTH -1) generate
    > > >  begin
    > > >          aligned_data(i) <= data((i/DES_FACT) + ((i mod DES_FACT)
    > > > *NUM_CHAN));
    > > >          bitmask((i/DES_FACT) + ((i mod DES_FACT)*NUM_CHAN)) <= '1';
    > > >  end generate SERDES_Scramble;

    >
    > > > process(clk)
    > > > begin
    > > >   assert (bitmask = (others => '1')) report "oops" severity FAILURE;
    > > > end process;

    >
    > > > ..or equivalently drive a port on the module with the same error
    > > > condition. You should be able to get the synthesizer to do this work
    > > > for you.

    >
    > > > Just a few random thoughts, hope they help.

    >
    > > >  - Kenn

    >
    > > And to make it even more robust, note that you actually have three free
    > > variables in your code fragment: BUS_WIDTH, DES_FACT, and NUM_CHAN, but
    > > only two real degrees of freedom (DES_FACT and NUM_CHAN). (Thy're
    > > presumably GENERICS in VHDL but variables in the mathematical
    > > sense). Your code implcitly relies on the fact that

    >
    > >   BUS_WIDTH=DES_FACT*NUM_CHAN

    >
    > > However, you don't assert or verify it. If you want a robust
    > > paramaterizable solution you should assert this.

    >
    > > How to verify it "stictly: though is another story... that implies that
    > > you have a strict spec. If your strict spec is in terms of an equation,
    > > then you just trace the equation back to VHDL.

    >
    > > Another way to look at it (although not formal in any sense) is to ask
    > > yourself if there's another intuitive way to frame the problem so that
    > > it's consistent with your goal, then see if the two solutions
    > > match. (The concept of safety through redundancy!)

    >
    > > Whn you draw out your manual mapping above, it's evident that you're
    > > just permuting address bits, so that the LHS has index vector iv

    >
    > >   iv(B-1 downto 0),

    >
    > > while on the RHS you're permuting these to form the address

    >
    > >   iv(B-C-1 downto 0) & iv((B-1) downto (B-C))

    >
    > > Where for brevity,

    >
    > >   BUS_WIDTH = 2**B; B = 6 here
    > >   NUM_CHAN  = 2 ** C; C = 2 here
    > >   iv := to_unsigned(i, B)

    >
    > > It's clear that by examining the indices that the RHS has the
    > > appropriate length in bits:

    >
    > >   (B-C) + (C) = B

    >
    > > Then you could either rewrite your code, or just assert this to be so:

    >
    > > for i in 0 to (BUS_WIDTH -1) generate
    > > begin
    > >   aligned_data(i) <= data((i/DES_FACT) + ((i mod DES_FACT)*NUM_CHAN));
    > >   process
    > >      variable iv : unisgned := to_unsigned(i, B)
    > >   begin
    > >     assert (to_integer(iv) = i) report "LHS oops" severity FAILURE;
    > >     assert (to_integer(iv(B-C-1 downto 0) & iv(B-1 downto B-C))
    > >           = ((i/DES_FACT) + ((i mod DES_FACT)*NUM_CHAN)))
    > >           report "RHS oops" severity FAILURE;
    > >   end process;
    > > end generate SERDES_Scramble;

    >
    > > Arguably, this is very complex on the surface; this has more to do with
    > > the fact that it's ugly to express this in VHDL, and little to do with
    > > the intent.

    >
    > > As a general principle, if you spend enought time on the problem to get
    > > at least two methods working, in all their ugly detail, you're probably
    > > in good shape!

    >
    > > Of course, the transformation I just described assumes that DES_FACT and
    > > NUM_CHAN are powers of two, and may have misbehaviour when either is
    > > zero, so you want to assert that... ad nauseum.  

    >
    > > HTH,

    >
    > >  - Kenn

    >
    > > --
    > > ---------------------------------
    > > Remove NOSPAM from email address.

    >
    > Thanks Kenn.  I've been staring at your solution and I have to admit
    > that you completely lost me when it came to your math.  I get the
    > concept though.  Find another solution and assert.
    >
    > This assertion I do not think will work however:
    >
    > assert (to_integer(iv(B-C-1 downto 0) & iv(B-1 downto B-C))
    >
    > >           = ((i/DES_FACT) + ((i mod DES_FACT)*NUM_CHAN)))
    > >           report "RHS oops" severity FAILURE;

    >
    > the LHS of the comparison is a constant and the RHS is dependent on
    > 'i' so this assertion must fail for all but one 'i'.
    >
    > iv(3 downto 0) & (5 downto 4)
    >
    > Thanks for the help though.  I'll keep searching for a way to make
    > this work.


    aahhhh nevermind. I get your math now. Sorry. You meant to say C=4
    and yes I see that it isn't constant. ok. Just needed some coffee
    there. Very interesting observation you made. I had to expand it out
    in binary to see it. Now I can look at my equation and actually see
    the bit manipulation. Thanks.

    assertions just get painlessly ignored during synthesis right?
     
    Shannon, Sep 21, 2009
    #6
  7. Shannon <> writes:

    > aahhhh nevermind. I get your math now. Sorry. You meant to say C=4


    you got me there... I guess I needed coffee too. Sorry if I cost you time.

    > and yes I see that it isn't constant. ok. Just needed some coffee
    > there. Very interesting observation you made. I had to expand it out
    > in binary to see it. Now I can look at my equation and actually see
    > the bit manipulation. Thanks.
    >


    I also realized that there's a perfectly good declarative region inside
    the block statement, which gives you this simpler pattern:

    for i... generate
    constant iv := ...
    begin
    x <= y;
    assert f(i) = g(iv) report ...;
    end block;

    > assertions just get painlessly ignored during synthesis right?
    >


    As far as I can tell they're supposed to, but anecdotally I seem to
    recall some funny behaviour with really old tools, so I often have an
    ENABLE_DEBUG generic in my code to turn them off (inside a nested
    if...generate for example) in case I run into issues. That's kind of
    stupid in the bigger picture (turning off your assertions that check
    synthesis, during the synthesis), but then, so are a lot of FPGA tool
    problems! Perhaps my anecdotal stories are nothing but unfounded fears
    that continue to poison my coding style needlessly... it's on my
    rainy-day list of things to research. On the other hand, there's
    probably little risk of me needing to recompile today's design targeted
    to a $500 FPGA with twelve year old tools that target 22V10's anyway!

    - Kenn


    --
    ---------------------------------
    Remove NOSPAM from email address.
     
    Kenn Heinrich, Sep 22, 2009
    #7
    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. Rajesh Bawa

    Re: Outsoursing Hardware verification

    Rajesh Bawa, Jul 5, 2003, in forum: VHDL
    Replies:
    2
    Views:
    1,178
    Prasanna
    Aug 5, 2003
  2. Recruit Interns

    Verification Intern Positions Available

    Recruit Interns, Aug 14, 2003, in forum: VHDL
    Replies:
    0
    Views:
    1,218
    Recruit Interns
    Aug 14, 2003
  3. Veritec
    Replies:
    2
    Views:
    977
    Andy Peters
    Sep 26, 2003
  4. thewhizkid
    Replies:
    3
    Views:
    735
    Jerker Hammarberg \(DST\)
    Oct 7, 2003
  5. geremy condra
    Replies:
    6
    Views:
    391
    Gregory Ewing
    Jul 30, 2010
Loading...

Share This Page