diff options
| author | Alasdair <alasdair.armstrong@cl.cam.ac.uk> | 2024-04-03 16:12:24 +0100 |
|---|---|---|
| committer | Bill McSpadden <bill@riscv.org> | 2024-05-10 13:24:19 -0500 |
| commit | 82acf052d4392f0662fa62cccea2353d57b4145a (patch) | |
| tree | 26febb6183dc99bcdd49686076d131f9d82ec12b | |
| parent | 440ac2c66deba0a42ecf6ddc670f09bdac83bb50 (diff) | |
| download | sail-riscv-82acf052d4392f0662fa62cccea2353d57b4145a.zip sail-riscv-82acf052d4392f0662fa62cccea2353d57b4145a.tar.gz sail-riscv-82acf052d4392f0662fa62cccea2353d57b4145a.tar.bz2 | |
lem: Add PMP related stubs for Isabelle build
These stub functions are required for building the Riscv.thy file
from the generated lem file.
| -rw-r--r-- | handwritten_support/riscv_extras.lem | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/handwritten_support/riscv_extras.lem b/handwritten_support/riscv_extras.lem index 27e8ee5..4bc3300 100644 --- a/handwritten_support/riscv_extras.lem +++ b/handwritten_support/riscv_extras.lem @@ -169,6 +169,14 @@ val sys_enable_writable_fiom : unit -> bool let sys_enable_writable_fiom () = true declare ocaml target_rep function sys_enable_writable_fiom = `Platform.enable_writable_fiom` +val sys_pmp_grain : unit -> integer +let sys_pmp_grain () = 0 +declare ocaml target_rep function sys_pmp_grain = `Platform.sys_pmp_grain` + +val sys_pmp_count : unit -> integer +let sys_pmp_count () = 0 +declare ocaml target_rep function sys_pmp_count = `Platform.sys_pmp_count` + val plat_ram_base : unit -> bitvector let plat_ram_base () = [] declare ocaml target_rep function plat_ram_base = `Platform.dram_base` |