(* This is a ________ _______ __ _________ _________ |_ ___ \.|_ __ \ / \ |_ ___ | _ _ | | | \. \ | |__) | / /\ \ | |_ \_|_/ | | \_| | | | | | __ / / ____ \ | _| | | _| |___.' /_| | \ \_ _/ / \ \_ _| |_ _| |_ |________.'|____| |___|____| |____|_____| |_____| model for ^~^ , ('Y') ) / \/ ASL __QQ (\|||/) (_)_"> / Please do consider this as a work in progress. *) ASL (* Renamings *) 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 (* Working relations *) let aarch64 = NASLLocal * NASLLocal let asl_fr_reg = ([Rreg] ; po ; [Wreg]) & loc (* loc extended to registers *) let asl_fr = ([R] ; po ; [W]) & loc let asl_data = asl_iico_data | asl_rf_reg let asl_deps = asl_data (* | asl_iico_ctrl *) let asl_deps_restricted = id | (asl_deps ; ([ASLLocal] ; asl_deps)+) let aarch64_iico_data = ( asl_deps_restricted ; asl_data+ ) & aarch64 (* Here we do need asl_iico_data after the asl_iico_ctrl as the asl_iico_ctrl does not propagate inside an asl statement *) 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 (* Event sets *) let AArch64 = NASLLocal (* DATA and NDATA *) 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 (* TODO *) (* B = write to PC *) (* BCC = range(aarch64_iico_ctrl) & B *) (* Pred = BranchTo(VBAR something) ??? *) (* F = call to (data memory ?) barrier *) (* Tests *) acyclic (aarch64_intrinsic | po) as asl_determinism (* Display *) (* show asl_iico_ctrl, asl_iico_data, asl_rf_reg show iico_ctrl, iico_data, rf, rf-reg *) show AArch64 show aarch64_iico_ctrl, aarch64_iico_data, aarch64_iico_order