arm/model/armScript.sml

347 val raise'exception_def = Def
357 val ArchVersion_def = Def
372 val HaveDSPSupport_def = Def
382 val HaveThumb2_def = Def
391 val HaveThumbEE_def = Def
404 val HaveMPExt_def = Def
414 val HaveSecurityExt_def = Def
425 val HaveVirtExt_def = Def
435 val rec'PSR_def = Def
448 val reg'PSR_def = Def
463 val write'rec'PSR_def = Def
467 val write'reg'PSR_def = Def
471 val rec'SCTLR_def = Def
491 val reg'SCTLR_def = Def
516 val write'rec'SCTLR_def = Def
520 val write'reg'SCTLR_def = Def
524 val rec'HSCTLR_def = Def
539 val reg'HSCTLR_def = Def
560 val write'rec'HSCTLR_def = Def
564 val write'reg'HSCTLR_def = Def
568 val rec'HSR_def = Def
574 val reg'HSR_def = Def
580 val write'rec'HSR_def = Def
584 val write'reg'HSR_def = Def
588 val rec'SCR_def = Def
598 val reg'SCR_def = Def
611 val write'rec'SCR_def = Def
615 val write'reg'SCR_def = Def
619 val rec'NSACR_def = Def
628 val reg'NSACR_def = Def
640 val write'rec'NSACR_def = Def
644 val write'reg'NSACR_def = Def
648 val rec'HCR_def = Def
665 val reg'HCR_def = Def
687 val write'rec'HCR_def = Def
691 val write'reg'HCR_def = Def
695 val ProcessorID_def = Def ("ProcessorID",AVar uTy,LI 0)
697 val IsExternalAbort_def = Def ("IsExternalAbort",AVar uTy,LX bTy)
699 val IsSecure_def = Def
715 val UnalignedSupport_def = Def
728 val BadMode_def = Def
742 val CurrentModeIsNotUser_def = Def
768 val CurrentModeIsUserOrSystem_def = Def
793 val CurrentModeIsHyp_def = Def
818 val IntegerZeroDivideTrappingEnabled_def = Def
826 val ISETSTATE_def = Def
831 val write'ISETSTATE_def = Def
851 val CurrentInstrSet_def = Def
861 val SelectInstrSet_def = Def
886 val ITSTATE_def = Def
891 val write'ITSTATE_def = Def
901 val ITAdvance_def = Def
924 val InITBlock_def = Def
932 val LastInITBlock_def = Def
939 val ThumbCondition_def = Def
956 val BigEndian_def = Def
960 val SetExclusiveMonitors_def = Def
963 val ExclusiveMonitorsPass_def = Def
966 val ClearExclusiveLocal_def = Def ("ClearExclusiveLocal",iVar"id",LU)
968 val CurrentCond_def = Def
972 val ConditionPassed_def = Def
1017 val SPSR_def = Def
1048 val write'SPSR_def = Def
1092 val CPSRWriteByInstr_def = Def
1577 val SPSRWriteByInstr_def = Def
1730 val RBankSelect_def = Def
1757 val RfiqBankSelect_def = Def
1771 val LookUpRName_def = Def
1846 val Rmode_def = Def
1884 val write'Rmode_def = Def
1946 val R_def = Def
1967 val write'R_def = Def
1978 val SP_def = Def
1982 val write'SP_def = Def
1990 val LR_def = Def
1994 val write'LR_def = Def
2002 val PC_def = Def
2006 val BranchTo_def = Def
2017 val PCStoreValue_def = Def
2021 val BranchWritePC_def = Def
2053 val BXWritePC_def = Def
2096 val LoadWritePC_def = Def
2108 val ALUWritePC_def = Def
2125 val ThisInstrLength_def = Def
2132 val IncPC_def = Def
2148 val mem1_def = Def
2155 val mem_def = Def
2247 val write'mem_def = Def
2403 val BigEndianReverse_def = Def
2434 val Align_def = Def
2439 val Aligned_def = Def
2443 val MemA_with_priv_def = Def
2535 val write'MemA_with_priv_def = Def
2583 val MemA_unpriv_def = Def
2592 val write'MemA_unpriv_def = Def
2603 val MemA_def = Def
2616 val write'MemA_def = Def
2630 val MemU_with_priv_def = Def
2779 val write'MemU_with_priv_def = Def
2851 val MemU_unpriv_def = Def
2860 val write'MemU_unpriv_def = Def
2871 val MemU_def = Def
2884 val write'MemU_def = Def
2898 val NullCheckIfThumbEE_def = Def
2991 val HighestSetBit_def = Def
2996 val CountLeadingZeroBits_def = Def
3002 val LowestSetBit_def = Def
3006 val BitCount_def = Def
3024 val SignExtendFrom_def = Def
3029 val Extend_def = Def
3034 val UInt_def = Def
3037 val SignedSatQ_def = Def
3055 val UnsignedSatQ_def = Def
3073 val SatQ_def = Def
3087 val SignedSat_def = Def
3098 val UnsignedSat_def = Def
3109 val LSL_C_def = Def
3125 val LSL_def = Def
3137 val LSR_C_def = Def
3152 val LSR_def = Def
3164 val ASR_C_def = Def
3179 val ASR_def = Def
3191 val ROR_C_def = Def
3205 val ROR_def = Def
3217 val RRX_C_def = Def
3225 val RRX_def = Def
3230 val DecodeImmShift_def = Def
3249 val DecodeRegShift_def = Def
3257 val Shift_C_def = Def
3291 val Shift_def = Def
3305 val ARMExpandImm_C_def = Def
3318 val ARMExpandImm_def = Def
3330 val ThumbExpandImm_C_def = Def
3384 val ExpandImm_C_def = Def
3399 val AddWithCarry_def = Def
3416 val DataProcessingALU_def = Def
3463 val ArithmeticOpcode_def = Def
3470 val ExcVectorBase_def = Def
3481 val EnterMonitorMode_def = Def
3574 val EnterHypMode_def = Def
3667 val TakeReset_def = Def
3777 val TakeUndefInstrException_def = Def
3982 val TakeSVCException_def = Def
4182 val TakeSMCException_def = Def
4220 val TakeHVCException_def = Def
4245 val TakeDataAbortException_def = Def
4486 val TakePrefetchAbortException_def = Def
4727 val TakePhysicalIRQException_def = Def
5005 val TakeVirtualIRQException_def = Def
5115 val TakePhysicalFIQException_def = Def
5442 val TakeVirtualFIQException_def = Def
5567 val TakeHypTrapException_def = Def
5585 val WriteHSR_def = Def
5666 val CallSupervisor_def = Def
5707 val CallHypervisor_def = Def
5718 val BankedRegisterAccessValid_def = Def
5815 val SPSRAccessValid_def = Def
5911 val rec'FPSCR_def = Def
5929 val reg'FPSCR_def = Def
5952 val write'rec'FPSCR_def = Def
5956 val write'reg'FPSCR_def = Def
5960 val RoundingMode_def = Def
5970 val FPAdd32_def = Def
5978 val FPSub32_def = Def
5986 val FPMul32_def = Def
5994 val FPAdd64_def = Def
6002 val FPSub64_def = Def
6010 val FPMul64_def = Def
6018 val FPToFixed32_def = Def
6052 val FPToFixed64_def = Def
6086 val FixedToFP32_def = Def
6099 val FixedToFP64_def = Def
6112 val D_def = Def
6120 val write'D_def = Def
6136 val S_def = Def
6148 val write'S_def = Def
6170 val VFPExpandImm_def = Def
6183 val FPCompare32_def = Def
6190 val FPCompare64_def = Def
6197 val FPZero32_def = Def
6200 val FPZero64_def = Def
6203 val dfn'vmov_imm_def = Def
6221 val dfn'vmov_def = Def
6241 val dfn'vmov_single_def = Def
6263 val dfn'vmov_two_singles_def = Def
6305 val dfn'vmov_double_def = Def
6358 val dfn'vabs_def = Def
6380 val dfn'vneg_def = Def
6402 val dfn'vsqrt_def = Def
6432 val dfn'vcvt_float_def = Def
6459 val dfn'vcvt_to_integer_def = Def
6495 val dfn'vcvt_from_integer_def = Def
6524 val dfn'vcmp_def = Def
6593 val dfn'vmsr_def = Def
6615 val dfn'vmrs_def = Def
6679 val dfn'vadd_def = Def
6714 val dfn'vsub_def = Def
6749 val dfn'vmul_def = Def
6784 val dfn'vdiv_def = Def
6821 val dfn'vmla_vmls_def = Def
6877 val dfn'vfma_vfms_def = Def
6923 val dfn'vfnma_vfnms_def = Def
6973 val dfn'vneg_mul_def = Def
7079 val dfn'vldr_def = Def
7129 val dfn'vstr_def = Def
7182 val dfn'vldm_def = Def
7399 val dfn'vstm_def = Def
7581 val dfn'BranchTarget_def = Def
7592 val dfn'BranchExchange_def = Def
7600 val dfn'BranchLinkExchangeImmediate_def = Def
7639 val dfn'BranchLinkExchangeRegister_def = Def
7664 val dfn'CompareBranch_def = Def
7679 val dfn'TableBranchByte_def = Def
7743 val dfn'CheckArray_def = Def
7775 val dfn'HandlerBranchLink_def = Def
7795 val dfn'HandlerBranchLinkParameter_def = Def
7819 val dfn'HandlerBranchParameter_def = Def
7834 val dfn'EnterxLeavex_def = Def
7860 val dfn'IfThen_def = Def
7877 val dfn'CountLeadingZeroes_def = Def
7892 val dfn'MoveHalfword_def = Def
7914 val DataProcessing_def = Def
7997 val DataProcessingPC_def = Def
8099 val dfn'Move_def = Def
8126 val dfn'TestCompareImmediate_def = Def
8145 val dfn'ArithLogicImmediate_def = Def
8172 val doRegister_def = Def
8203 val dfn'Register_def = Def
8216 val dfn'TestCompareRegister_def = Def
8229 val dfn'ShiftImmediate_def = Def
8248 val doRegisterShiftedRegister_def = Def
8281 val dfn'RegisterShiftedRegister_def = Def
8294 val dfn'ShiftRegister_def = Def
8313 val dfn'AddSub_def = Def
8323 val dfn'SaturatingAddSubtract_def = Def
8686 val dfn'Multiply32_def = Def
8754 val dfn'MultiplyAccumulate_def = Def
8837 val dfn'MultiplyLong_def = Def
8975 val dfn'MultiplyAccumulateAccumulate_def = Def
9015 val dfn'MultiplySubtract_def = Def
9045 val dfn'Signed16Multiply32Accumulate_def = Def
9106 val dfn'Signed16Multiply32Result_def = Def
9145 val dfn'Signed16x32Multiply32Accumulate_def = Def
9202 val dfn'Signed16x32Multiply32Result_def = Def
9233 val dfn'Signed16Multiply64Accumulate_def = Def
9296 val dfn'SignedMultiplyDual_def = Def
9369 val dfn'SignedMultiplyLongDual_def = Def
9434 val dfn'SignedMostSignificantMultiply_def = Def
9468 val dfn'SignedMostSignificantMultiplySubtract_def = Def
9501 val SignedParallelAddSub16_def = Def
9544 val dfn'SignedAddSub16_def = Def
9590 val dfn'SignedSaturatingAddSub16_def = Def
9622 val dfn'SignedHalvingAddSub16_def = Def
9642 val SignedParallelAddSub8_def = Def
9677 val dfn'SignedAddSub8_def = Def
9756 val dfn'SignedSaturatingAddSub8_def = Def
9812 val dfn'SignedHalvingAddSub8_def = Def
9836 val UnsignedParallelAddSub16_def = Def
9903 val dfn'UnsignedAddSub16_def = Def
9957 val dfn'UnsignedSaturatingAddSub16_def = Def
9990 val dfn'UnsignedHalvingAddSub16_def = Def
10010 val UnsignedParallelAddSub8_def = Def
10059 val dfn'UnsignedAddSub8_def = Def
10151 val dfn'UnsignedSaturatingAddSub8_def = Def
10207 val dfn'UnsignedHalvingAddSub8_def = Def
10231 val dfn'UnsignedSumAbsoluteDifferences_def = Def
10304 val GenerateIntegerZeroDivide_def = Def
10310 val dfn'Divide_def = Def
10361 val dfn'PackHalfword_def = Def
10402 val dfn'Saturate_def = Def
10453 val dfn'Saturate16_def = Def
10525 val dfn'ExtendByte_def = Def
10553 val dfn'ExtendByte16_def = Def
10586 val dfn'ExtendHalfword_def = Def
10614 val dfn'SelectBytes_def = Def
10655 val dfn'ByteReverse_def = Def
10672 val dfn'ByteReversePackedHalfword_def = Def
10689 val dfn'ByteReverseSignedHalfword_def = Def
10704 val dfn'ReverseBits_def = Def
10717 val dfn'BitFieldExtract_def = Def
10746 val dfn'BitFieldClearOrInsert_def = Def
10769 val dfn'LoadWord_def = Def
10911 val dfn'LoadLiteral_def = Def
10998 val dfn'LoadUnprivileged_def = Def
11117 val dfn'LoadByte_def = Def
11186 val dfn'LoadByteLiteral_def = Def
11220 val dfn'LoadByteUnprivileged_def = Def
11286 val dfn'LoadSignedByteUnprivileged_def = Def
11337 val dfn'LoadHalf_def = Def
11424 val dfn'LoadHalfLiteral_def = Def
11469 val dfn'LoadHalfUnprivileged_def = Def
11542 val dfn'LoadMultiple_def = Def
11705 val dfn'LoadMultipleExceptionReturn_def = Def
11903 val dfn'LoadMultipleUserRegisters_def = Def
12045 val dfn'LoadDual_def = Def
12112 val dfn'LoadDualLiteral_def = Def
12156 val dfn'LoadExclusive_def = Def
12182 val dfn'LoadExclusiveByte_def = Def
12207 val dfn'LoadExclusiveHalf_def = Def
12232 val dfn'LoadExclusiveDoubleword_def = Def
12274 val dfn'StoreWord_def = Def
12374 val dfn'StoreUnprivileged_def = Def
12476 val dfn'StoreByte_def = Def
12543 val dfn'StoreByteUnprivileged_def = Def
12610 val dfn'StoreHalf_def = Def
12692 val dfn'StoreHalfUnprivileged_def = Def
12761 val dfn'StoreMultiple_def = Def
12938 val dfn'StoreMultipleUserRegisters_def = Def
13083 val dfn'StoreDual_def = Def
13150 val dfn'StoreExclusive_def = Def
13189 val dfn'StoreExclusiveByte_def = Def
13226 val dfn'StoreExclusiveHalf_def = Def
13263 val dfn'StoreExclusiveDoubleword_def = Def
13322 val dfn'ClearExclusive_def = Def
13326 val dfn'Swap_def = Def
13382 val dfn'ChangeProcessorState_def = Def
13503 val dfn'ExceptionReturn_def = Def
13562 val dfn'HypervisorCall_def = Def
13607 val dfn'MoveToRegisterFromSpecial_def = Def
13645 val dfn'MoveToRegisterFromBankedOrSpecial_def = Def
13917 val dfn'MoveToSpecialFromImmediate_def = Def
13951 val dfn'MoveToSpecialFromRegister_def = Def
13995 val dfn'MoveToBankedOrSpecialRegister_def = Def
14346 val dfn'ReturnFromException_def = Def
14461 val dfn'SecureMonitorCall_def = Def
14519 val dfn'SupervisorCall_def = Def
14528 val dfn'StoreReturnState_def = Def
14651 val dfn'Setend_def = Def
14664 val dfn'Undefined_def = Def
14670 val dfn'NoOperation_def = Def
14674 val dfn'Breakpoint_def = Def
14678 val dfn'Debug_def = Def
14682 val dfn'DataMemoryBarrier_def = Def
14686 val dfn'DataSynchronizationBarrier_def = Def
14690 val dfn'InstructionSynchronizationBarrier_def = Def
14694 val dfn'PreloadData_def = Def
14699 val dfn'PreloadDataLiteral_def = Def
14703 val dfn'PreloadInstruction_def = Def
14708 val dfn'SendEvent_def = Def
14712 val dfn'WaitForEvent_def = Def
14716 val dfn'WaitForInterrupt_def = Def
14720 val dfn'Yield_def = Def
14724 val Run_def = Def
15923 val Fetch_def = Def
15994 val Do_def = Def
16008 val Skip_def = Def
16016 val UndefinedARM_def = Def
16028 val UndefinedThumb_def = Def
16040 val DECODE_UNPREDICTABLE_def = Def
16071 val DecodeHint_def = Def
16177 val DecodeParallelAdditionSubtraction_def = Def
16303 val DecodeVFP_def = Def
17728 val DecodeARM_def = Def
27826 val DecodeThumb_def = Def
30650 val DecodeThumbEE_def = Def
31244 val DecodeThumb2_def = Def
42704 val Decode_def = Def
42735 val Next_def = Def
42751 val EncodeARMImmediate_aux_def = Def
42762 val EncodeARMImmediate_def = Def
42766 val EncodeImmShift_def = Def
42783 val EncodeRegShift_def = Def
42792 val EncodeAddSubOpc_def = Def
42798 val EncodeVFPImmediate_def = Def
42826 val EncodeVFPReg_def = Def
42832 val e_branch_def = Def
42904 val e_vfp_def = Def
43374 val e_data_def = Def
43489 val e_media_def = Def
43612 val e_hint_def = Def
43715 val e_system_def = Def
43834 val e_multiply_def = Def
43955 val e_simd_def = Def
44050 val e_load_def = Def
44436 val e_store_def = Def
44703 val encode_def = Def
44761 val SetPassCondition_def = Def