PPC PPC068-F "Wse Rfi DpAddrdR PodRW Wse Rfi DpAddrdW" {0:r2=y; 0:r6=z; 0:r8=x; 0:r10=a; 0:r14=b; 1:r2=x; 1:r6=y; 1:r8=b; 1:r12=c; 1:r14=a;} P0 | P1 ; li r9,2 | li r1,2 ; li r1,2 | stw r1,0(r2) ; stw r1,0(r2) | li r7,2 ; stw r9,0(r10) | lwz r3,0(r2) ; lwz r11,0(r10) | stw r7,0(r8) ; sync | lwz r9,0(r8) ; lwz r3,0(r2) | xor r10,r9,r9 ; xor r12,r11,r11 | xor r4,r3,r3 ; xor r4,r3,r3 | li r5,1 ; li r13,1 | lwzx r11,r10,r12 ; lwzx r5,r4,r6 | lwsync ; lwsync | stwx r5,r4,r6 ; li r7,1 | lwsync ; stw r7,0(r8) | li r13,1 ; stwx r13,r12,r14 | stw r13,0(r14) ; forall (0:r3=2 /\ (0:r11=2 /\ (1:r3=2 /\ (1:r9=2 /\ (a=2 /\ b=1 /\ x=1 /\ y=2 \/ a=1 /\ (b=2 /\ y=1 /\ (x=2 \/ x=1) \/ b=1 /\ (x=2 /\ y=1 \/ x=1 /\ (y=2 \/ y=1)))) \/ 1:r9=1 /\ a=1 /\ b=1 /\ y=1 /\ (x=2 \/ x=1)) \/ 1:r3=1 /\ a=1 /\ x=1 /\ y=1 /\ (1:r9=2 /\ (b=2 \/ b=1) \/ 1:r9=1 /\ b=1)) \/ 0:r11=1 /\ 1:r3=2 /\ 1:r9=2 /\ a=1 /\ b=1 /\ x=1 /\ y=2) \/ 0:r3=1 /\ 1:r3=2 /\ 1:r9=2 /\ b=1 /\ x=1 /\ y=1 /\ (0:r11=2 /\ (a=2 \/ a=1) \/ 0:r11=1 /\ a=1))