riscv/model/riscvScript.sml

360 val raise'exception_def = Def
384 val archBase_def = Def
391 val architecture_def = Def
409 val archName_def = Def
416 val privLevel_def = Def
424 val privilege_def = Def
432 val privName_def = Def
440 val vmType_def = Def
463 val isValidVM_def = Def
469 val vmMode_def = Def
481 val vmModeName_def = Def
493 val ext_status_def = Def
501 val extStatus_def = Def
509 val extStatusName_def = Def
517 val interruptIndex_def = Def
523 val excCode_def = Def
538 val excType_def = Def
568 val excName_def = Def
583 val rec'mcpuid_def = Def
595 val reg'mcpuid_def = Def
612 val write'rec'mcpuid_def = Def
616 val write'reg'mcpuid_def = Def
620 val rec'mimpid_def = Def
626 val reg'mimpid_def = Def
632 val write'rec'mimpid_def = Def
636 val write'reg'mimpid_def = Def
640 val rec'mstatus_def = Def
653 val reg'mstatus_def = Def
668 val write'rec'mstatus_def = Def
672 val write'reg'mstatus_def = Def
676 val rec'mtdeleg_def = Def
682 val reg'mtdeleg_def = Def
688 val write'rec'mtdeleg_def = Def
692 val write'reg'mtdeleg_def = Def
696 val rec'mip_def = Def
705 val reg'mip_def = Def
719 val write'rec'mip_def = Def
723 val write'reg'mip_def = Def
727 val rec'mie_def = Def
736 val reg'mie_def = Def
750 val write'rec'mie_def = Def
754 val write'reg'mie_def = Def
758 val rec'mcause_def = Def
764 val reg'mcause_def = Def
770 val write'rec'mcause_def = Def
774 val write'reg'mcause_def = Def
778 val rec'sstatus_def = Def
789 val reg'sstatus_def = Def
803 val write'rec'sstatus_def = Def
807 val write'reg'sstatus_def = Def
811 val rec'sip_def = Def
818 val reg'sip_def = Def
828 val write'rec'sip_def = Def
832 val write'reg'sip_def = Def
836 val rec'sie_def = Def
843 val reg'sie_def = Def
853 val write'rec'sie_def = Def
857 val write'reg'sie_def = Def
861 val rec'FPCSR_def = Def
869 val reg'FPCSR_def = Def
879 val write'rec'FPCSR_def = Def
883 val write'reg'FPCSR_def = Def
887 val lift_mip_sip_def = Def
897 val lift_mie_sie_def = Def
907 val lower_sip_mip_def = Def
916 val lower_sie_mie_def = Def
925 val update_mstatus_def = Def
995 val lift_mstatus_sstatus_def = Def
1042 val lower_sstatus_mstatus_def = Def
1081 val popPrivilegeStack_def = Def
1105 val pushPrivilegeStack_def = Def
1130 val scheduleCore_def = Def
1137 val gpr_def = Def
1146 val write'gpr_def = Def
1162 val fcsr_def = Def
1170 val write'fcsr_def = Def
1229 val fpr_def = Def
1238 val write'fpr_def = Def
1254 val PC_def = Def
1259 val write'PC_def = Def
1270 val UCSR_def = Def
1276 val write'UCSR_def = Def
1287 val SCSR_def = Def
1293 val write'SCSR_def = Def
1305 val HCSR_def = Def
1311 val write'HCSR_def = Def
1323 val MCSR_def = Def
1329 val write'MCSR_def = Def
1340 val NextFetch_def = Def
1346 val write'NextFetch_def = Def
1359 val ReserveLoad_def = Def
1365 val write'ReserveLoad_def = Def
1376 val ExitCode_def = Def
1382 val write'ExitCode_def = Def
1393 val curArch_def = Def
1408 val in32BitMode_def = Def
1419 val curPrivilege_def = Def
1431 val curEPC_def = Def
1462 val sendIPI_def = Def
1490 val rnd_mode_static_def = Def
1501 val rnd_mode_dynamic_def = Def
1511 val l3round_def = Def
1524 val round_def = Def
1547 val FP32_IsSignalingNan_def = Def
1553 val FP64_IsSignalingNan_def = Def
1559 val FP32_Sign_def = Def
1562 val FP64_Sign_def = Def
1565 val setFP_Invalid_def = Def
1577 val setFP_DivZero_def = Def
1589 val setFP_Overflow_def = Def
1601 val setFP_Underflow_def = Def
1613 val setFP_Inexact_def = Def
1625 val csrRW_def = Def
1628 val csrPR_def = Def
1631 val check_CSR_access_def = Def
1641 val is_CSR_defined_def = Def
1763 val CSRMap_def = Def
2316 val write'CSRMap_def = Def
3206 val csrName_def = Def
3243 val Delta_def = Def
3249 val write'Delta_def = Def
3260 val hex32_def = Def
3264 val hex64_def = Def
3268 val log_w_csr_def = Def
3273 val reg_def = Def
3307 val fpreg_def = Def
3341 val log_w_gpr_def = Def
3347 val log_w_fprs_def = Def
3353 val log_w_fprd_def = Def
3359 val log_w_mem_mask_def = Def
3370 val log_w_mem_mask_misaligned_def = Def
3382 val log_w_mem_def = Def
3389 val log_r_mem_def = Def
3397 val log_exc_def = Def
3402 val log_tohost_def = Def
3407 val clear_logs_def = Def
3411 val setTrap_def = Def
3429 val signalException_def = Def
3438 val signalAddressException_def = Def
3449 val signalEnvCall_def = Def
3558 val checkPrivInterrupt_def = Def
3621 val checkInterrupts_def = Def
3786 val takeTrap_def = Def
4058 val CSR_def = Def
4065 val write'CSR_def = Def
4074 val writeCSR_def = Def
4111 val GPR_def = Def
4118 val write'GPR_def = Def
4129 val FPRS_def = Def
4136 val write'FPRS_def = Def
4148 val FPRD_def = Def
4154 val write'FPRD_def = Def
4163 val writeFPRS_def = Def
4221 val writeFPRD_def = Def
4278 val MEM_def = Def
4306 val write'MEM_def = Def
4383 val rawReadData_def = Def
4406 val rawWriteData_def = Def
4493 val rawReadInst_def = Def
4506 val rawWriteMem_def = Def
4516 val checkMemPermission_def = Def
4627 val isGlobal_def = Def
4631 val rec'SV_PTE_def = Def
4639 val reg'SV_PTE_def = Def
4651 val write'rec'SV_PTE_def = Def
4655 val write'reg'SV_PTE_def = Def
4659 val rec'SV_Vaddr_def = Def
4666 val reg'SV_Vaddr_def = Def
4675 val write'rec'SV_Vaddr_def = Def
4679 val write'reg'SV_Vaddr_def = Def
4899 val curASID_def = Def
4908 val mkTLBEntry_def = Def
4962 val lookupTLB_def = Def
5017 val addToTLB_def = Def
5324 val flushTLB_def = Def
5410 val TLB_def = Def
5416 val write'TLB_def = Def
5429 val translate64_def = Def
5562 val translateAddr_def = Def
5629 val matchLoadReservation_def = Def
5640 val branchTo_def = Def
5651 val dfn'ADDI_def = Def
5664 val dfn'ADDIW_def = Def
5687 val dfn'SLTI_def = Def
5711 val dfn'SLTIU_def = Def
5735 val dfn'ANDI_def = Def
5748 val dfn'ORI_def = Def
5761 val dfn'XORI_def = Def
5774 val dfn'SLLI_def = Def
5794 val dfn'SRLI_def = Def
5826 val dfn'SRAI_def = Def
5858 val dfn'SLLIW_def = Def
5881 val dfn'SRLIW_def = Def
5904 val dfn'SRAIW_def = Def
5927 val dfn'LUI_def = Def
5937 val dfn'AUIPC_def = Def
5948 val dfn'ADD_def = Def
5963 val dfn'ADDW_def = Def
5990 val dfn'SUB_def = Def
6005 val dfn'SUBW_def = Def
6032 val dfn'SLT_def = Def
6069 val dfn'SLTU_def = Def
6106 val dfn'AND_def = Def
6121 val dfn'OR_def = Def
6136 val dfn'XOR_def = Def
6151 val dfn'SLL_def = Def
6185 val dfn'SLLW_def = Def
6214 val dfn'SRL_def = Def
6252 val dfn'SRLW_def = Def
6281 val dfn'SRA_def = Def
6319 val dfn'SRAW_def = Def
6348 val dfn'MUL_def = Def
6363 val dfn'MULH_def = Def
6411 val dfn'MULHU_def = Def
6455 val dfn'MULHSU_def = Def
6499 val dfn'MULW_def = Def
6528 val dfn'DIV_def = Def
6549 val dfn'REM_def = Def
6572 val dfn'DIVU_def = Def
6613 val dfn'REMU_def = Def
6636 val dfn'DIVW_def = Def
6669 val dfn'REMW_def = Def
6701 val dfn'DIVUW_def = Def
6734 val dfn'REMUW_def = Def
6766 val dfn'JAL_def = Def
6788 val dfn'JALR_def = Def
6813 val dfn'BEQ_def = Def
6846 val dfn'BNE_def = Def
6882 val dfn'BLT_def = Def
6916 val dfn'BLTU_def = Def
6950 val dfn'BGE_def = Def
6984 val dfn'BGEU_def = Def
7018 val dfn'LW_def = Def
7050 val dfn'LWU_def = Def
7092 val dfn'LH_def = Def
7124 val dfn'LHU_def = Def
7156 val dfn'LB_def = Def
7188 val dfn'LBU_def = Def
7220 val dfn'LD_def = Def
7259 val dfn'SW_def = Def
7289 val dfn'SH_def = Def
7319 val dfn'SB_def = Def
7349 val dfn'SD_def = Def
7390 val dfn'FENCE_def = Def
7394 val dfn'FENCE_I_def = Def
7397 val dfn'LR_W_def = Def
7440 val dfn'LR_D_def = Def
7489 val dfn'SC_W_def = Def
7542 val dfn'SC_D_def = Def
7607 val dfn'AMOSWAP_W_def = Def
7655 val dfn'AMOSWAP_D_def = Def
7700 val dfn'AMOADD_W_def = Def
7751 val dfn'AMOADD_D_def = Def
7800 val dfn'AMOXOR_W_def = Def
7851 val dfn'AMOXOR_D_def = Def
7900 val dfn'AMOAND_W_def = Def
7951 val dfn'AMOAND_D_def = Def
8000 val dfn'AMOOR_W_def = Def
8051 val dfn'AMOOR_D_def = Def
8100 val dfn'AMOMIN_W_def = Def
8151 val dfn'AMOMIN_D_def = Def
8200 val dfn'AMOMAX_W_def = Def
8251 val dfn'AMOMAX_D_def = Def
8300 val dfn'AMOMINU_W_def = Def
8351 val dfn'AMOMINU_D_def = Def
8400 val dfn'AMOMAXU_W_def = Def
8451 val dfn'AMOMAXU_D_def = Def
8500 val dfn'FLW_def = Def
8531 val dfn'FSW_def = Def
8563 val dfn'FADD_S_def = Def
8589 val dfn'FSUB_S_def = Def
8615 val dfn'FMUL_S_def = Def
8641 val dfn'FDIV_S_def = Def
8667 val dfn'FSQRT_S_def = Def
8689 val dfn'FMIN_S_def = Def
8728 val dfn'FMAX_S_def = Def
8767 val dfn'FMADD_S_def = Def
8801 val dfn'FMSUB_S_def = Def
8835 val dfn'FNMADD_S_def = Def
8871 val dfn'FNMSUB_S_def = Def
8907 val dfn'FCVT_S_W_def = Def
8932 val dfn'FCVT_S_WU_def = Def
8958 val dfn'FCVT_W_S_def = Def
8996 val dfn'FCVT_WU_S_def = Def
9029 val dfn'FCVT_S_L_def = Def
9052 val dfn'FCVT_S_LU_def = Def
9077 val dfn'FCVT_L_S_def = Def
9115 val dfn'FCVT_LU_S_def = Def
9148 val dfn'FSGNJ_S_def = Def
9166 val dfn'FSGNJN_S_def = Def
9185 val dfn'FSGNJX_S_def = Def
9206 val dfn'FMV_X_S_def = Def
9218 val dfn'FMV_S_X_def = Def
9230 val dfn'FEQ_S_def = Def
9257 val dfn'FLT_S_def = Def
9284 val dfn'FLE_S_def = Def
9311 val dfn'FCLASS_S_def = Def
9392 val dfn'FLD_def = Def
9423 val dfn'FSD_def = Def
9453 val dfn'FADD_D_def = Def
9479 val dfn'FSUB_D_def = Def
9505 val dfn'FMUL_D_def = Def
9531 val dfn'FDIV_D_def = Def
9557 val dfn'FSQRT_D_def = Def
9579 val dfn'FMIN_D_def = Def
9618 val dfn'FMAX_D_def = Def
9657 val dfn'FMADD_D_def = Def
9691 val dfn'FMSUB_D_def = Def
9725 val dfn'FNMADD_D_def = Def
9761 val dfn'FNMSUB_D_def = Def
9797 val dfn'FCVT_D_W_def = Def
9822 val dfn'FCVT_D_WU_def = Def
9848 val dfn'FCVT_W_D_def = Def
9886 val dfn'FCVT_WU_D_def = Def
9919 val dfn'FCVT_D_L_def = Def
9942 val dfn'FCVT_D_LU_def = Def
9967 val dfn'FCVT_L_D_def = Def
10005 val dfn'FCVT_LU_D_def = Def
10038 val dfn'FCVT_S_D_def = Def
10060 val dfn'FCVT_D_S_def = Def
10081 val dfn'FSGNJ_D_def = Def
10099 val dfn'FSGNJN_D_def = Def
10118 val dfn'FSGNJX_D_def = Def
10139 val dfn'FMV_X_D_def = Def
10151 val dfn'FMV_D_X_def = Def
10162 val dfn'FEQ_D_def = Def
10189 val dfn'FLT_D_def = Def
10216 val dfn'FLE_D_def = Def
10243 val dfn'FCLASS_D_def = Def
10324 val dfn'ECALL_def = Def
10328 val dfn'EBREAK_def = Def
10335 val dfn'ERET_def = Def
10342 val dfn'MRTS_def = Def
10416 val checkCSROp_def = Def
10435 val dfn'CSRRW_def = Def
10466 val dfn'CSRRS_def = Def
10503 val dfn'CSRRC_def = Def
10541 val dfn'CSRRWI_def = Def
10574 val dfn'CSRRSI_def = Def
10608 val dfn'CSRRCI_def = Def
10643 val dfn'SFENCE_VM_def = Def
10662 val dfn'UnknownInstruction_def = Def
10669 val dfn'FETCH_MISALIGNED_def = Def
10679 val dfn'FETCH_FAULT_def = Def
10689 val Run_def = Def
11881 val Fetch_def = Def
12088 val asImm12_def = Def
12093 val asImm20_def = Def
12098 val asSImm12_def = Def
12102 val Decode_def = Def
17498 val imm_def = Def
17501 val instr_def = Def
17504 val amotype_def = Def
17510 val pRtype_def = Def
17516 val pARtype_def = Def
17525 val pLRtype_def = Def
17534 val pItype_def = Def
17540 val pCSRtype_def = Def
17547 val pCSRItype_def = Def
17554 val pStype_def = Def
17560 val pSBtype_def = Def
17567 val pUtype_def = Def
17572 val pUJtype_def = Def
17577 val pN0type_def = Def ("pN0type",sVar"o",Call("instr",sTy,sVar"o"))
17579 val pN1type_def = Def
17583 val pFRtype_def = Def
17590 val pFR1type_def = Def
17595 val pFR3type_def = Def
17604 val pFItype_def = Def
17610 val pFStype_def = Def
17617 val pCFItype_def = Def
17622 val pCIFtype_def = Def
17627 val instructionToString_def = Def
18914 val Rtype_def = Def
18921 val R4type_def = Def
18928 val Itype_def = Def
18935 val Stype_def = Def
18943 val SBtype_def = Def
18952 val Utype_def = Def
18956 val UJtype_def = Def
18963 val opc_def = Def
18966 val amofunc_def = Def
18970 val Encode_def = Def
20433 val log_instruction_def = Def
20447 val exitCode_def = Def
20455 val tickClock_def = Def
20475 val incrInstret_def = Def
20490 val checkTimers_def = Def
20549 val Next_def = Def
20790 val initIdent_def = Def
20924 val initMachine_def = Def
21079 val initRegs_def = Def