blob: 06e20f9680d7bdec7bd31017acbe1e08ec47bb0e (
plain)
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
|
/* default fetch address checks */
type ext_fetch_addr_error = unit
/* Since fetch is done in granules, the check function gets two arguments:
* start_pc: the PC at the start of the current fetch sequence
* pc: the PC for the current granule
*
* returns: the *virtual* memory address to use for the fetch.
* any address translation errors are reported for pc, not the returned value.
*/
function ext_fetch_check_pc(start_pc : xlenbits, pc : xlenbits) -> Ext_FetchAddr_Check(ext_fetch_addr_error) =
Ext_FetchAddr_OK(pc)
function ext_handle_fetch_check_error(err : ext_fetch_addr_error) -> unit =
()
/* default control address checks */
type ext_control_addr_error = unit
/* these functions return the address to use as the target for
* the control transfer. any address translation or other errors
* are reported for the original value, not the returned value.
*
* NOTE: the input value does *not* have bit[0] set to 0, to enable
* more accurate bounds checking. There is no constraint on the output
* value, which will have bit[0] cleared by the caller if needed.
*/
/* the control address is derived from a non-PC register, e.g. in JALR */
function ext_control_check_addr(pc : xlenbits) -> Ext_ControlAddr_Check(ext_control_addr_error) =
Ext_ControlAddr_OK(pc)
/* the control address is derived from the PC register, e.g. in JAL */
function ext_control_check_pc(pc : xlenbits) -> Ext_ControlAddr_Check(ext_control_addr_error) =
Ext_ControlAddr_OK(pc)
function ext_handle_control_check_error(err : ext_control_addr_error) -> unit =
()
/* The default data address function does not perform any checks so
just uses unit for error type. */
type ext_data_addr_error = unit
/* Default data addr is just base register + immediate offset (may be zero).
Extensions might override and add additional checks. */
function ext_data_get_addr(base : regidx, offset : xlenbits, acc : AccessType, width : word_width)
-> Ext_DataAddr_Check(ext_data_addr_error) =
let addr = X(base) + offset in
Ext_DataAddr_OK(addr)
function ext_handle_data_check_error(err : ext_data_addr_error) -> unit =
()
|
