Test ppc-n6v1

PPC ppc-n6v1 (PPCnSixOne) "Real store buffering illustration"
{
  P0:r5=x; P0:r6=y;
  P1:r5=x; P1:r6=y; 
  x = 0 ; y = 0 ;
  P0:r3=1; P1:r7=2;
}
   P0          |     P1       ;
stw r3,0,r5    |  stw r7,0,r6 ;
               |  lwsync      ;
lwz r1,0,r5    |  stw r7,0,r5 ;
lwsync         |              ;
lwz r2,0,r6    |              ;


exists (x=1 /\ P0:r1=1 /\ P0:r2=0)
(* On power, indeed illustrate store buffers (cf. option -buffer false) *)
<<
genprog generated/ppc-n6v1-prog.tex
show 0
essdump generated/ppc-n6v1-ess.dot
>>
<<
show 0
readfrom generated/ppc-n6v1-rf.dot
>>