From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mailman by lists.gnu.org with tmda-scanned (Exim 4.43) id 1FU9Ap-0000ob-6b for qemu-devel@nongnu.org; Thu, 13 Apr 2006 17:16:19 -0400 Received: from exim by lists.gnu.org with spam-scanned (Exim 4.43) id 1FU9Ao-0000oG-5U for qemu-devel@nongnu.org; Thu, 13 Apr 2006 17:16:18 -0400 Received: from [199.232.76.173] (helo=monty-python.gnu.org) by lists.gnu.org with esmtp (Exim 4.43) id 1FU9Ao-0000oD-2l for qemu-devel@nongnu.org; Thu, 13 Apr 2006 17:16:18 -0400 Received: from [212.247.155.44] (helo=swip.net) by monty-python.gnu.org with esmtp (Exim 4.52) id 1FU9GC-0002e5-Cv for qemu-devel@nongnu.org; Thu, 13 Apr 2006 17:21:52 -0400 From: Even Rouault Subject: Re: [Qemu-devel] [PATCH] SPARC target : Fix carry flagupdate inaddxcc and subxc Date: Thu, 13 Apr 2006 23:14:43 +0200 References: In-Reply-To: MIME-Version: 1.0 Content-Type: multipart/alternative; boundary="Boundary-00=_E9rPEt2zgrfIGks" Content-Transfer-Encoding: 7bit Content-Disposition: inline Message-Id: <200604132314.44622.even.rouault@mines-paris.org> Reply-To: qemu-devel@nongnu.org List-Id: qemu-devel.nongnu.org List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , To: Blue Swirl , qemu-devel@nongnu.org --Boundary-00=_E9rPEt2zgrfIGks Content-Type: text/plain; charset="iso-8859-15" Content-Transfer-Encoding: quoted-printable Hello,=20 As far as the V flag is concerned, I've taken a look at the Sparc V8 refere= nce manual (www.sparc.org/standards/V8.pdf) We can read at page 170 for the update of the V flag for "addcc" and "addxc= c": Vtheory =3D (r[rs1]<31> & operand2<31> & !result<31>) | (!r[rs1]<31> & !ope= rand2<31> && result<31>) Let's transform this with the name of the variables in the qemu code : Vtheory =3D (src1<31> & T1<31> & !T0<31>) | (!src1<31> & !T1<31> & T0<31>) Vtheory =3D ((src1 & T1 & ~T0) | (~src1 & ~T1 & T0)<31> And we have in qemu code : Vqemu =3D ((src1 ^ T1 ^ -1) & (src1 ^ T0))<31> Now, let's transform Vqemu : Vqemu =3D ((src1 ^ (T1 ^ -1)) & (src1 ^ T0))<31> Vqemu =3D ((src1 ^ ~T1) & (src1 ^ T0))<31> Vqemu =3D (((src1 & ~(~T1)) | (~src1 & ~T1)) & (src1 ^ T0))<31> Vqemu =3D (((src1 & T1) | (~src1 & ~T1)) & (src1 ^ T0))<31> Vqemu =3D ((src1 & T1 & (src1 ^ T0)) | (~src1 & ~T1 & (src1 ^ T0)))<31> Vqemu =3D ((src1 & T1 & ((src1 & ~T0) | (~src1 & T0))) | (~src1 & ~T1 & ((src1 & ~T0) | (~src1 & T0))))<31> Vqemu =3D ((src1 & T1 & src1 & ~T0) | (src1 & T1 & ~src1 & T0) | (~src1 & ~T1 & src1 & ~T0) | (~src1 & ~T1 & ~src1 & T0))<31> Vqemu =3D ((src1 & T1 & ~T0) | (~src1 & ~T1 & T0))<31> Vqemu =3D Vtheroy ! After theory, a bit of practice! I just wrote a small piece of code that en= umerates the 2*2*2=3D8 combinations and proves experimentally that Vqemu = =3D Vtheroy. int main(int argc, char* argv[]) { int src1, T1, T0; for(src1=3D0;src1<=3D1;src1++) { for(T1=3D0;T1<=3D1;T1++) { for(T0=3D0;T0<=3D1;T0++) { int V1 =3D (src1 & T1 & ~T0) | (~src1 & ~T1 & T0); int V2 =3D (src1 ^ T1 ^ 1) & (src1 ^ T0); printf("src1=3D%d T1=3D%d T0=3D%d, V=3D%d=3D%d\n", src1, T1, T0, V= 1, V2); } } } } The output is : src1=3D0 T1=3D0 T0=3D0, V=3D0=3D0 src1=3D0 T1=3D0 T0=3D1, V=3D1=3D1 src1=3D0 T1=3D1 T0=3D0, V=3D0=3D0 src1=3D0 T1=3D1 T0=3D1, V=3D0=3D0 src1=3D1 T1=3D0 T0=3D0, V=3D0=3D0 src1=3D1 T1=3D0 T0=3D1, V=3D0=3D0 src1=3D1 T1=3D1 T0=3D0, V=3D1=3D1 src1=3D1 T1=3D1 T0=3D1, V=3D0=3D0 In other words, the V flag is set when : the most significant bit of src1=3Dsrc2=3D0 and dst=3D1 : the result of the= addition of two signed positive words is not a signed positive word the most significant bit of src1=3Dsrc2=3D1 and dst=3D0 : the result of the= addition of two signed negative words is not a signed negative word (or th= e 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 :-) =46or tomorrow, the formal proof of the correctness of the whole qemu code = ;-) Le Jeudi 13 Avril 2006 20:39, vous avez =E9crit=A0: > >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 =3D ffffffff7fffffff, NZVC: 9 > while unpatched Qemu the following: > $ qemu-sparc ./addx -1 -1 0x80000000 -1 > ffffffffffffffff + ffffffff80000000 =3D ffffffff7fffffff, NZVC: 8 > > So the carry flag not set. When your patch is applied, the output is > identical: > ffffffffffffffff + ffffffff80000000 =3D 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/ --Boundary-00=_E9rPEt2zgrfIGks Content-Type: text/html; charset="iso-8859-15" Content-Transfer-Encoding: quoted-printable

Hello,

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

We can read at page 170 for the update of the V flag for "addcc&quo= t; and "addxcc":

Vtheory =3D (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 =3D (src1<31> & T1<31> & !T0<31>) | (!= src1<31> & !T1<31> & T0<31>)

Vtheory =3D ((src1 & T1 & ~T0) | (~src1 & ~T1 & T0)<3= 1>

And we have in qemu code :

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

Now, let's transform Vqemu :

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

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

Vqemu =3D (((src1 & ~(~T1)) | (~src1 & ~T1)) & (src1 ^ T0))&= lt;31>

Vqemu =3D (((src1 & T1) | (~src1 & ~T1)) & (src1 ^ T0))<3= 1>

Vqemu =3D ((src1 & T1 & (src1 ^ T0)) | (~src1 & ~T1 & (s= rc1 ^ T0)))<31>

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

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

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

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

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

Vqemu =3D Vtheroy !

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

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

{

int src1, T1, T0;

for(src1=3D0;src1<=3D1;src1++)

{

for(T1=3D0;T1<=3D1;T1++)

{

for(T0=3D0;T0<=3D1;T0++)

{

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

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

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

}

}

}

}

The output is :

src1=3D0 T1=3D0 T0=3D0, V=3D0=3D0

src1=3D0 T1=3D0 T0=3D1, V=3D1=3D1=

src1=3D0 T1=3D1 T0=3D0, V=3D0=3D0

src1=3D0 T1=3D1 T0=3D1, V=3D0=3D0

src1=3D1 T1=3D0 T0=3D0, V=3D0=3D0

src1=3D1 T1=3D0 T0=3D1, V=3D0=3D0

src1=3D1 T1=3D1 T0=3D0, V=3D1=3D1=

src1=3D1 T1=3D1 T0=3D1, V=3D0=3D0

In other words, the V flag is set when :

  • the most significant bit of src1=3Dsrc2=3D0 and dst= =3D1 : the result of the addition of two signed positive words is not a sig= ned positive word
  • the most significant bit of src1=3Dsrc2=3D1 and dst=3D0 : the result of= the addition of two signed negative words is not a signed negative word (o= r 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 =E9crit=A0:

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

> >should

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

> > don't take into account the fact that the carry flag is set be= fore.

> >

> >We'd probably need some extensive tests and their associated ex= pected

> >results.

>

> I made a small test program (attached) to test the addx instruction= =2E The

> program calculates the sum of two 64-bit values, given on the comma= nd line

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

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

> ffffffffffffffff + ffffffff80000000 =3D ffffffff7fffffff, NZVC: 9

> while unpatched Qemu the following:

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

> ffffffffffffffff + ffffffff80000000 =3D ffffffff7fffffff, NZVC: 8

>

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

> identical:

> ffffffffffffffff + ffffffff80000000 =3D ffffffff7fffffff, NZVC: 9

>

> I couldn't think of a combination of values that would set the V fl= ag 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/

--Boundary-00=_E9rPEt2zgrfIGks--