1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
|
/*=======================================================================================*/
/* This Sail RISC-V architecture model, comprising all files and */
/* directories except where otherwise noted is subject the BSD */
/* two-clause license in the LICENSE file. */
/* */
/* SPDX-License-Identifier: BSD-2-Clause */
/*=======================================================================================*/
/* default exception model */
type ext_exception = unit
/* Is XRET from given mode permitted by extension? */
function ext_check_xret_priv (p : Privilege) : Privilege -> bool = true
/* Called if above check fails */
function ext_fail_xret_priv () : unit -> unit = ()
function handle_trap_extension(p : Privilege, pc : xlenbits, u : option(unit)) -> unit = ()
/* used for traps and ECALL */
function prepare_trap_vector(p : Privilege, cause : Mcause) -> xlenbits = {
let tvec : Mtvec = match p {
Machine => mtvec,
Supervisor => stvec,
User => internal_error(__FILE__, __LINE__, "Invalid privilege level"),
};
match tvec_addr(tvec, cause) {
Some(epc) => epc,
None() => internal_error(__FILE__, __LINE__, "Invalid tvec mode")
}
}
/* xRET handling involves three functions:
*
* get_xepc: used to read the value of the xret target (no control flow transfer)
* set_xepc: used to write a value of the xret target (no control flow transfer)
* prepare_xret_target: used to get the value for control transfer to the xret target
*/
val get_xepc : Privilege -> xlenbits
function get_xepc(p) =
match p {
Machine => align_pc(mepc),
Supervisor => align_pc(sepc),
User => internal_error(__FILE__, __LINE__, "Invalid privilege level"),
}
val set_xepc : (Privilege, xlenbits) -> xlenbits
function set_xepc(p, value) = {
let target = legalize_xepc(value);
match p {
Machine => mepc = target,
Supervisor => sepc = target,
User => internal_error(__FILE__, __LINE__, "Invalid privilege level"),
};
target
}
val prepare_xret_target : (Privilege) -> xlenbits
function prepare_xret_target(p) =
get_xepc(p)
/* other trap-related CSRs */
function get_mtvec() -> xlenbits =
mtvec.bits
function get_stvec() -> xlenbits =
stvec.bits
function set_mtvec(value : xlenbits) -> xlenbits = {
mtvec = legalize_tvec(mtvec, value);
mtvec.bits
}
function set_stvec(value : xlenbits) -> xlenbits = {
stvec = legalize_tvec(stvec, value);
stvec.bits
}
mapping clause csr_name_map = 0x105 <-> "stvec"
mapping clause csr_name_map = 0x141 <-> "sepc"
mapping clause csr_name_map = 0x305 <-> "mtvec"
mapping clause csr_name_map = 0x341 <-> "mepc"
function clause is_CSR_accessible(0x105, _, _) = currentlyEnabled(Ext_S) // stvec
function clause is_CSR_accessible(0x141, _, _) = currentlyEnabled(Ext_S) // sepc
function clause is_CSR_accessible(0x305, _, _) = true // mtvec
function clause is_CSR_accessible(0x341, _, _) = true // mepc
function clause read_CSR(0x105) = get_stvec()
function clause read_CSR(0x141) = get_xepc(Supervisor)
function clause read_CSR(0x305) = get_mtvec()
function clause read_CSR(0x341) = get_xepc(Machine)
function clause write_CSR(0x105, value) = { Ok(set_stvec(value)) }
function clause write_CSR(0x141, value) = { Ok(set_xepc(Supervisor, value)) }
function clause write_CSR(0x305, value) = { Ok(set_mtvec(value)) }
function clause write_CSR(0x341, value) = { Ok(set_xepc(Machine, value)) }
|
