Test ppc-n6

PPC ppc-n6 (PPCnSix) "Store buffering illustration"
{
  P0:r5=x; P0:r6=y;
  P1:r5=x; P1:r6=y; 
  x = 0 ; y = 0 ;
  P0:r0=1; P1:r7=2;
}
   P0          |     P1       ;
stw r0,0,r5    |  stw r7,0,r6 ;
lwz r1,0,r5    |  stw r7,0,r5 ;
lwz r2,0,r6    |              ;


exists (x=1 /\ P0:r1=1 /\ P0:r2=0)
(* On power, does not exactly identify store buffers... *)
<<
genprog generated/ppc-n6-prog.tex
show 0
essdump generated/ppc-n6-ess.dot
>>
<<
show 0
readfrom generated/ppc-n6-rf.dot
>>