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