include "aarch64util.cat"
let tc-ib = [Imp & Tag & R]; iico_data; [B]; iico_ctrl; [(Exp & W) \ Tag | TagCheck & FAULT]
let tr-ib =
[Imp & TTD & R]; iico_data; [B]; iico_ctrl; [Exp & M | MMU & FAULT]
let f-ib =
[Imp & Instr & R]; iico_data; [B]; iico_ctrl; [
_]
let TTD-same-oa = same-oa(TTD*TTD)
let same-loc = loc | tr-ib^-1; TTD-same-oa; tr-ib
let po-loc = po & same-loc
let va-loc = (tr-ib; same-low-order-bits; tr-ib^-1) & loc
let po-va-loc = po & va-loc
let lrs = [W]; (po-loc \ intervening-write(po-loc)) ; [R]
let lws = [M]; po-loc; [W | MMU & FAULT]
let HU = Imp & TTD & W
assert empty HU \ (AF | DB)
let DSB-ob =
[M | DC.CVAU | IC]; po; [dsb.full]; po; [~(Imp & M)]
| (
if "ETS2" then [M | DC.CVAU | IC]; po; [dsb.full]; po; [Imp & TTD & M]
else 0)
| [(Exp & R) \ NoRet]; po; [dsb.ld]; po; [~(Imp & M)]
| (
if "ETS2" then [(Exp & R) \ NoRet]; po; [dsb.ld]; po; [Imp & TTD & M]
else 0)
| [Exp & W]; po; [dsb.st]; po; [~(Imp & M)]
| (
if "ETS2" then [Exp & W]; po; [dsb.st]; po; [Imp & TTD & M]
else 0)
let EXC-ENTRY-CSE = EXC-ENTRY
let EXC-RET-CSE =
if not "ExS" ||
"EOS" then EXC-RET
else {}
let CSE = ISB | EXC-ENTRY-CSE | EXC-RET-CSE
let CSE-ob =
[Exp & R]; ctrl; [CSE]; po
| DSB-ob; [CSE]; po
| [Imp & TTD & R]; tr-ib; [CSE]; po
| [Imp & Instr & R]; f-ib; [CSE]; po
let dob = addr | data
| ctrl; [W]
| addr; [Exp]; po; [CSE]; po; [R]
| addr; [Exp]; po; [W]
| (addr | data); [Exp]; lrs
let pob = [Exp]; pick-dep; [W]
| [Exp]; pick-ctrl-dep; [CSE]; po; [M]
| [Exp]; pick-addr-dep; [Exp]; po; [CSE]; po; [M]
| [Exp]; pick-addr-dep; [Exp & M]; po; [W]
let aob = rmw
| rmw; lrs; [A | Q]
let bob = po; [dmb.full]; po
| [R \ NoRet]; po; [dmb.ld]; po
| [W]; po; [dmb.st]; po; [W | MMU & FAULT]
| [range([A];amo;[L])]; po
| [L]; po; [A]
| [A | Q]; (po | iico_order)
| (po | iico_order); [L]
let rec lob = lws; sca-class?
| dob
| pob
| aob
| bob
| lob; lob
let pick-lob = pick-basic-dep; lob; [W]
let TLBUncacheable = MMU & (Translation | AccessFlag)
let rec local-hw-reqs =
tc-ib
| tr-ib
| f-ib
| [Exp & M | Imp & Tag & R]; (lob | pick-lob); [Exp & M | Imp & Tag & R | (TagCheck | MMU) & FAULT]
| (
if "ETS2" then [Exp & M]; po; [TLBUncacheable & FAULT]; tr-ib^-1; [Imp & TTD & R]
else 0)
| DSB-ob
| CSE-ob
| [Imp & TTD & R]; po-loc; [W]
| [Imp & TTD & R]; rmw; [HU]
| [Exp & M]; po-loc; [TLBUncacheable & FAULT]
| [Exp & R]; addr; [TLBI | DC.CVAU | IC]
| [Exp & R]; ctrl; [HU]
| [Imp & Instr & R]; po; [~(Imp & Instr & R)]
| [Exp & M]; po; [dmb.full]; po; [DC.CVAU]
| [DC.CVAU]; po; [dmb.full]; po; [Exp & M]
| [DC.CVAU]; po; [dmb.full]; po; [DC.CVAU]
| [Exp & M]; (po & scl); [DC.CVAU]
| [DC.CVAU]; (po & scl); [Exp & M]
| [DC.CVAU]; (po & scl); [DC.CVAU]
| local-hw-reqs; local-hw-reqs