Re: [Qemu-devel] [PATCH] SPARC target : Fix carry flagupdate inaddxcc and subxc

[Even Rouault]

Hello,

As far as the V flag is concerned, I've taken a look at the Sparc V8 reference manual (www.sparc.org/standards/V8.pdf)

We can read at page 170 for the update of the V flag for "addcc" and "addxcc":

Vtheory = (r[rs1]<31> & operand2<31> & !result<31>) | (!r[rs1]<31> & !operand2<31> && result<31>)

Let's transform this with the name of the variables in the qemu code :

Vtheory = (src1<31> & T1<31> & !T0<31>) | (!src1<31> & !T1<31> & T0<31>)

Vtheory = ((src1 & T1 & ~T0) | (~src1 & ~T1 & T0)<31>

And we have in qemu code :

Vqemu = ((src1 ^ T1 ^ -1) & (src1 ^ T0))<31>

Now, let's transform Vqemu :

Vqemu = ((src1 ^ (T1 ^ -1)) & (src1 ^ T0))<31>

Vqemu = ((src1 ^ ~T1) & (src1 ^ T0))<31>

Vqemu = (((src1 & ~(~T1)) | (~src1 & ~T1)) & (src1 ^ T0))<31>

Vqemu = (((src1 & T1) | (~src1 & ~T1)) & (src1 ^ T0))<31>

Vqemu = ((src1 & T1 & (src1 ^ T0)) | (~src1 & ~T1 & (src1 ^ T0)))<31>

Vqemu = ((src1 & T1 & ((src1 & ~T0) | (~src1 & T0))) |

(~src1 & ~T1 & ((src1 & ~T0) | (~src1 & T0))))<31>

Vqemu = ((src1 & T1 & src1 & ~T0) | (src1 & T1 & ~src1 & T0) |

(~src1 & ~T1 & src1 & ~T0) | (~src1 & ~T1 & ~src1 & T0))<31>

Vqemu = ((src1 & T1 & ~T0) | (~src1 & ~T1 & T0))<31>

Vqemu = Vtheroy !

After theory, a bit of practice! I just wrote a small piece of code that enumerates the 2*2*2=8 combinations and proves experimentally that Vqemu = Vtheroy.

int main(int argc, char* argv[])

{

int src1, T1, T0;

for(src1=0;src1<=1;src1++)

{

for(T1=0;T1<=1;T1++)

{

for(T0=0;T0<=1;T0++)

{

int V1 = (src1 & T1 & ~T0) | (~src1 & ~T1 & T0);

int V2 = (src1 ^ T1 ^ 1) & (src1 ^ T0);

printf("src1=%d T1=%d T0=%d, V=%d=%d\n", src1, T1, T0, V1, V2);

}

}

}

}

The output is :

src1=0 T1=0 T0=0, V=0=0

src1=0 T1=0 T0=1, V=1=1

src1=0 T1=1 T0=0, V=0=0

src1=0 T1=1 T0=1, V=0=0

src1=1 T1=0 T0=0, V=0=0

src1=1 T1=0 T0=1, V=0=0

src1=1 T1=1 T0=0, V=1=1

src1=1 T1=1 T0=1, V=0=0

In other words, the V flag is set when :

• the most significant bit of src1=src2=0 and dst=1 : the result of the addition of two signed positive words is not a signed positive word
• the most significant bit of src1=src2=1 and dst=0 : the result of the addition of two signed negative words is not a signed negative word (or the result of the addition of two unsigned words is a lower unsigned word)

Conclusion : the computation of the V flag in qemu is correct, and their is no special case to consider if the C flag is set or not :-)

For tomorrow, the formal proof of the correctness of the whole qemu code ;-)

Le Jeudi 13 Avril 2006 20:39, vous avez écrit :

> >As far as the V flag is concerned, mmm, I'm not really sure whether we

> >should

> >change something in the sparc code. If we compare to the arm code, we

> > don't take into account the fact that the carry flag is set before.

> >

> >We'd probably need some extensive tests and their associated expected

> >results.

>

> I made a small test program (attached) to test the addx instruction. The

> program calculates the sum of two 64-bit values, given on the command line

> as 32-bit lower and upper parts. Native system produces following:

> $ ./addx -1 -1 0x80000000 -1

> ffffffffffffffff + ffffffff80000000 = ffffffff7fffffff, NZVC: 9

> while unpatched Qemu the following:

> $ qemu-sparc ./addx -1 -1 0x80000000 -1

> ffffffffffffffff + ffffffff80000000 = ffffffff7fffffff, NZVC: 8

>

> So the carry flag not set. When your patch is applied, the output is

> identical:

> ffffffffffffffff + ffffffff80000000 = ffffffff7fffffff, NZVC: 9

>

> I couldn't think of a combination of values that would set the V flag when

> there is also a carry from the 32-bit addition, any suggestions?

>

> _________________________________________________________________

> FREE pop-up blocking with the new MSN Toolbar - get it now!

> http://toolbar.msn.click-url.com/go/onm00200415ave/direct/01/