diff options
| author | Prashanth Mundkur <prashanth.mundkur@gmail.com> | 2019-05-06 11:42:28 -0700 |
|---|---|---|
| committer | Prashanth Mundkur <prashanth.mundkur@gmail.com> | 2019-05-06 11:59:10 -0700 |
| commit | 0856a511e198b063c555f69bac7586a7dc39879f (patch) | |
| tree | 31e33fae645a694207c7ff5412c44962a1368573 /model | |
| parent | e884e955feed337100c791c705f65de709ec4a4b (diff) | |
| download | sail-riscv-0856a511e198b063c555f69bac7586a7dc39879f.zip sail-riscv-0856a511e198b063c555f69bac7586a7dc39879f.tar.gz sail-riscv-0856a511e198b063c555f69bac7586a7dc39879f.tar.bz2 | |
Factor out sync_exception to fix dependencies in cheri, and similarly split out pc access.
Diffstat (limited to 'model')
| -rw-r--r-- | model/riscv_addr_checks.sail | 17 | ||||
| -rw-r--r-- | model/riscv_pc_access.sail | 15 | ||||
| -rw-r--r-- | model/riscv_sync_exception.sail | 7 | ||||
| -rw-r--r-- | model/riscv_sys_control.sail | 8 |
4 files changed, 23 insertions, 24 deletions
diff --git a/model/riscv_addr_checks.sail b/model/riscv_addr_checks.sail index 2471075..25b6396 100644 --- a/model/riscv_addr_checks.sail +++ b/model/riscv_addr_checks.sail @@ -53,20 +53,3 @@ function ext_data_get_addr(base : regbits, offset : xlenbits, acc : AccessType, function ext_handle_data_check_error(err : ext_data_addr_error) -> unit = () - -/* accessors for default architectural addresses, for use from within instructions */ -/* FIXME: these don't really belong in this file. */ -/* FIXME: see note in cheri_addr_checks.sail */ - -val get_next_pc : unit -> xlenbits effect {rreg} -function get_next_pc() = nextPC - -val set_next_pc : xlenbits -> unit effect {wreg} -function set_next_pc(pc) = { - nextPC = pc -} - -val tick_pc : unit -> unit effect {rreg, wreg} -function tick_pc() = { - PC = nextPC -} diff --git a/model/riscv_pc_access.sail b/model/riscv_pc_access.sail new file mode 100644 index 0000000..a51e627 --- /dev/null +++ b/model/riscv_pc_access.sail @@ -0,0 +1,15 @@ +/* accessors for default architectural addresses, for use from within instructions */ +/* FIXME: see note in cheri_addr_checks.sail */ + +val get_next_pc : unit -> xlenbits effect {rreg} +function get_next_pc() = nextPC + +val set_next_pc : xlenbits -> unit effect {wreg} +function set_next_pc(pc) = { + nextPC = pc +} + +val tick_pc : unit -> unit effect {rreg, wreg} +function tick_pc() = { + PC = nextPC +} diff --git a/model/riscv_sync_exception.sail b/model/riscv_sync_exception.sail new file mode 100644 index 0000000..208d518 --- /dev/null +++ b/model/riscv_sync_exception.sail @@ -0,0 +1,7 @@ +/* model context for synchronous exceptions, parameterized for extensions */ + +struct sync_exception = { + trap : ExceptionType, + excinfo : option(xlenbits), + ext : option(ext_exception) /* for extensions */ +} diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index d37ffc9..52111f1 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -244,13 +244,7 @@ function dispatchInterrupt(priv : Privilege) -> option((InterruptType, Privilege } } -/* model context for synchronous exceptions, parameterized for extensions */ - -struct sync_exception = { - trap : ExceptionType, - excinfo : option(xlenbits), - ext : option(ext_exception) /* for extensions */ -} +/* types of privilege transitions */ union ctl_result = { CTL_TRAP : sync_exception, |