ASL
let NASLLocal = (M | Wreg | Rreg) \ ASLLocal
let ASLDATA = DATA
let asl_iico_ctrl = iico_ctrl
let asl_iico_data = iico_data
let asl_rf_reg = rf-reg
let asl_rf = rf
let aarch64 = NASLLocal * NASLLocal
let asl_fr_reg = ([Rreg] ; po ; [Wreg]) & loc
let asl_fr = ([R] ; po ; [W]) & loc
let asl_data = asl_iico_data | asl_rf_reg
let asl_deps = asl_data
let asl_deps_restricted = id | (asl_deps ; ([ASLLocal] ; asl_deps)+)
let aarch64_iico_data = ( asl_deps_restricted ; asl_data+ ) & aarch64
let aarch64_iico_ctrl = ( asl_deps_restricted ; asl_iico_ctrl ; asl_iico_data* ) & aarch64
let aarch64_iico_order = ( asl_fr | asl_fr_reg ) & aarch64
let aarch64_intrinsic = aarch64_iico_ctrl | aarch64_iico_data | aarch64_iico_order
let AArch64 = NASLLocal
let to_data = (asl_deps_restricted ; [DATA] ; asl_iico_data ; [W | Wreg]) & aarch64
let AArch64_DATA = NASLLocal & domain (to_data)
show [AArch64_DATA] as AArch64_DATA
show [DATA] as debug_data
acyclic (aarch64_intrinsic | po) as asl_determinism
show AArch64
show aarch64_iico_ctrl, aarch64_iico_data, aarch64_iico_order