1(* riscv - generated by L3 - Mon Sep 18 10:41:50 2017 *) 2 3signature riscv = 4sig 5 6structure Map : Map 7 8(* ------------------------------------------------------------------------- 9 Types 10 ------------------------------------------------------------------------- *) 11 12datatype accessType = Read | Write 13 14datatype fetchType = Instruction | Data 15 16datatype Architecture = RV32I | RV64I | RV128I 17 18datatype Privilege = User | Supervisor | Hypervisor | Machine 19 20datatype VM_Mode = Mbare | Mbb | Mbbid | Sv32 | Sv39 | Sv48 | Sv57 | Sv64 21 22datatype ExtStatus = Off | Initial | Clean | Dirty 23 24datatype Interrupt = Software | Timer 25 26datatype ExceptionType 27 = Fetch_Misaligned | Fetch_Fault | Illegal_Instr | Breakpoint 28 | Load_Fault | AMO_Misaligned | Store_AMO_Fault | UMode_Env_Call 29 | SMode_Env_Call | HMode_Env_Call | MMode_Env_Call 30 31type mcpuid = 32 { ArchBase: BitsN.nbit, I: bool, M: bool, S: bool, U: bool, 33 mcpuid'rst: BitsN.nbit } 34 35type mimpid = { RVImpl: BitsN.nbit, RVSource: BitsN.nbit } 36 37type mstatus = 38 { MFS: BitsN.nbit, MIE: bool, MIE1: bool, MIE2: bool, MIE3: bool, 39 MMPRV: bool, MPRV: BitsN.nbit, MPRV1: BitsN.nbit, MPRV2: BitsN.nbit, 40 MPRV3: BitsN.nbit, MSD: bool, MXS: BitsN.nbit, VM: BitsN.nbit, 41 mstatus'rst: BitsN.nbit } 42 43type mtdeleg = { Exc_deleg: BitsN.nbit, Intr_deleg: BitsN.nbit } 44 45type mip = 46 { HSIP: bool, HTIP: bool, MSIP: bool, MTIP: bool, SSIP: bool, 47 STIP: bool, mip'rst: BitsN.nbit } 48 49type mie = 50 { HSIE: bool, HTIE: bool, MSIE: bool, MTIE: bool, SSIE: bool, 51 STIE: bool, mie'rst: BitsN.nbit } 52 53type mcause = { EC: BitsN.nbit, Int: bool, mcause'rst: BitsN.nbit } 54 55type MachineCSR = 56 { mbadaddr: BitsN.nbit, mbase: BitsN.nbit, mbound: BitsN.nbit, 57 mcause: mcause, mcpuid: mcpuid, mdbase: BitsN.nbit, 58 mdbound: BitsN.nbit, mepc: BitsN.nbit, mfromhost: BitsN.nbit, 59 mhartid: BitsN.nbit, mibase: BitsN.nbit, mibound: BitsN.nbit, 60 mie: mie, mimpid: mimpid, mip: mip, mscratch: BitsN.nbit, 61 mstatus: mstatus, mtdeleg: mtdeleg, mtime_delta: BitsN.nbit, 62 mtimecmp: BitsN.nbit, mtohost: BitsN.nbit, mtvec: BitsN.nbit } 63 64type HypervisorCSR = 65 { hbadaddr: BitsN.nbit, hcause: mcause, hepc: BitsN.nbit, 66 hscratch: BitsN.nbit, hstatus: mstatus, htdeleg: mtdeleg, 67 htime_delta: BitsN.nbit, htimecmp: BitsN.nbit, htvec: BitsN.nbit } 68 69type sstatus = 70 { SFS: BitsN.nbit, SIE: bool, SMPRV: bool, SPIE: bool, SPS: bool, 71 SSD: bool, SXS: BitsN.nbit, sstatus'rst: BitsN.nbit } 72 73type sip = { SSIP: bool, STIP: bool, sip'rst: BitsN.nbit } 74 75type sie = { SSIE: bool, STIE: bool, sie'rst: BitsN.nbit } 76 77type SupervisorCSR = 78 { sasid: BitsN.nbit, sbadaddr: BitsN.nbit, scause: mcause, 79 sepc: BitsN.nbit, sptbr: BitsN.nbit, sscratch: BitsN.nbit, 80 stime_delta: BitsN.nbit, stimecmp: BitsN.nbit, stvec: BitsN.nbit } 81 82type FPCSR = 83 { DZ: bool, FRM: BitsN.nbit, NV: bool, NX: bool, OF: bool, UF: bool, 84 fpcsr'rst: BitsN.nbit } 85 86type UserCSR = 87 { cycle_delta: BitsN.nbit, fpcsr: FPCSR, instret_delta: BitsN.nbit, 88 time_delta: BitsN.nbit } 89 90type SynchronousTrap = { badaddr: BitsN.nbit option, trap: ExceptionType } 91 92datatype TransferControl 93 = BranchTo of BitsN.nbit | Ereturn | Mrts | Trap of SynchronousTrap 94 95datatype Rounding = RNE | RTZ | RDN | RUP | RMM | RDYN 96 97type StateDelta = 98 { addr: BitsN.nbit option, data1: BitsN.nbit option, 99 data2: BitsN.nbit option, exc_taken: bool, fetch_exc: bool, 100 fp_data: BitsN.nbit option, pc: BitsN.nbit, rinstr: BitsN.nbit, 101 st_width: BitsN.nbit option } 102 103type SV_PTE = 104 { PTE_D: bool, PTE_PPNi: BitsN.nbit, PTE_R: bool, PTE_SW: BitsN.nbit, 105 PTE_T: BitsN.nbit, PTE_V: bool, sv_pte'rst: BitsN.nbit } 106 107type SV_Vaddr = 108 { Sv_PgOfs: BitsN.nbit, Sv_VPNi: BitsN.nbit, sv_vaddr'rst: BitsN.nbit } 109 110type TLBEntry = 111 { age: BitsN.nbit, asid: BitsN.nbit, global: bool, pAddr: BitsN.nbit, 112 pte: SV_PTE, pteAddr: BitsN.nbit, vAddr: BitsN.nbit, 113 vAddrMask: BitsN.nbit, vMatchMask: BitsN.nbit } 114 115datatype Internal 116 = FETCH_FAULT of BitsN.nbit | FETCH_MISALIGNED of BitsN.nbit 117 118datatype System 119 = CSRRC of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 120 | CSRRCI of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 121 | CSRRS of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 122 | CSRRSI of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 123 | CSRRW of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 124 | CSRRWI of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 125 | EBREAK 126 | ECALL 127 | ERET 128 | MRTS 129 | SFENCE_VM of BitsN.nbit 130 | WFI 131 132datatype FConv 133 = FCLASS_D of BitsN.nbit * BitsN.nbit 134 | FCLASS_S of BitsN.nbit * BitsN.nbit 135 | FCVT_D_L of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 136 | FCVT_D_LU of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 137 | FCVT_D_S of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 138 | FCVT_D_W of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 139 | FCVT_D_WU of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 140 | FCVT_LU_D of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 141 | FCVT_LU_S of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 142 | FCVT_L_D of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 143 | FCVT_L_S of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 144 | FCVT_S_D of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 145 | FCVT_S_L of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 146 | FCVT_S_LU of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 147 | FCVT_S_W of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 148 | FCVT_S_WU of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 149 | FCVT_WU_D of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 150 | FCVT_WU_S of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 151 | FCVT_W_D of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 152 | FCVT_W_S of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 153 | FMV_D_X of BitsN.nbit * BitsN.nbit 154 | FMV_S_X of BitsN.nbit * BitsN.nbit 155 | FMV_X_D of BitsN.nbit * BitsN.nbit 156 | FMV_X_S of BitsN.nbit * BitsN.nbit 157 | FSGNJN_D of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 158 | FSGNJN_S of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 159 | FSGNJX_D of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 160 | FSGNJX_S of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 161 | FSGNJ_D of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 162 | FSGNJ_S of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 163 164datatype FArith 165 = FADD_D of BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) 166 | FADD_S of BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) 167 | FDIV_D of BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) 168 | FDIV_S of BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) 169 | FEQ_D of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 170 | FEQ_S of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 171 | FLE_D of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 172 | FLE_S of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 173 | FLT_D of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 174 | FLT_S of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 175 | FMADD_D of 176 BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) 177 | FMADD_S of 178 BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) 179 | FMAX_D of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 180 | FMAX_S of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 181 | FMIN_D of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 182 | FMIN_S of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 183 | FMSUB_D of 184 BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) 185 | FMSUB_S of 186 BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) 187 | FMUL_D of BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) 188 | FMUL_S of BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) 189 | FNMADD_D of 190 BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) 191 | FNMADD_S of 192 BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) 193 | FNMSUB_D of 194 BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) 195 | FNMSUB_S of 196 BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) 197 | FSQRT_D of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 198 | FSQRT_S of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 199 | FSUB_D of BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) 200 | FSUB_S of BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) 201 202datatype FPStore 203 = FSD of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 204 | FSW of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 205 206datatype FPLoad 207 = FLD of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 208 | FLW of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 209 210datatype AMO 211 = AMOADD_D of 212 BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) 213 | AMOADD_W of 214 BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) 215 | AMOAND_D of 216 BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) 217 | AMOAND_W of 218 BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) 219 | AMOMAXU_D of 220 BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) 221 | AMOMAXU_W of 222 BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) 223 | AMOMAX_D of 224 BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) 225 | AMOMAX_W of 226 BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) 227 | AMOMINU_D of 228 BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) 229 | AMOMINU_W of 230 BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) 231 | AMOMIN_D of 232 BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) 233 | AMOMIN_W of 234 BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) 235 | AMOOR_D of 236 BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) 237 | AMOOR_W of 238 BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) 239 | AMOSWAP_D of 240 BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) 241 | AMOSWAP_W of 242 BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) 243 | AMOXOR_D of 244 BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) 245 | AMOXOR_W of 246 BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) 247 | LR_D of BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) 248 | LR_W of BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) 249 | SC_D of 250 BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) 251 | SC_W of 252 BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) 253 254datatype Store 255 = SB of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 256 | SD of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 257 | SH of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 258 | SW of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 259 260datatype Load 261 = LB of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 262 | LBU of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 263 | LD of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 264 | LH of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 265 | LHU of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 266 | LW of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 267 | LWU of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 268 269datatype Branch 270 = BEQ of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 271 | BGE of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 272 | BGEU of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 273 | BLT of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 274 | BLTU of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 275 | BNE of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 276 | JAL of BitsN.nbit * BitsN.nbit 277 | JALR of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 278 279datatype MulDiv 280 = DIV of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 281 | DIVU of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 282 | DIVUW of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 283 | DIVW of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 284 | MUL of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 285 | MULH of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 286 | MULHSU of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 287 | MULHU of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 288 | MULW of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 289 | REM of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 290 | REMU of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 291 | REMUW of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 292 | REMW of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 293 294datatype Shift 295 = SLL of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 296 | SLLI of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 297 | SLLIW of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 298 | SLLW of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 299 | SRA of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 300 | SRAI of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 301 | SRAIW of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 302 | SRAW of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 303 | SRL of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 304 | SRLI of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 305 | SRLIW of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 306 | SRLW of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 307 308datatype ArithR 309 = ADD of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 310 | ADDW of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 311 | AND of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 312 | OR of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 313 | SLT of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 314 | SLTU of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 315 | SUB of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 316 | SUBW of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 317 | XOR of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 318 319datatype ArithI 320 = ADDI of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 321 | ADDIW of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 322 | ANDI of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 323 | AUIPC of BitsN.nbit * BitsN.nbit 324 | LUI of BitsN.nbit * BitsN.nbit 325 | ORI of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 326 | SLTI of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 327 | SLTIU of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 328 | XORI of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 329 330datatype instruction 331 = AMO of AMO 332 | ArithI of ArithI 333 | ArithR of ArithR 334 | Branch of Branch 335 | FArith of FArith 336 | FConv of FConv 337 | FENCE of BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) 338 | FENCE_I of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 339 | FPLoad of FPLoad 340 | FPStore of FPStore 341 | Internal of Internal 342 | Load of Load 343 | MulDiv of MulDiv 344 | Shift of Shift 345 | Store of Store 346 | System of System 347 | UnknownInstruction 348 349datatype FetchResult = F_Error of instruction | F_Result of BitsN.nbit 350 351(* ------------------------------------------------------------------------- 352 Exceptions 353 ------------------------------------------------------------------------- *) 354 355exception INTERNAL_ERROR of string 356 357exception UNDEFINED of string 358 359(* ------------------------------------------------------------------------- 360 Functions 361 ------------------------------------------------------------------------- *) 362 363structure Cast: 364sig 365 366val natToaccessType: Nat.nat -> accessType 367val accessTypeToNat: accessType -> Nat.nat 368val stringToaccessType: string -> accessType 369val accessTypeToString: accessType -> string 370val natTofetchType: Nat.nat -> fetchType 371val fetchTypeToNat: fetchType -> Nat.nat 372val stringTofetchType: string -> fetchType 373val fetchTypeToString: fetchType -> string 374val natToArchitecture: Nat.nat -> Architecture 375val ArchitectureToNat: Architecture -> Nat.nat 376val stringToArchitecture: string -> Architecture 377val ArchitectureToString: Architecture -> string 378val natToPrivilege: Nat.nat -> Privilege 379val PrivilegeToNat: Privilege -> Nat.nat 380val stringToPrivilege: string -> Privilege 381val PrivilegeToString: Privilege -> string 382val natToVM_Mode: Nat.nat -> VM_Mode 383val VM_ModeToNat: VM_Mode -> Nat.nat 384val stringToVM_Mode: string -> VM_Mode 385val VM_ModeToString: VM_Mode -> string 386val natToExtStatus: Nat.nat -> ExtStatus 387val ExtStatusToNat: ExtStatus -> Nat.nat 388val stringToExtStatus: string -> ExtStatus 389val ExtStatusToString: ExtStatus -> string 390val natToInterrupt: Nat.nat -> Interrupt 391val InterruptToNat: Interrupt -> Nat.nat 392val stringToInterrupt: string -> Interrupt 393val InterruptToString: Interrupt -> string 394val natToExceptionType: Nat.nat -> ExceptionType 395val ExceptionTypeToNat: ExceptionType -> Nat.nat 396val stringToExceptionType: string -> ExceptionType 397val ExceptionTypeToString: ExceptionType -> string 398val natToRounding: Nat.nat -> Rounding 399val RoundingToNat: Rounding -> Nat.nat 400val stringToRounding: string -> Rounding 401val RoundingToString: Rounding -> string 402 403end 404 405val MEM8: (BitsN.nbit Map.map) ref 406val c_ExitCode: (BitsN.nbit Map.map) ref 407val c_HCSR: (HypervisorCSR Map.map) ref 408val c_MCSR: (MachineCSR Map.map) ref 409val c_NextFetch: ((TransferControl option) Map.map) ref 410val c_PC: (BitsN.nbit Map.map) ref 411val c_ReserveLoad: ((BitsN.nbit option) Map.map) ref 412val c_SCSR: (SupervisorCSR Map.map) ref 413val c_UCSR: (UserCSR Map.map) ref 414val c_cycles: (BitsN.nbit Map.map) ref 415val c_fpr: ((BitsN.nbit Map.map) Map.map) ref 416val c_gpr: ((BitsN.nbit Map.map) Map.map) ref 417val c_instret: (BitsN.nbit Map.map) ref 418val c_tlb: (((TLBEntry option) Map.map) Map.map) ref 419val c_update: (StateDelta Map.map) ref 420val clock: BitsN.nbit ref 421val done: bool ref 422val log: ((Nat.nat * string) list) ref 423val procID: BitsN.nbit ref 424val totalCore: Nat.nat ref 425val mcpuid_ArchBase_rupd: mcpuid * BitsN.nbit -> mcpuid 426val mcpuid_I_rupd: mcpuid * bool -> mcpuid 427val mcpuid_M_rupd: mcpuid * bool -> mcpuid 428val mcpuid_S_rupd: mcpuid * bool -> mcpuid 429val mcpuid_U_rupd: mcpuid * bool -> mcpuid 430val mcpuid_mcpuid'rst_rupd: mcpuid * BitsN.nbit -> mcpuid 431val mimpid_RVImpl_rupd: mimpid * BitsN.nbit -> mimpid 432val mimpid_RVSource_rupd: mimpid * BitsN.nbit -> mimpid 433val mstatus_MFS_rupd: mstatus * BitsN.nbit -> mstatus 434val mstatus_MIE_rupd: mstatus * bool -> mstatus 435val mstatus_MIE1_rupd: mstatus * bool -> mstatus 436val mstatus_MIE2_rupd: mstatus * bool -> mstatus 437val mstatus_MIE3_rupd: mstatus * bool -> mstatus 438val mstatus_MMPRV_rupd: mstatus * bool -> mstatus 439val mstatus_MPRV_rupd: mstatus * BitsN.nbit -> mstatus 440val mstatus_MPRV1_rupd: mstatus * BitsN.nbit -> mstatus 441val mstatus_MPRV2_rupd: mstatus * BitsN.nbit -> mstatus 442val mstatus_MPRV3_rupd: mstatus * BitsN.nbit -> mstatus 443val mstatus_MSD_rupd: mstatus * bool -> mstatus 444val mstatus_MXS_rupd: mstatus * BitsN.nbit -> mstatus 445val mstatus_VM_rupd: mstatus * BitsN.nbit -> mstatus 446val mstatus_mstatus'rst_rupd: mstatus * BitsN.nbit -> mstatus 447val mtdeleg_Exc_deleg_rupd: mtdeleg * BitsN.nbit -> mtdeleg 448val mtdeleg_Intr_deleg_rupd: mtdeleg * BitsN.nbit -> mtdeleg 449val mip_HSIP_rupd: mip * bool -> mip 450val mip_HTIP_rupd: mip * bool -> mip 451val mip_MSIP_rupd: mip * bool -> mip 452val mip_MTIP_rupd: mip * bool -> mip 453val mip_SSIP_rupd: mip * bool -> mip 454val mip_STIP_rupd: mip * bool -> mip 455val mip_mip'rst_rupd: mip * BitsN.nbit -> mip 456val mie_HSIE_rupd: mie * bool -> mie 457val mie_HTIE_rupd: mie * bool -> mie 458val mie_MSIE_rupd: mie * bool -> mie 459val mie_MTIE_rupd: mie * bool -> mie 460val mie_SSIE_rupd: mie * bool -> mie 461val mie_STIE_rupd: mie * bool -> mie 462val mie_mie'rst_rupd: mie * BitsN.nbit -> mie 463val mcause_EC_rupd: mcause * BitsN.nbit -> mcause 464val mcause_Int_rupd: mcause * bool -> mcause 465val mcause_mcause'rst_rupd: mcause * BitsN.nbit -> mcause 466val MachineCSR_mbadaddr_rupd: MachineCSR * BitsN.nbit -> MachineCSR 467val MachineCSR_mbase_rupd: MachineCSR * BitsN.nbit -> MachineCSR 468val MachineCSR_mbound_rupd: MachineCSR * BitsN.nbit -> MachineCSR 469val MachineCSR_mcause_rupd: MachineCSR * mcause -> MachineCSR 470val MachineCSR_mcpuid_rupd: MachineCSR * mcpuid -> MachineCSR 471val MachineCSR_mdbase_rupd: MachineCSR * BitsN.nbit -> MachineCSR 472val MachineCSR_mdbound_rupd: MachineCSR * BitsN.nbit -> MachineCSR 473val MachineCSR_mepc_rupd: MachineCSR * BitsN.nbit -> MachineCSR 474val MachineCSR_mfromhost_rupd: MachineCSR * BitsN.nbit -> MachineCSR 475val MachineCSR_mhartid_rupd: MachineCSR * BitsN.nbit -> MachineCSR 476val MachineCSR_mibase_rupd: MachineCSR * BitsN.nbit -> MachineCSR 477val MachineCSR_mibound_rupd: MachineCSR * BitsN.nbit -> MachineCSR 478val MachineCSR_mie_rupd: MachineCSR * mie -> MachineCSR 479val MachineCSR_mimpid_rupd: MachineCSR * mimpid -> MachineCSR 480val MachineCSR_mip_rupd: MachineCSR * mip -> MachineCSR 481val MachineCSR_mscratch_rupd: MachineCSR * BitsN.nbit -> MachineCSR 482val MachineCSR_mstatus_rupd: MachineCSR * mstatus -> MachineCSR 483val MachineCSR_mtdeleg_rupd: MachineCSR * mtdeleg -> MachineCSR 484val MachineCSR_mtime_delta_rupd: MachineCSR * BitsN.nbit -> MachineCSR 485val MachineCSR_mtimecmp_rupd: MachineCSR * BitsN.nbit -> MachineCSR 486val MachineCSR_mtohost_rupd: MachineCSR * BitsN.nbit -> MachineCSR 487val MachineCSR_mtvec_rupd: MachineCSR * BitsN.nbit -> MachineCSR 488val HypervisorCSR_hbadaddr_rupd: 489 HypervisorCSR * BitsN.nbit -> HypervisorCSR 490val HypervisorCSR_hcause_rupd: HypervisorCSR * mcause -> HypervisorCSR 491val HypervisorCSR_hepc_rupd: HypervisorCSR * BitsN.nbit -> HypervisorCSR 492val HypervisorCSR_hscratch_rupd: 493 HypervisorCSR * BitsN.nbit -> HypervisorCSR 494val HypervisorCSR_hstatus_rupd: HypervisorCSR * mstatus -> HypervisorCSR 495val HypervisorCSR_htdeleg_rupd: HypervisorCSR * mtdeleg -> HypervisorCSR 496val HypervisorCSR_htime_delta_rupd: 497 HypervisorCSR * BitsN.nbit -> HypervisorCSR 498val HypervisorCSR_htimecmp_rupd: 499 HypervisorCSR * BitsN.nbit -> HypervisorCSR 500val HypervisorCSR_htvec_rupd: HypervisorCSR * BitsN.nbit -> HypervisorCSR 501val sstatus_SFS_rupd: sstatus * BitsN.nbit -> sstatus 502val sstatus_SIE_rupd: sstatus * bool -> sstatus 503val sstatus_SMPRV_rupd: sstatus * bool -> sstatus 504val sstatus_SPIE_rupd: sstatus * bool -> sstatus 505val sstatus_SPS_rupd: sstatus * bool -> sstatus 506val sstatus_SSD_rupd: sstatus * bool -> sstatus 507val sstatus_SXS_rupd: sstatus * BitsN.nbit -> sstatus 508val sstatus_sstatus'rst_rupd: sstatus * BitsN.nbit -> sstatus 509val sip_SSIP_rupd: sip * bool -> sip 510val sip_STIP_rupd: sip * bool -> sip 511val sip_sip'rst_rupd: sip * BitsN.nbit -> sip 512val sie_SSIE_rupd: sie * bool -> sie 513val sie_STIE_rupd: sie * bool -> sie 514val sie_sie'rst_rupd: sie * BitsN.nbit -> sie 515val SupervisorCSR_sasid_rupd: SupervisorCSR * BitsN.nbit -> SupervisorCSR 516val SupervisorCSR_sbadaddr_rupd: 517 SupervisorCSR * BitsN.nbit -> SupervisorCSR 518val SupervisorCSR_scause_rupd: SupervisorCSR * mcause -> SupervisorCSR 519val SupervisorCSR_sepc_rupd: SupervisorCSR * BitsN.nbit -> SupervisorCSR 520val SupervisorCSR_sptbr_rupd: SupervisorCSR * BitsN.nbit -> SupervisorCSR 521val SupervisorCSR_sscratch_rupd: 522 SupervisorCSR * BitsN.nbit -> SupervisorCSR 523val SupervisorCSR_stime_delta_rupd: 524 SupervisorCSR * BitsN.nbit -> SupervisorCSR 525val SupervisorCSR_stimecmp_rupd: 526 SupervisorCSR * BitsN.nbit -> SupervisorCSR 527val SupervisorCSR_stvec_rupd: SupervisorCSR * BitsN.nbit -> SupervisorCSR 528val FPCSR_DZ_rupd: FPCSR * bool -> FPCSR 529val FPCSR_FRM_rupd: FPCSR * BitsN.nbit -> FPCSR 530val FPCSR_NV_rupd: FPCSR * bool -> FPCSR 531val FPCSR_NX_rupd: FPCSR * bool -> FPCSR 532val FPCSR_OF_rupd: FPCSR * bool -> FPCSR 533val FPCSR_UF_rupd: FPCSR * bool -> FPCSR 534val FPCSR_fpcsr'rst_rupd: FPCSR * BitsN.nbit -> FPCSR 535val UserCSR_cycle_delta_rupd: UserCSR * BitsN.nbit -> UserCSR 536val UserCSR_fpcsr_rupd: UserCSR * FPCSR -> UserCSR 537val UserCSR_instret_delta_rupd: UserCSR * BitsN.nbit -> UserCSR 538val UserCSR_time_delta_rupd: UserCSR * BitsN.nbit -> UserCSR 539val SynchronousTrap_badaddr_rupd: 540 SynchronousTrap * (BitsN.nbit option) -> SynchronousTrap 541val SynchronousTrap_trap_rupd: 542 SynchronousTrap * ExceptionType -> SynchronousTrap 543val StateDelta_addr_rupd: StateDelta * (BitsN.nbit option) -> StateDelta 544val StateDelta_data1_rupd: StateDelta * (BitsN.nbit option) -> StateDelta 545val StateDelta_data2_rupd: StateDelta * (BitsN.nbit option) -> StateDelta 546val StateDelta_exc_taken_rupd: StateDelta * bool -> StateDelta 547val StateDelta_fetch_exc_rupd: StateDelta * bool -> StateDelta 548val StateDelta_fp_data_rupd: 549 StateDelta * (BitsN.nbit option) -> StateDelta 550val StateDelta_pc_rupd: StateDelta * BitsN.nbit -> StateDelta 551val StateDelta_rinstr_rupd: StateDelta * BitsN.nbit -> StateDelta 552val StateDelta_st_width_rupd: 553 StateDelta * (BitsN.nbit option) -> StateDelta 554val SV_PTE_PTE_D_rupd: SV_PTE * bool -> SV_PTE 555val SV_PTE_PTE_PPNi_rupd: SV_PTE * BitsN.nbit -> SV_PTE 556val SV_PTE_PTE_R_rupd: SV_PTE * bool -> SV_PTE 557val SV_PTE_PTE_SW_rupd: SV_PTE * BitsN.nbit -> SV_PTE 558val SV_PTE_PTE_T_rupd: SV_PTE * BitsN.nbit -> SV_PTE 559val SV_PTE_PTE_V_rupd: SV_PTE * bool -> SV_PTE 560val SV_PTE_sv_pte'rst_rupd: SV_PTE * BitsN.nbit -> SV_PTE 561val SV_Vaddr_Sv_PgOfs_rupd: SV_Vaddr * BitsN.nbit -> SV_Vaddr 562val SV_Vaddr_Sv_VPNi_rupd: SV_Vaddr * BitsN.nbit -> SV_Vaddr 563val SV_Vaddr_sv_vaddr'rst_rupd: SV_Vaddr * BitsN.nbit -> SV_Vaddr 564val TLBEntry_age_rupd: TLBEntry * BitsN.nbit -> TLBEntry 565val TLBEntry_asid_rupd: TLBEntry * BitsN.nbit -> TLBEntry 566val TLBEntry_global_rupd: TLBEntry * bool -> TLBEntry 567val TLBEntry_pAddr_rupd: TLBEntry * BitsN.nbit -> TLBEntry 568val TLBEntry_pte_rupd: TLBEntry * SV_PTE -> TLBEntry 569val TLBEntry_pteAddr_rupd: TLBEntry * BitsN.nbit -> TLBEntry 570val TLBEntry_vAddr_rupd: TLBEntry * BitsN.nbit -> TLBEntry 571val TLBEntry_vAddrMask_rupd: TLBEntry * BitsN.nbit -> TLBEntry 572val TLBEntry_vMatchMask_rupd: TLBEntry * BitsN.nbit -> TLBEntry 573val boolify'32: 574 BitsN.nbit -> 575 bool * 576 (bool * 577 (bool * 578 (bool * 579 (bool * 580 (bool * 581 (bool * 582 (bool * 583 (bool * 584 (bool * 585 (bool * 586 (bool * 587 (bool * 588 (bool * 589 (bool * 590 (bool * 591 (bool * 592 (bool * 593 (bool * 594 (bool * 595 (bool * 596 (bool * 597 (bool * 598 (bool * 599 (bool * 600 (bool * 601 (bool * 602 (bool * (bool * (bool * (bool * bool)))))))))))))))))))))))))))))) 603val ASID_SIZE: Nat.nat 604val PAGESIZE_BITS: Nat.nat 605val LEVEL_BITS: Nat.nat 606val BYTE: BitsN.nbit 607val HALFWORD: BitsN.nbit 608val WORD: BitsN.nbit 609val DOUBLEWORD: BitsN.nbit 610val archBase: Architecture -> BitsN.nbit 611val architecture: BitsN.nbit -> Architecture 612val archName: Architecture -> string 613val privLevel: Privilege -> BitsN.nbit 614val privilege: BitsN.nbit -> Privilege 615val privName: Privilege -> string 616val vmType: BitsN.nbit -> VM_Mode 617val isValidVM: BitsN.nbit -> bool 618val vmMode: VM_Mode -> BitsN.nbit 619val vmModeName: VM_Mode -> string 620val ext_status: ExtStatus -> BitsN.nbit 621val extStatus: BitsN.nbit -> ExtStatus 622val extStatusName: ExtStatus -> string 623val interruptIndex: Interrupt -> BitsN.nbit 624val excCode: ExceptionType -> BitsN.nbit 625val excType: BitsN.nbit -> ExceptionType 626val excName: ExceptionType -> string 627val rec'mcpuid: BitsN.nbit -> mcpuid 628val reg'mcpuid: mcpuid -> BitsN.nbit 629val write'rec'mcpuid: (BitsN.nbit * mcpuid) -> BitsN.nbit 630val write'reg'mcpuid: (mcpuid * BitsN.nbit) -> mcpuid 631val rec'mimpid: BitsN.nbit -> mimpid 632val reg'mimpid: mimpid -> BitsN.nbit 633val write'rec'mimpid: (BitsN.nbit * mimpid) -> BitsN.nbit 634val write'reg'mimpid: (mimpid * BitsN.nbit) -> mimpid 635val rec'mstatus: BitsN.nbit -> mstatus 636val reg'mstatus: mstatus -> BitsN.nbit 637val write'rec'mstatus: (BitsN.nbit * mstatus) -> BitsN.nbit 638val write'reg'mstatus: (mstatus * BitsN.nbit) -> mstatus 639val rec'mtdeleg: BitsN.nbit -> mtdeleg 640val reg'mtdeleg: mtdeleg -> BitsN.nbit 641val write'rec'mtdeleg: (BitsN.nbit * mtdeleg) -> BitsN.nbit 642val write'reg'mtdeleg: (mtdeleg * BitsN.nbit) -> mtdeleg 643val rec'mip: BitsN.nbit -> mip 644val reg'mip: mip -> BitsN.nbit 645val write'rec'mip: (BitsN.nbit * mip) -> BitsN.nbit 646val write'reg'mip: (mip * BitsN.nbit) -> mip 647val rec'mie: BitsN.nbit -> mie 648val reg'mie: mie -> BitsN.nbit 649val write'rec'mie: (BitsN.nbit * mie) -> BitsN.nbit 650val write'reg'mie: (mie * BitsN.nbit) -> mie 651val rec'mcause: BitsN.nbit -> mcause 652val reg'mcause: mcause -> BitsN.nbit 653val write'rec'mcause: (BitsN.nbit * mcause) -> BitsN.nbit 654val write'reg'mcause: (mcause * BitsN.nbit) -> mcause 655val rec'sstatus: BitsN.nbit -> sstatus 656val reg'sstatus: sstatus -> BitsN.nbit 657val write'rec'sstatus: (BitsN.nbit * sstatus) -> BitsN.nbit 658val write'reg'sstatus: (sstatus * BitsN.nbit) -> sstatus 659val rec'sip: BitsN.nbit -> sip 660val reg'sip: sip -> BitsN.nbit 661val write'rec'sip: (BitsN.nbit * sip) -> BitsN.nbit 662val write'reg'sip: (sip * BitsN.nbit) -> sip 663val rec'sie: BitsN.nbit -> sie 664val reg'sie: sie -> BitsN.nbit 665val write'rec'sie: (BitsN.nbit * sie) -> BitsN.nbit 666val write'reg'sie: (sie * BitsN.nbit) -> sie 667val rec'FPCSR: BitsN.nbit -> FPCSR 668val reg'FPCSR: FPCSR -> BitsN.nbit 669val write'rec'FPCSR: (BitsN.nbit * FPCSR) -> BitsN.nbit 670val write'reg'FPCSR: (FPCSR * BitsN.nbit) -> FPCSR 671val lift_mip_sip: mip -> sip 672val lift_mie_sie: mie -> sie 673val lower_sip_mip: (sip * mip) -> mip 674val lower_sie_mie: (sie * mie) -> mie 675val update_mstatus: (mstatus * mstatus) -> mstatus 676val lift_mstatus_sstatus: mstatus -> sstatus 677val lower_sstatus_mstatus: (sstatus * mstatus) -> mstatus 678val popPrivilegeStack: mstatus -> mstatus 679val pushPrivilegeStack: (mstatus * Privilege) -> mstatus 680val scheduleCore: Nat.nat -> unit 681val gpr: BitsN.nbit -> BitsN.nbit 682val write'gpr: (BitsN.nbit * BitsN.nbit) -> unit 683val fcsr: unit -> FPCSR 684val write'fcsr: FPCSR -> unit 685val fpr: BitsN.nbit -> BitsN.nbit 686val write'fpr: (BitsN.nbit * BitsN.nbit) -> unit 687val PC: unit -> BitsN.nbit 688val write'PC: BitsN.nbit -> unit 689val UCSR: unit -> UserCSR 690val write'UCSR: UserCSR -> unit 691val SCSR: unit -> SupervisorCSR 692val write'SCSR: SupervisorCSR -> unit 693val HCSR: unit -> HypervisorCSR 694val write'HCSR: HypervisorCSR -> unit 695val MCSR: unit -> MachineCSR 696val write'MCSR: MachineCSR -> unit 697val NextFetch: unit -> (TransferControl option) 698val write'NextFetch: (TransferControl option) -> unit 699val ReserveLoad: unit -> (BitsN.nbit option) 700val write'ReserveLoad: (BitsN.nbit option) -> unit 701val ExitCode: unit -> BitsN.nbit 702val write'ExitCode: BitsN.nbit -> unit 703val curArch: unit -> Architecture 704val in32BitMode: unit -> bool 705val curPrivilege: unit -> Privilege 706val curEPC: unit -> BitsN.nbit 707val sendIPI: BitsN.nbit -> unit 708val rnd_mode_static: BitsN.nbit -> (Rounding option) 709val rnd_mode_dynamic: BitsN.nbit -> (Rounding option) 710val l3round: Rounding -> (IEEEReal.rounding_mode option) 711val round: BitsN.nbit -> (IEEEReal.rounding_mode option) 712val RV32_CanonicalNan: BitsN.nbit 713val RV64_CanonicalNan: BitsN.nbit 714val FP32_IsSignalingNan: BitsN.nbit -> bool 715val FP64_IsSignalingNan: BitsN.nbit -> bool 716val FP32_Sign: BitsN.nbit -> bool 717val FP64_Sign: BitsN.nbit -> bool 718val setFP_Invalid: unit -> unit 719val setFP_DivZero: unit -> unit 720val setFP_Overflow: unit -> unit 721val setFP_Underflow: unit -> unit 722val setFP_Inexact: unit -> unit 723val csrRW: BitsN.nbit -> BitsN.nbit 724val csrPR: BitsN.nbit -> BitsN.nbit 725val check_CSR_access: 726 (BitsN.nbit * (BitsN.nbit * (Privilege * accessType))) -> bool 727val is_CSR_defined: BitsN.nbit -> bool 728val CSRMap: BitsN.nbit -> BitsN.nbit 729val write'CSRMap: (BitsN.nbit * BitsN.nbit) -> unit 730val csrName: BitsN.nbit -> string 731val Delta: unit -> StateDelta 732val write'Delta: StateDelta -> unit 733val hex32: BitsN.nbit -> string 734val hex64: BitsN.nbit -> string 735val log_w_csr: (BitsN.nbit * BitsN.nbit) -> string 736val reg: BitsN.nbit -> string 737val fpreg: BitsN.nbit -> string 738val log_w_gpr: (BitsN.nbit * BitsN.nbit) -> string 739val log_w_fprs: (BitsN.nbit * BitsN.nbit) -> string 740val log_w_fprd: (BitsN.nbit * BitsN.nbit) -> string 741val log_w_mem_mask: 742 (BitsN.nbit * 743 (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))) -> 744 string 745val log_w_mem_mask_misaligned: 746 (BitsN.nbit * 747 (BitsN.nbit * 748 (BitsN.nbit * (BitsN.nbit * (Nat.nat * (BitsN.nbit * BitsN.nbit)))))) -> 749 string 750val log_w_mem: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> string 751val log_r_mem: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> string 752val log_exc: ExceptionType -> string 753val log_tohost: BitsN.nbit -> string 754val clear_logs: unit -> unit 755val setTrap: (ExceptionType * (BitsN.nbit option)) -> unit 756val signalException: ExceptionType -> unit 757val signalAddressException: (ExceptionType * BitsN.nbit) -> unit 758val signalEnvCall: unit -> unit 759val checkDelegation: (Privilege * (bool * BitsN.nbit)) -> Privilege 760val checkPrivInterrupt: Privilege -> ((Interrupt * Privilege) option) 761val checkInterrupts: unit -> ((Interrupt * Privilege) option) 762val takeTrap: 763 (bool * (BitsN.nbit * (BitsN.nbit * ((BitsN.nbit option) * Privilege)))) -> 764 unit 765val CSR: BitsN.nbit -> BitsN.nbit 766val write'CSR: (BitsN.nbit * BitsN.nbit) -> unit 767val writeCSR: (BitsN.nbit * BitsN.nbit) -> unit 768val GPR: BitsN.nbit -> BitsN.nbit 769val write'GPR: (BitsN.nbit * BitsN.nbit) -> unit 770val FPRS: BitsN.nbit -> BitsN.nbit 771val write'FPRS: (BitsN.nbit * BitsN.nbit) -> unit 772val FPRD: BitsN.nbit -> BitsN.nbit 773val write'FPRD: (BitsN.nbit * BitsN.nbit) -> unit 774val writeFPRS: (BitsN.nbit * BitsN.nbit) -> unit 775val writeFPRD: (BitsN.nbit * BitsN.nbit) -> unit 776val MEM: BitsN.nbit -> BitsN.nbit 777val write'MEM: (BitsN.nbit * BitsN.nbit) -> unit 778val rawReadData: BitsN.nbit -> BitsN.nbit 779val rawWriteData: (BitsN.nbit * (BitsN.nbit * Nat.nat)) -> unit 780val rawReadInst: BitsN.nbit -> BitsN.nbit 781val rawWriteMem: (BitsN.nbit * BitsN.nbit) -> unit 782val checkMemPermission: 783 (fetchType * (accessType * (Privilege * BitsN.nbit))) -> bool 784val isGlobal: BitsN.nbit -> bool 785val rec'SV_PTE: BitsN.nbit -> SV_PTE 786val reg'SV_PTE: SV_PTE -> BitsN.nbit 787val write'rec'SV_PTE: (BitsN.nbit * SV_PTE) -> BitsN.nbit 788val write'reg'SV_PTE: (SV_PTE * BitsN.nbit) -> SV_PTE 789val rec'SV_Vaddr: BitsN.nbit -> SV_Vaddr 790val reg'SV_Vaddr: SV_Vaddr -> BitsN.nbit 791val write'rec'SV_Vaddr: (BitsN.nbit * SV_Vaddr) -> BitsN.nbit 792val write'reg'SV_Vaddr: (SV_Vaddr * BitsN.nbit) -> SV_Vaddr 793val walk64: 794 (BitsN.nbit * 795 (fetchType * (accessType * (Privilege * (BitsN.nbit * Nat.nat))))) -> 796 ((BitsN.nbit * (SV_PTE * (Nat.nat * (bool * BitsN.nbit)))) option) 797val curASID: unit -> BitsN.nbit 798val mkTLBEntry: 799 (BitsN.nbit * 800 (bool * (BitsN.nbit * (BitsN.nbit * (SV_PTE * (Nat.nat * BitsN.nbit)))))) -> 801 TLBEntry 802val TLBEntries: Nat.nat 803val lookupTLB: 804 (BitsN.nbit * (BitsN.nbit * ((TLBEntry option) Map.map))) -> 805 ((TLBEntry * BitsN.nbit) option) 806val addToTLB: 807 (BitsN.nbit * 808 (BitsN.nbit * 809 (BitsN.nbit * 810 (SV_PTE * 811 (BitsN.nbit * (Nat.nat * (bool * ((TLBEntry option) Map.map)))))))) -> 812 ((TLBEntry option) Map.map) 813val flushTLB: 814 (BitsN.nbit * ((BitsN.nbit option) * ((TLBEntry option) Map.map))) -> 815 ((TLBEntry option) Map.map) 816val TLB: unit -> ((TLBEntry option) Map.map) 817val write'TLB: ((TLBEntry option) Map.map) -> unit 818val translate64: 819 (BitsN.nbit * (fetchType * (accessType * (Privilege * Nat.nat)))) -> 820 (BitsN.nbit option) 821val translateAddr: 822 (BitsN.nbit * (fetchType * accessType)) -> (BitsN.nbit option) 823val matchLoadReservation: BitsN.nbit -> bool 824val branchTo: BitsN.nbit -> unit 825val dfn'ADDI: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 826val dfn'ADDIW: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 827val dfn'SLTI: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 828val dfn'SLTIU: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 829val dfn'ANDI: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 830val dfn'ORI: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 831val dfn'XORI: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 832val dfn'SLLI: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 833val dfn'SRLI: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 834val dfn'SRAI: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 835val dfn'SLLIW: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 836val dfn'SRLIW: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 837val dfn'SRAIW: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 838val dfn'LUI: (BitsN.nbit * BitsN.nbit) -> unit 839val dfn'AUIPC: (BitsN.nbit * BitsN.nbit) -> unit 840val dfn'ADD: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 841val dfn'ADDW: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 842val dfn'SUB: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 843val dfn'SUBW: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 844val dfn'SLT: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 845val dfn'SLTU: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 846val dfn'AND: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 847val dfn'OR: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 848val dfn'XOR: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 849val dfn'SLL: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 850val dfn'SLLW: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 851val dfn'SRL: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 852val dfn'SRLW: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 853val dfn'SRA: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 854val dfn'SRAW: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 855val dfn'MUL: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 856val dfn'MULH: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 857val dfn'MULHU: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 858val dfn'MULHSU: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 859val dfn'MULW: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 860val dfn'DIV: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 861val dfn'REM: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 862val dfn'DIVU: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 863val dfn'REMU: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 864val dfn'DIVW: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 865val dfn'REMW: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 866val dfn'DIVUW: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 867val dfn'REMUW: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 868val dfn'JAL: (BitsN.nbit * BitsN.nbit) -> unit 869val dfn'JALR: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 870val dfn'BEQ: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 871val dfn'BNE: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 872val dfn'BLT: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 873val dfn'BLTU: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 874val dfn'BGE: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 875val dfn'BGEU: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 876val dfn'LW: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 877val dfn'LWU: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 878val dfn'LH: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 879val dfn'LHU: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 880val dfn'LB: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 881val dfn'LBU: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 882val dfn'LD: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 883val dfn'SW: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 884val dfn'SH: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 885val dfn'SB: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 886val dfn'SD: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 887val dfn'FENCE: 888 (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit 889val dfn'FENCE_I: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 890val dfn'LR_W: 891 (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit 892val dfn'LR_D: 893 (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit 894val dfn'SC_W: 895 (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> 896 unit 897val dfn'SC_D: 898 (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> 899 unit 900val dfn'AMOSWAP_W: 901 (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> 902 unit 903val dfn'AMOSWAP_D: 904 (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> 905 unit 906val dfn'AMOADD_W: 907 (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> 908 unit 909val dfn'AMOADD_D: 910 (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> 911 unit 912val dfn'AMOXOR_W: 913 (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> 914 unit 915val dfn'AMOXOR_D: 916 (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> 917 unit 918val dfn'AMOAND_W: 919 (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> 920 unit 921val dfn'AMOAND_D: 922 (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> 923 unit 924val dfn'AMOOR_W: 925 (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> 926 unit 927val dfn'AMOOR_D: 928 (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> 929 unit 930val dfn'AMOMIN_W: 931 (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> 932 unit 933val dfn'AMOMIN_D: 934 (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> 935 unit 936val dfn'AMOMAX_W: 937 (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> 938 unit 939val dfn'AMOMAX_D: 940 (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> 941 unit 942val dfn'AMOMINU_W: 943 (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> 944 unit 945val dfn'AMOMINU_D: 946 (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> 947 unit 948val dfn'AMOMAXU_W: 949 (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> 950 unit 951val dfn'AMOMAXU_D: 952 (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> 953 unit 954val dfn'FLW: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 955val dfn'FSW: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 956val dfn'FADD_S: 957 (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit 958val dfn'FSUB_S: 959 (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit 960val dfn'FMUL_S: 961 (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit 962val dfn'FDIV_S: 963 (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit 964val dfn'FSQRT_S: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 965val dfn'FMIN_S: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 966val dfn'FMAX_S: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 967val dfn'FMADD_S: 968 (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> 969 unit 970val dfn'FMSUB_S: 971 (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> 972 unit 973val dfn'FNMADD_S: 974 (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> 975 unit 976val dfn'FNMSUB_S: 977 (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> 978 unit 979val dfn'FCVT_S_W: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 980val dfn'FCVT_S_WU: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 981val dfn'FCVT_W_S: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 982val dfn'FCVT_WU_S: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 983val dfn'FCVT_S_L: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 984val dfn'FCVT_S_LU: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 985val dfn'FCVT_L_S: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 986val dfn'FCVT_LU_S: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 987val dfn'FSGNJ_S: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 988val dfn'FSGNJN_S: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 989val dfn'FSGNJX_S: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 990val dfn'FMV_X_S: (BitsN.nbit * BitsN.nbit) -> unit 991val dfn'FMV_S_X: (BitsN.nbit * BitsN.nbit) -> unit 992val dfn'FEQ_S: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 993val dfn'FLT_S: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 994val dfn'FLE_S: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 995val dfn'FCLASS_S: (BitsN.nbit * BitsN.nbit) -> unit 996val dfn'FLD: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 997val dfn'FSD: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 998val dfn'FADD_D: 999 (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit 1000val dfn'FSUB_D: 1001 (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit 1002val dfn'FMUL_D: 1003 (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit 1004val dfn'FDIV_D: 1005 (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit 1006val dfn'FSQRT_D: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 1007val dfn'FMIN_D: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 1008val dfn'FMAX_D: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 1009val dfn'FMADD_D: 1010 (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> 1011 unit 1012val dfn'FMSUB_D: 1013 (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> 1014 unit 1015val dfn'FNMADD_D: 1016 (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> 1017 unit 1018val dfn'FNMSUB_D: 1019 (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> 1020 unit 1021val dfn'FCVT_D_W: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 1022val dfn'FCVT_D_WU: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 1023val dfn'FCVT_W_D: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 1024val dfn'FCVT_WU_D: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 1025val dfn'FCVT_D_L: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 1026val dfn'FCVT_D_LU: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 1027val dfn'FCVT_L_D: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 1028val dfn'FCVT_LU_D: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 1029val dfn'FCVT_S_D: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 1030val dfn'FCVT_D_S: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 1031val dfn'FSGNJ_D: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 1032val dfn'FSGNJN_D: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 1033val dfn'FSGNJX_D: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 1034val dfn'FMV_X_D: (BitsN.nbit * BitsN.nbit) -> unit 1035val dfn'FMV_D_X: (BitsN.nbit * BitsN.nbit) -> unit 1036val dfn'FEQ_D: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 1037val dfn'FLT_D: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 1038val dfn'FLE_D: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 1039val dfn'FCLASS_D: (BitsN.nbit * BitsN.nbit) -> unit 1040val dfn'ECALL: unit -> unit 1041val dfn'EBREAK: unit -> unit 1042val dfn'ERET: unit -> unit 1043val dfn'MRTS: unit -> unit 1044val dfn'WFI: unit 1045val checkCSROp: (BitsN.nbit * (BitsN.nbit * accessType)) -> bool 1046val dfn'CSRRW: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 1047val dfn'CSRRS: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 1048val dfn'CSRRC: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 1049val dfn'CSRRWI: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 1050val dfn'CSRRSI: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 1051val dfn'CSRRCI: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 1052val dfn'SFENCE_VM: BitsN.nbit -> unit 1053val dfn'UnknownInstruction: unit -> unit 1054val dfn'FETCH_MISALIGNED: BitsN.nbit -> unit 1055val dfn'FETCH_FAULT: BitsN.nbit -> unit 1056val Run: instruction -> unit 1057val Fetch: unit -> FetchResult 1058val asImm12: 1059 (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> BitsN.nbit 1060val asImm20: 1061 (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> BitsN.nbit 1062val asSImm12: (BitsN.nbit * BitsN.nbit) -> BitsN.nbit 1063val Decode: BitsN.nbit -> instruction 1064val imm: Nat.nat -> BitsN.nbit -> string 1065val instr: string -> string 1066val amotype: (BitsN.nbit * BitsN.nbit) -> string 1067val pRtype: (string * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> string 1068val pARtype: 1069 (string * 1070 (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))) -> 1071 string 1072val pLRtype: 1073 (string * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> 1074 string 1075val pItype: Nat.nat -> 1076 (string * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> string 1077val pCSRtype: 1078 (string * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> string 1079val pCSRItype: Nat.nat -> 1080 (string * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> string 1081val pStype: Nat.nat -> 1082 (string * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> string 1083val pSBtype: Nat.nat -> 1084 (string * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> string 1085val pUtype: Nat.nat -> (string * (BitsN.nbit * BitsN.nbit)) -> string 1086val pUJtype: Nat.nat -> (string * (BitsN.nbit * BitsN.nbit)) -> string 1087val pN0type: string -> string 1088val pN1type: (string * BitsN.nbit) -> string 1089val pFRtype: (string * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> string 1090val pFR1type: (string * (BitsN.nbit * BitsN.nbit)) -> string 1091val pFR3type: 1092 (string * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> 1093 string 1094val pFItype: Nat.nat -> 1095 (string * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> string 1096val pFStype: Nat.nat -> 1097 (string * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> string 1098val pCFItype: (string * (BitsN.nbit * BitsN.nbit)) -> string 1099val pCIFtype: (string * (BitsN.nbit * BitsN.nbit)) -> string 1100val instructionToString: instruction -> string 1101val Rtype: 1102 (BitsN.nbit * 1103 (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))) -> 1104 BitsN.nbit 1105val R4type: 1106 (BitsN.nbit * 1107 (BitsN.nbit * 1108 (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))))) -> 1109 BitsN.nbit 1110val Itype: 1111 (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> 1112 BitsN.nbit 1113val Stype: 1114 (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> 1115 BitsN.nbit 1116val SBtype: 1117 (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> 1118 BitsN.nbit 1119val Utype: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> BitsN.nbit 1120val UJtype: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> BitsN.nbit 1121val opc: BitsN.nbit -> BitsN.nbit 1122val amofunc: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> BitsN.nbit 1123val Encode: instruction -> BitsN.nbit 1124val log_instruction: (BitsN.nbit * instruction) -> string 1125val exitCode: unit -> Nat.nat 1126val CYCLES_PER_TIMER_TICK: Nat.nat 1127val tickClock: unit -> unit 1128val incrInstret: unit -> unit 1129val checkTimers: unit -> unit 1130val Next: unit -> unit 1131val initIdent: Architecture -> unit 1132val initMachine: BitsN.nbit -> unit 1133val initRegs: Nat.nat -> unit 1134 1135end