arm8/model/arm8Script.sml

379 val raise'exception_def = Def
389 val rec'TCR_EL1_def = Def
396 val reg'TCR_EL1_def = Def
404 val write'rec'TCR_EL1_def = Def
408 val write'reg'TCR_EL1_def = Def
412 val rec'TCR_EL2_EL3_def = Def
419 val reg'TCR_EL2_EL3_def = Def
427 val write'rec'TCR_EL2_EL3_def = Def
431 val write'reg'TCR_EL2_EL3_def = Def
435 val rec'SCTLRType_def = Def
445 val reg'SCTLRType_def = Def
459 val write'rec'SCTLRType_def = Def
463 val write'reg'SCTLRType_def = Def
467 val X_def = Def
475 val write'X_def = Def
487 val SP_def = Def
499 val write'SP_def = Def
515 val TranslationRegime_def = Def
522 val SCTLR_def = Def
530 val Hint_Branch_def = Def
538 val BranchTo_def = Def
596 val Align_def = Def
601 val Aligned_def = Def
605 val CheckSPAlignment_def = Def
628 val CheckAlignment_def = Def
655 val BigEndian_def = Def
664 val ByteList_def = Def
674 val BigEndianReverse_def = Def
678 val Mem_def = Def
721 val write'Mem_def = Def
768 val ConditionTest_def = Def
781 val ConditionHolds_def = Def
793 val Ones_def = Def ("Ones",nVar"n",Mop(PadLeft,TP[LT,nVar"n",LNL bTy]))
795 val Zeros_def = Def ("Zeros",nVar"n",Mop(PadLeft,TP[LF,nVar"n",LNL bTy]))
797 val Replicate_def = Def
802 val HighestSetBit_def = Def
807 val CountLeadingZeroBits_def = Def
813 val CountLeadingSignBits_def = Def
822 val Poly32Mod2_loop_def = Def
836 val Poly32Mod2_def = Def
844 val AddWithCarry_def = Def
862 val SetTheFlags_def = Def
899 val DecodeShift_def = Def
902 val ShiftValue_def = Def
915 val ShiftReg_def = Def
924 val ExtendWord_def = Def
929 val Extend_def = Def
935 val DecodeRegExtend_def = Def
939 val ExtendValue_def = Def
962 val ExtendReg_def = Def
971 val DecodeBitMasks_def = Def
1027 val dfn'Address_def = Def
1041 val dfn'AddSubCarry_def = Def
1072 val dfn'AddSubExtendRegister_def = Def
1118 val dfn'AddSubImmediate_def = Def
1157 val dfn'AddSubShiftedRegister_def = Def
1193 val dfn'LogicalImmediate_def = Def
1228 val dfn'LogicalShiftedRegister_def = Def
1266 val dfn'Shift_def = Def
1287 val dfn'MoveWide_def = Def
1309 val dfn'BitfieldMove_def = Def
1342 val dfn'ConditionalCompareImmediate_def = Def
1374 val dfn'ConditionalCompareRegister_def = Def
1410 val dfn'ConditionalSelect_def = Def
1438 val dfn'CountLeading_def = Def
1456 val dfn'ExtractRegister_def = Def
1478 val dfn'Division_def = Def
1497 val dfn'MultiplyAddSub_def = Def
1522 val dfn'MultiplyAddSubLong_def = Def
1550 val dfn'MultiplyHigh_def = Def
1571 val dfn'Reverse_def = Def
1634 val dfn'CRC_def = Def
1664 val dfn'BranchConditional_def = Def
1678 val dfn'BranchImmediate_def = Def
1697 val dfn'BranchRegister_def = Def
1715 val dfn'CompareAndBranch_def = Def
1729 val dfn'TestBitAndBranch_def = Def
1746 val LoadStoreSingle_def = Def
1828 val dfn'LoadStoreImmediate_def = Def
1845 val dfn'LoadStoreRegister_def = Def
1865 val dfn'LoadStorePair_def = Def
2009 val ExclusiveMonitorPass_def = Def
2012 val SetExclusiveMonitors_def = Def
2017 val dfn'LoadStoreAcquire_def = Def
2093 val dfn'LoadStoreAcquirePair_def = Def
2281 val dfn'LoadLiteral_def = Def
2306 val dfn'MemoryBarrier_def = Def
2317 val dfn'ClearExclusive_def = Def
2328 val dfn'Hint_def = Def
2341 val dfn'Breakpoint_def = Def
2352 val dfn'DebugSwitch_def = Def
2363 val dfn'DebugRestore_def = Def
2372 val dfn'Halt_def = Def
2383 val dfn'SystemInstruction_def = Def
2396 val dfn'MoveSystemRegister_def = Def
2411 val dfn'MoveImmediateProcState_def = Def
2424 val dfn'SupervisorCall_def = Def
2435 val dfn'HypervisorCall_def = Def
2446 val dfn'SecureMonitorCall_def = Def
2458 val dfn'ExceptionReturn_def = Def
2467 val dfn'Unallocated_def = Def
2476 val dfn'Reserved_def = Def
2485 val Run_def = Def
3645 val DecodeLogicalOp_def = Def
3657 val LoadStoreRegister_def = Def
3700 val LoadStoreImmediateN_def = Def
3748 val LoadStoreImmediate_def = Def
3819 val LoadStorePairN_def = Def
3845 val LoadStorePair_def = Def
3915 val LoadStoreAcquireN_def = Def
3977 val LoadStoreAcquire_def = Def
4057 val Decode_def = Def
7194 val Fetch_def = Def
7202 val Next_def = Def
7236 val EncodeBitMaskAux_def = Def
7267 val EncodeBitMask_def = Def
7293 val e_sf_def = Def
7296 val EncodeLogicalOp_def = Def
7305 val e_data_def = Def
7793 val e_debug_def = Def
7804 val e_crc_def = Def
7832 val e_branch_def = Def
7929 val e_system_def = Def
7966 val e_LoadStoreImmediate_def = Def
8034 val e_LoadStoreRegister_def = Def
8054 val e_load_store_def = Def
8465 val Encode_def = Def