Test MP+HD-DSB.LD

AArch64 MP+HD-DSB.LD
TTHM=HD
{
pte_x=(oa:phy_x,db:0,dbm:1);

0:X1=x;
0:X2=1;
0:X3=1;
0:X4=y;

1:X4=y;
1:X1=pte_x;
}
P0          | P1          ;
STR W2,[X1] | LDR W3,[X4] ;
DSB LD      | DMB LD      ;
STR W3,[X4] | LDR X2,[X1] ;
exists (1:X2=(oa:PA(x), dbm:1, db:0) /\ 1:X3=1)