Verification Question

S

Shannon

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

sleeman

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
 
K

Kenn Heinrich

sleeman said:
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
 
S

Shannon

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

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

Kenn Heinrich

Shannon said:
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))

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
 
S

Shannon

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


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?
 
K

Kenn Heinrich

Shannon said:
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
 

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

No members online now.

Forum statistics

Threads
473,744
Messages
2,569,482
Members
44,900
Latest member
Nell636132

Latest Threads

Top