Skip to content

Commit 0224391

Browse files
authored
Add unratified Smclic, Ssclic, Smclicshv extensions
Spec: https://github.com/riscv/riscv-fast-interrupt Tests: riscv-non-isa/riscv-arch-test#436
1 parent 0288a3d commit 0224391

File tree

2 files changed

+16
-0
lines changed

2 files changed

+16
-0
lines changed

handwritten_support/riscv_extras.lem

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -193,6 +193,14 @@ val plat_clint_size : unit -> bitvector
193193
let plat_clint_size () = []
194194
declare ocaml target_rep function plat_clint_size = `Platform.clint_size`
195195

196+
val plat_clic_base : unit -> bitvector
197+
let plat_clic_base () = []
198+
declare ocaml target_rep function plat_clic_base = `Platform.clic_base`
199+
200+
val plat_clic_size : unit -> bitvector
201+
let plat_clic_size () = []
202+
declare ocaml target_rep function plat_clic_size = `Platform.clic_size`
203+
196204
val plat_enable_dirty_update : unit -> bool
197205
let plat_enable_dirty_update () = false
198206
declare ocaml target_rep function plat_enable_dirty_update = `Platform.enable_dirty_update`

handwritten_support/riscv_extras_sequential.lem

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -181,6 +181,14 @@ val plat_clint_size : forall 'a. Size 'a => unit -> bitvector 'a
181181
let plat_clint_size () = wordFromInteger 0
182182
declare ocaml target_rep function plat_clint_size = `Platform.clint_size`
183183

184+
val plat_clic_base : forall 'a. Size 'a => unit -> bitvector 'a
185+
let plat_clic_base () = wordFromInteger 0
186+
declare ocaml target_rep function plat_clic_base = `Platform.clic_base`
187+
188+
val plat_clic_size : forall 'a. Size 'a => unit -> bitvector 'a
189+
let plat_clic_size () = wordFromInteger 0
190+
declare ocaml target_rep function plat_clic_size = `Platform.clic_size`
191+
184192
val plat_enable_dirty_update : unit -> bool
185193
let plat_enable_dirty_update () = false
186194
declare ocaml target_rep function plat_enable_dirty_update = `Platform.enable_dirty_update`

0 commit comments

Comments
 (0)