(* This is a ________ _______ __ _________ _________ |_ ___ \.|_ __ \ / \ |_ ___ | _ _ | | | \. \ | |__) | / /\ \ | |_ \_|_/ | | \_| | | | | | __ / / ____ \ | _| | | _| |___.' /_| | \ \_ _/ / \ \_ _| |_ _| |_ |________.'|____| |___|____| |____|_____| |_____| model for ^~^ , ('Y') ) / \/ ASL __QQ (\|||/) (_)_"> / Please do consider this as a work in progress. *) ASL (*************) (* Renamings *) (*************) let AArch64 = ~ASLLocal let asl_iico_ctrl = iico_ctrl let asl_iico_data = iico_data let asl_rf_reg = rf-reg let asl_rf = rf (* Warning, partial_po is _implicitely_ transitive *) let asl_po = as_transitive (partial_po) (*********************) (* Working relations *) (*********************) let aarch64 = AArch64 * AArch64 let asl_data = asl_iico_data | asl_rf_reg let asl_deps = asl_data+ let asl_ctrl_deps = (asl_data | asl_iico_ctrl)+ (**********************************) (* Intra-instruction dependencies *) (**********************************) (* Intra-instruction Data dependencies *) let aarch64_iico_data = [AArch64 \ B]; asl_deps; [AArch64] (* Intra-instruction Control dependencies *) let aarch64_iico_ctrl = [B]; asl_ctrl_deps; [AArch64] (* Intra-instruction Order dependencies *) let asl_fr = asl_po & ([R] ; loc ; [W]) let aarch64_iico_order = asl_fr & aarch64 let aarch64_intrinsic = aarch64_iico_ctrl | aarch64_iico_data | aarch64_iico_order (* Tests *) acyclic (aarch64_intrinsic | asl_po) as asl_determinism (**************) (* Event sets *) (**************) let restrict-finals s = (* Asumming that non-final writes are read internally *) let non-final = domain(rf-reg) in s \ non-final let AArch64_Finals = restrict-finals(AArch64&Wreg) (* Compute AArch64 ADDR and DATA event sets *) let AArch64Reg = AArch64\(M|B) let to_addr = [AArch64Reg]; asl_deps; [ADDR]; asl_iico_data; [AArch64] let AArch64_ADDR = domain(to_addr) let to_memwrite = [AArch64Reg \ AArch64_ADDR]; aarch64_iico_data; aarch64_iico_ctrl?; [W] let AArch64_DATA = domain(to_memwrite) (* Branching events to PC writes are of the branch conditional kind *) let AArch64_BCC = domain ([B]; aarch64_iico_ctrl; [WPC]) (***********) (* Display *) (***********) (* Keep significant branching effects only. * Significant branching effect are the ones * that stand on a control path from AArch64 * relevant accesses. *) let AArch64NoB = AArch64 \ B let reaching = domain ([B]; aarch64_iico_ctrl; [AArch64NoB]) let R = [B];asl_iico_ctrl;asl_data? let reachable = range ([AArch64NoB]; aarch64_iico_data; R?; [B]) let AArch64B = reaching & reachable let AArch64 = AArch64NoB | AArch64B show AArch64 show aarch64_iico_ctrl show aarch64_iico_data show aarch64_iico_order show AArch64_Finals show AArch64_ADDR show AArch64_DATA show AArch64_BCC