aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rwxr-xr-xbuild_simulators.sh8
-rw-r--r--c_emulator/riscv_platform.c5
-rw-r--r--c_emulator/riscv_platform.h3
-rw-r--r--c_emulator/riscv_platform_impl.c2
-rw-r--r--c_emulator/riscv_platform_impl.h2
-rw-r--r--c_emulator/riscv_sim.c12
-rw-r--r--handwritten_support/riscv_extras.lem11
-rw-r--r--handwritten_support/riscv_extras.v50
-rw-r--r--handwritten_support/riscv_extras_sequential.lem11
-rw-r--r--model/prelude.sail14
-rw-r--r--model/prelude_mem.sail24
-rw-r--r--model/riscv_insts_cext.sail9
-rw-r--r--model/riscv_sys_control.sail13
-rw-r--r--model/riscv_sys_regs.sail31
-rw-r--r--ocaml_emulator/platform.ml29
-rw-r--r--ocaml_emulator/riscv_ocaml_sim.ml6
-rw-r--r--os-boot/README.md3
17 files changed, 154 insertions, 79 deletions
diff --git a/build_simulators.sh b/build_simulators.sh
new file mode 100755
index 0000000..bf32e15
--- /dev/null
+++ b/build_simulators.sh
@@ -0,0 +1,8 @@
+#!/bin/bash
+
+make ARCH=RV32 ocaml_emulator/riscv_ocaml_sim_RV32
+make ARCH=RV64 ocaml_emulator/riscv_ocaml_sim_RV64
+
+make ARCH=RV32 c_emulator/riscv_sim_RV32
+make ARCH=RV64 c_emulator/riscv_sim_RV64
+
diff --git a/c_emulator/riscv_platform.c b/c_emulator/riscv_platform.c
index d1b1f6e..dcc5766 100644
--- a/c_emulator/riscv_platform.c
+++ b/c_emulator/riscv_platform.c
@@ -9,6 +9,11 @@
static mach_bits reservation = 0;
static bool reservation_valid = false;
+bool sys_enable_rvc(unit u)
+{ return rv_enable_rvc; }
+bool sys_enable_writable_misa(unit u)
+{ return rv_enable_writable_misa; }
+
bool plat_enable_dirty_update(unit u)
{ return rv_enable_dirty_update; }
diff --git a/c_emulator/riscv_platform.h b/c_emulator/riscv_platform.h
index 728555e..31f2807 100644
--- a/c_emulator/riscv_platform.h
+++ b/c_emulator/riscv_platform.h
@@ -1,6 +1,9 @@
#pragma once
#include "sail.h"
+bool sys_enable_rvc(unit);
+bool sys_enable_writable_misa(unit);
+
bool plat_enable_dirty_update(unit);
bool plat_enable_misaligned_access(unit);
bool plat_mtval_has_illegal_inst_bits(unit);
diff --git a/c_emulator/riscv_platform_impl.c b/c_emulator/riscv_platform_impl.c
index ed32979..5894fc9 100644
--- a/c_emulator/riscv_platform_impl.c
+++ b/c_emulator/riscv_platform_impl.c
@@ -3,6 +3,8 @@
#include <stdio.h>
/* Settings of the platform implementation, with common defaults. */
+bool rv_enable_rvc = true;
+bool rv_enable_writable_misa = true;
bool rv_enable_dirty_update = false;
bool rv_enable_misaligned = false;
diff --git a/c_emulator/riscv_platform_impl.h b/c_emulator/riscv_platform_impl.h
index 2e59fd8..cf3bc30 100644
--- a/c_emulator/riscv_platform_impl.h
+++ b/c_emulator/riscv_platform_impl.h
@@ -7,6 +7,8 @@
#define DEFAULT_RSTVEC 0x00001000
+extern bool rv_enable_rvc;
+extern bool rv_enable_writable_misa;
extern bool rv_enable_dirty_update;
extern bool rv_enable_misaligned;
extern bool rv_mtval_has_illegal_inst_bits;
diff --git a/c_emulator/riscv_sim.c b/c_emulator/riscv_sim.c
index 7be7fce..1176400 100644
--- a/c_emulator/riscv_sim.c
+++ b/c_emulator/riscv_sim.c
@@ -45,7 +45,6 @@ const char *RV32ISA = "RV32IMAC";
#define CSR_MIP 0x344
static bool do_dump_dts = false;
-static bool disable_compressed = false;
static bool do_show_times = false;
struct tv_spike_t *s = NULL;
char *term_log = NULL;
@@ -78,6 +77,7 @@ static struct option options[] = {
{"enable-misaligned", no_argument, 0, 'm'},
{"ram-size", required_argument, 0, 'z'},
{"disable-compressed", no_argument, 0, 'C'},
+ {"disable-writable-misa", no_argument, 0, 'I'},
{"mtval-has-illegal-inst-bits", no_argument, 0, 'i'},
{"dump-dts", no_argument, 0, 's'},
{"device-tree-blob", required_argument, 0, 'b'},
@@ -187,7 +187,10 @@ char *process_args(int argc, char **argv)
rv_enable_misaligned = true;
break;
case 'C':
- disable_compressed = true;
+ rv_enable_rvc = false;
+ break;
+ case 'I':
+ rv_enable_writable_misa = false;
break;
case 'i':
rv_mtval_has_illegal_inst_bits = true;
@@ -424,8 +427,9 @@ void init_sail(uint64_t elf_entry)
} else
#endif
init_sail_reset_vector(elf_entry);
- if (disable_compressed)
- z_set_Misa_C(&zmisa, 0);
+
+ // this is probably unnecessary now; remove
+ if (!rv_enable_rvc) z_set_Misa_C(&zmisa, 0);
}
int init_check(struct tv_spike_t *s)
diff --git a/handwritten_support/riscv_extras.lem b/handwritten_support/riscv_extras.lem
index ed572be..d2cd03b 100644
--- a/handwritten_support/riscv_extras.lem
+++ b/handwritten_support/riscv_extras.lem
@@ -71,6 +71,14 @@ let speculate_conditional_success () = excl_result ()
let match_reservation _ = true
let cancel_reservation () = ()
+val sys_enable_writable_misa : unit -> bool
+let sys_enable_writable_misa () = true
+declare ocaml target_rep function sys_enable_writable_misa = `Platform.enable_writable_misa`
+
+val sys_enable_rvc : unit -> bool
+let sys_enable_rvc () = true
+declare ocaml target_rep function sys_enable_rvc = `Platform.enable_rvc`
+
val plat_ram_base : forall 'a. Size 'a => unit -> bitvector 'a
let plat_ram_base () = wordFromInteger 0
declare ocaml target_rep function plat_ram_base = `Platform.dram_base`
@@ -139,3 +147,6 @@ let prerr_bits msg bs = prerr_endline (msg ^ (show_bitlist (bits_of bs)))
val print_bits : forall 'a. Size 'a => string -> bitvector 'a -> unit
let print_bits msg bs = () (* print_endline (msg ^ (show_bitlist (bits_of bs))) *)
+
+val print_dbg : string -> unit
+let print_dbg msg = ()
diff --git a/handwritten_support/riscv_extras.v b/handwritten_support/riscv_extras.v
index ff235a9..33bc9ec 100644
--- a/handwritten_support/riscv_extras.v
+++ b/handwritten_support/riscv_extras.v
@@ -36,31 +36,38 @@ Definition MEMea_conditional_release {rv a e} (addr : mword a) size : monad rv u
Definition MEMea_conditional_strong_release {rv a e} (addr : mword a) size : monad rv unit e
:= write_mem_ea Write_RISCV_conditional_strong_release addr size.
-
-(* Some wrappers copied from aarch64_extras *)
-(* TODO: Harmonise into a common library *)
(*
-Definition get_slice_int_bl len n lo :=
- (* TODO: Is this the intended behaviour? *)
- let hi := lo + len - 1 in
- let bs := bools_of_int (hi + 1) n in
- subrange_list false bs hi lo
-
-val get_slice_int : forall 'a. Bitvector 'a => integer -> integer -> integer -> 'a
-Definition get_slice_int len n lo := of_bools (get_slice_int_bl len n lo)
+val MEMr : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e
+val MEMr_acquire : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e
+val MEMr_strong_acquire : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e
+val MEMr_reserved : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e
+val MEMr_reserved_acquire : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e
+val MEMr_reserved_strong_acquire : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e
*)
-Definition write_ram {rv e} m size (hexRAM : mword m) (addr : mword m) (data : mword (8 * size)) : monad rv bool e :=
- write_mem_val data.
-Definition read_ram {rv e} m size `{ArithFact (size >= 0)} (_ : mword m) (addr : mword m) : monad rv (mword (8 * size)) e :=
- read_mem Read_plain addr size.
-(*
-Definition string_of_bits bs := string_of_bv (bits_of bs).
-Definition string_of_int := show
+Definition MEMr {rv e} addrsize size (hexRAM addr : mword addrsize) `{ArithFact (size >= 0)} : monad rv (mword (8 * size)) e := read_mem Read_plain addr size.
+Definition MEMr_acquire {rv e} addrsize size (hexRAM addr : mword addrsize) `{ArithFact (size >= 0)} : monad rv (mword (8 * size)) e := read_mem Read_RISCV_acquire addr size.
+Definition MEMr_strong_acquire {rv e} addrsize size (hexRAM addr : mword addrsize) `{ArithFact (size >= 0)} : monad rv (mword (8 * size)) e := read_mem Read_RISCV_strong_acquire addr size.
+Definition MEMr_reserved {rv e} addrsize size (hexRAM addr : mword addrsize) `{ArithFact (size >= 0)} : monad rv (mword (8 * size)) e := read_mem Read_RISCV_reserved addr size.
+Definition MEMr_reserved_acquire {rv e} addrsize size (hexRAM addr : mword addrsize) `{ArithFact (size >= 0)} : monad rv (mword (8 * size)) e := read_mem Read_RISCV_reserved_acquire addr size.
+Definition MEMr_reserved_strong_acquire {rv e} addrsize size (hexRAM addr : mword addrsize) `{ArithFact (size >= 0)} : monad rv (mword (8 * size)) e := read_mem Read_RISCV_reserved_strong_acquire addr size.
-Definition _sign_extend bits len := maybe_failwith (of_bits (exts_bv len bits))
-Definition _zero_extend bits len := maybe_failwith (of_bits (extz_bv len bits))
+(*
+val MEMw : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e
+val MEMw_release : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e
+val MEMw_strong_release : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e
+val MEMw_conditional : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e
+val MEMw_conditional_release : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e
+val MEMw_conditional_strong_release : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e
*)
+
+Definition MEMw {rv e} addrsize size (hexRAM addr : mword addrsize) (v : mword (8 * size)) : monad rv bool e := write_mem Write_plain addr size v.
+Definition MEMw_release {rv e} addrsize size (hexRAM addr : mword addrsize) (v : mword (8 * size)) : monad rv bool e := write_mem Write_RISCV_release addr size v.
+Definition MEMw_strong_release {rv e} addrsize size (hexRAM addr : mword addrsize) (v : mword (8 * size)) : monad rv bool e := write_mem Write_RISCV_strong_release addr size v.
+Definition MEMw_conditional {rv e} addrsize size (hexRAM addr : mword addrsize) (v : mword (8 * size)) : monad rv bool e := write_mem Write_RISCV_conditional addr size v.
+Definition MEMw_conditional_release {rv e} addrsize size (hexRAM addr : mword addrsize) (v : mword (8 * size)) : monad rv bool e := write_mem Write_RISCV_conditional_release addr size v.
+Definition MEMw_conditional_strong_release {rv e} addrsize size (hexRAM addr : mword addrsize) (v : mword (8 * size)) : monad rv bool e := write_mem Write_RISCV_conditional_strong_release addr size v.
+
Definition shift_bits_left {a b} (v : mword a) (n : mword b) : mword a :=
shiftl v (int_of_mword false n).
@@ -134,6 +141,9 @@ Definition putchar {T} (_:T) : unit := tt.
Require DecimalString.
Definition string_of_int z := DecimalString.NilZero.string_of_int (Z.to_int z).
+Axiom sys_enable_writable_misa : unit -> bool.
+Axiom sys_enable_rvc : unit -> bool.
+
(* The constraint solver can do this itself, but a Coq bug puts
anonymous_subproof into the term instead of an actual subproof. *)
Lemma n_leading_spaces_fact {w__0} :
diff --git a/handwritten_support/riscv_extras_sequential.lem b/handwritten_support/riscv_extras_sequential.lem
index 2919d77..604911a 100644
--- a/handwritten_support/riscv_extras_sequential.lem
+++ b/handwritten_support/riscv_extras_sequential.lem
@@ -67,6 +67,14 @@ let speculate_conditional_success () = excl_result ()
let match_reservation _ = true
let cancel_reservation () = ()
+val sys_enable_writable_misa : unit -> bool
+let sys_enable_writable_misa () = true
+declare ocaml target_rep function sys_enable_writable_misa = `Platform.enable_writable_misa`
+
+val sys_enable_rvc : unit -> bool
+let sys_enable_rvc () = true
+declare ocaml target_rep function sys_enable_rvc = `Platform.enable_rvc`
+
val plat_ram_base : forall 'a. Size 'a => unit -> bitvector 'a
let plat_ram_base () = wordFromInteger 0
declare ocaml target_rep function plat_ram_base = `Platform.dram_base`
@@ -135,3 +143,6 @@ let prerr_bits msg bs = prerr_endline (msg ^ (show_bitlist (bits_of bs)))
val print_bits : forall 'a. Size 'a => string -> bitvector 'a -> unit
let print_bits msg bs = () (* print_endline (msg ^ (show_bitlist (bits_of bs))) *)
+
+val print_dbg : string -> unit
+let print_dbg msg = ()
diff --git a/model/prelude.sail b/model/prelude.sail
index 73f96b0..457c4d4 100644
--- a/model/prelude.sail
+++ b/model/prelude.sail
@@ -1,5 +1,6 @@
default Order dec
+$include <smt.sail>
$include <option.sail>
$include <arith.sail>
$include <string.sail>
@@ -84,9 +85,8 @@ overload operator - = {sub_vec, sub_vec_int}
val quot_round_zero = {ocaml: "quot_round_zero", interpreter: "quot_round_zero", lem: "hardware_quot", c: "tdiv_int"} : (int, int) -> int
val rem_round_zero = {ocaml: "rem_round_zero", interpreter: "rem_round_zero", lem: "hardware_mod", c: "tmod_int"} : (int, int) -> int
-val modulus = {lem: "hardware_mod"} : (int, int) -> int
-
-overload operator % = {modulus}
+/* The following should get us euclidean modulus, and is compatible with pre and post 0.9 versions of sail */
+overload operator % = {emod_int, mod}
val min_nat = {ocaml: "min_int", lem: "min", coq: "min_nat", c: "min_int"} : (nat, nat) -> nat
@@ -105,10 +105,10 @@ val pow2 = "pow2" : forall 'n. atom('n) -> atom(2 ^ 'n)
val print = "print_endline" : string -> unit
val print_string = "print_string" : (string, string) -> unit
-val print_instr = {ocaml: "Platform.print_instr", interpreter: "print_endline", c: "print_instr", _: "print_endline"} : string -> unit
-val print_reg = {ocaml: "Platform.print_reg", interpreter: "print_endline", c: "print_reg", _: "print_endline"} : string -> unit
-val print_mem = {ocaml: "Platform.print_mem_access", interpreter: "print_endline", c: "print_mem_access", _: "print_endline"} : string -> unit
-val print_platform = {ocaml: "Platform.print_platform", interpreter: "print_endline", c: "print_platform", _: "print_endline"} : string -> unit
+val print_instr = {ocaml: "Platform.print_instr", interpreter: "print_endline", c: "print_instr", lem: "print_dbg", _: "print_endline"} : string -> unit
+val print_reg = {ocaml: "Platform.print_reg", interpreter: "print_endline", c: "print_reg", lem: "print_dbg", _: "print_endline"} : string -> unit
+val print_mem = {ocaml: "Platform.print_mem_access", interpreter: "print_endline", c: "print_mem_access", lem: "print_dbg", _: "print_endline"} : string -> unit
+val print_platform = {ocaml: "Platform.print_platform", interpreter: "print_endline", c: "print_platform", lem: "print_dbg", _: "print_endline"} : string -> unit
$ifndef FEATURE_IMPLICITS
val EXTS : forall 'n 'm , 'm >= 'n . bits('n) -> bits('m)
diff --git a/model/prelude_mem.sail b/model/prelude_mem.sail
index 8e483f8..b6fa0bc 100644
--- a/model/prelude_mem.sail
+++ b/model/prelude_mem.sail
@@ -2,22 +2,22 @@
* They depend on the XLEN of the architecture.
*/
-val __WriteRAM = {lem: "MEMw", _: "write_ram"} : forall 'n 'm.
+val __WriteRAM = {lem: "MEMw", coq: "MEMw", _: "write_ram"} : forall 'n 'm.
(atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv}
-val __WriteRAM_release = {lem: "MEMw_release", _: "write_ram"} : forall 'n 'm.
+val __WriteRAM_release = {lem: "MEMw_release", coq: "MEMw_release", _: "write_ram"} : forall 'n 'm.
(atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv}
-val __WriteRAM_strong_release = {lem: "MEMw_strong_release", _: "write_ram"} : forall 'n 'm.
+val __WriteRAM_strong_release = {lem: "MEMw_strong_release", coq: "MEMw_strong_release", _: "write_ram"} : forall 'n 'm.
(atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv}
-val __WriteRAM_conditional = {lem: "MEMw_conditional", _: "write_ram"} : forall 'n 'm.
+val __WriteRAM_conditional = {lem: "MEMw_conditional", coq: "MEMw_conditional", _: "write_ram"} : forall 'n 'm.
(atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv}
-val __WriteRAM_conditional_release = {lem: "MEMw_conditional_release", _: "write_ram"} : forall 'n 'm.
+val __WriteRAM_conditional_release = {lem: "MEMw_conditional_release", coq: "MEMw_conditional_release", _: "write_ram"} : forall 'n 'm.
(atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv}
-val __WriteRAM_conditional_strong_release = {lem: "MEMw_conditional_strong_release", _: "write_ram"} : forall 'n 'm.
+val __WriteRAM_conditional_strong_release = {lem: "MEMw_conditional_strong_release", coq: "MEMw_conditional_strong_release", _: "write_ram"} : forall 'n 'm.
(atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv}
val __RISCV_write : forall 'n. (xlenbits, atom('n), bits(8 * 'n), bool, bool, bool) -> bool effect {wmv}
@@ -36,22 +36,22 @@ function __RISCV_write (addr, width, data, aq, rl, con) =
val __TraceMemoryWrite : forall 'n 'm.
(atom('n), bits('m), bits(8 * 'n)) -> unit
-val __ReadRAM = { lem: "MEMr", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
+val __ReadRAM = { lem: "MEMr", coq: "MEMr", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
(atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
-val __ReadRAM_acquire = { lem: "MEMr_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
+val __ReadRAM_acquire = { lem: "MEMr_acquire", coq: "MEMr_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
(atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
-val __ReadRAM_strong_acquire = { lem: "MEMr_strong_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
+val __ReadRAM_strong_acquire = { lem: "MEMr_strong_acquire", coq: "MEMr_strong_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
(atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
-val __ReadRAM_reserved = { lem: "MEMr_reserved", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
+val __ReadRAM_reserved = { lem: "MEMr_reserved", coq: "MEMr_reserved", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
(atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
-val __ReadRAM_reserved_acquire = { lem: "MEMr_reserved_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
+val __ReadRAM_reserved_acquire = { lem: "MEMr_reserved_acquire", coq: "MEMr_reserved_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
(atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
-val __ReadRAM_reserved_strong_acquire = { lem: "MEMr_reserved_strong_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
+val __ReadRAM_reserved_strong_acquire = { lem: "MEMr_reserved_strong_acquire", coq: "MEMr_reserved_strong_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
(atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
val __RISCV_read : forall 'n, 'n >= 0. (xlenbits, atom('n), bool, bool, bool) -> option(bits(8 * 'n)) effect {rmem}
diff --git a/model/riscv_insts_cext.sail b/model/riscv_insts_cext.sail
index 70d4978..4986278 100644
--- a/model/riscv_insts_cext.sail
+++ b/model/riscv_insts_cext.sail
@@ -150,13 +150,8 @@ mapping clause encdec_compressed = C_ADDIW(imm5 @ imm40, rsd)
<-> 0b001 @ imm5 : bits(1) @ rsd : regbits @ imm40 : bits(5) @ 0b01
if rsd != zreg & sizeof(xlen) == 64
-function clause execute (C_ADDIW(imm, rsd)) = {
- let imm : bits(32) = EXTS(imm);
- let rs_val = X(rsd);
- let res : bits(32) = rs_val[31..0] + imm;
- X(rsd) = EXTS(res);
- true
-}
+function clause execute (C_ADDIW(imm, rsd)) =
+ execute(ADDIW(EXTS(imm), rsd, rsd))
mapping clause assembly = C_ADDIW(imm, rsd)
if sizeof(xlen) == 64
diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail
index 2f02839..4155d66 100644
--- a/model/riscv_sys_control.sail
+++ b/model/riscv_sys_control.sail
@@ -415,18 +415,19 @@ function handle_interrupt(i : InterruptType, del_priv : Privilege) -> unit =
/* state state initialization */
+val sys_enable_rvc = {c: "sys_enable_rvc", ocaml: "Platform.enable_rvc", _: "sys_enable_rvc"} : unit -> bool
function init_sys() -> unit = {
cur_privilege = Machine;
mhartid = EXTZ(0b0);
misa->MXL() = arch_to_bits(if sizeof(xlen) == 32 then RV32 else RV64);
- misa->A() = true; /* atomics */
- misa->C() = true; /* RVC */
- misa->I() = true; /* base integer ISA */
- misa->M() = true; /* integer multiply/divide */
- misa->U() = true; /* user-mode */
- misa->S() = true; /* supervisor-mode */
+ misa->A() = true; /* atomics */
+ misa->C() = sys_enable_rvc (); /* RVC */
+ misa->I() = true; /* base integer ISA */
+ misa->M() = true; /* integer multiply/divide */
+ misa->U() = true; /* user-mode */
+ misa->S() = true; /* supervisor-mode */
mstatus = set_mstatus_SXL(mstatus, misa.MXL());
mstatus = set_mstatus_UXL(mstatus, misa.MXL());
diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail
index 439d12d..fb8a994 100644
--- a/model/riscv_sys_regs.sail
+++ b/model/riscv_sys_regs.sail
@@ -70,13 +70,19 @@ bitfield Misa : xlenbits = {
}
register misa : Misa
+val sys_enable_writable_misa = {c: "sys_enable_writable_misa", ocaml: "Platform.enable_writable_misa", _: "sys_enable_writable_misa"} : unit -> bool
+
+/* We currently only support dynamic changes for the C extension. */
function legalize_misa(m : Misa, v : xlenbits) -> Misa = {
- /* Allow modifications to C. */
- let v = Mk_Misa(v);
- // Suppress changing C if nextPC would become misaligned.
- if v.C() == false & nextPC[1] == true
- then m
- else update_C(m, v.C())
+ if sys_enable_writable_misa ()
+ then { /* Allow modifications to C only for now. */
+ let v = Mk_Misa(v);
+ /* Suppress changing C if nextPC would become misaligned. */
+ if v.C() == false & nextPC[1] == true
+ then m
+ else update_C(m, v.C())
+ }
+ else m
}
/* helpers to check support for various extensions. */
@@ -319,12 +325,15 @@ function tvec_addr(m : Mtvec, c : Mcause) -> option(xlenbits) = {
register mepc : xlenbits
-// legalizing writes to xepc
-function legalize_xepc(v : xlenbits) -> xlenbits = {
- v & EXTS(if haveRVC() then 0b110 else 0b100)
-}
+/* The xepc legalization zeroes xepc[1:0] when misa.C is hardwired to 0.
+ * When misa.C is writable, it zeroes only xepc[0].
+ */
+function legalize_xepc(v : xlenbits) -> xlenbits =
+ if sys_enable_writable_misa () | misa.C() == true
+ then [v with 0 = bitzero]
+ else v & EXTS(0b100)
-// masking for reads to xepc
+/* masking for reads to xepc */
function pc_alignment_mask() -> xlenbits =
~(EXTZ(if misa.C() == true then 0b00 else 0b10))
diff --git a/ocaml_emulator/platform.ml b/ocaml_emulator/platform.ml
index 45e3d43..95e7c57 100644
--- a/ocaml_emulator/platform.ml
+++ b/ocaml_emulator/platform.ml
@@ -4,8 +4,10 @@ module Elf = Elf_loader;;
(* Platform configuration *)
-let config_enable_dirty_update = ref false
-let config_enable_misaligned_access = ref false
+let config_enable_rvc = ref true
+let config_enable_writable_misa = ref true
+let config_enable_dirty_update = ref false
+let config_enable_misaligned_access = ref false
let config_mtval_has_illegal_inst_bits = ref false
let platform_arch = ref P.RV64
@@ -65,24 +67,27 @@ let make_rom arch start_pc =
*)
rom )
-let enable_dirty_update () = !config_enable_dirty_update
-let enable_misaligned_access () = !config_enable_misaligned_access
-let mtval_has_illegal_inst_bits () = !config_mtval_has_illegal_inst_bits
+let enable_writable_misa () = !config_enable_writable_misa
+let enable_rvc () = !config_enable_rvc
+let enable_dirty_update () = !config_enable_dirty_update
+let enable_misaligned_access () = !config_enable_misaligned_access
+let mtval_has_illegal_inst_bits () = !config_mtval_has_illegal_inst_bits
-let rom_base () = arch_bits_of_int64 P.rom_base
-let rom_size () = arch_bits_of_int !rom_size_ref
+let rom_base () = arch_bits_of_int64 P.rom_base
+let rom_size () = arch_bits_of_int !rom_size_ref
-let dram_base () = arch_bits_of_int64 P.dram_base
-let dram_size () = arch_bits_of_int64 !P.dram_size_ref
-
-let htif_tohost () =
- arch_bits_of_int64 (Big_int.to_int64 (Elf.elf_tohost ()))
+let dram_base () = arch_bits_of_int64 P.dram_base
+let dram_size () = arch_bits_of_int64 !P.dram_size_ref
let clint_base () = arch_bits_of_int64 P.clint_base
let clint_size () = arch_bits_of_int64 P.clint_size
let insns_per_tick () = Big_int.of_int P.insns_per_tick
+let htif_tohost () =
+ arch_bits_of_int64 (Big_int.to_int64 (Elf.elf_tohost ()))
+
+
(* load reservation *)
let speculate_conditional () = true
diff --git a/ocaml_emulator/riscv_ocaml_sim.ml b/ocaml_emulator/riscv_ocaml_sim.ml
index 9046a2f..5f5c716 100644
--- a/ocaml_emulator/riscv_ocaml_sim.ml
+++ b/ocaml_emulator/riscv_ocaml_sim.ml
@@ -40,6 +40,12 @@ let options = Arg.align ([("-dump-dts",
("-mtval-has-illegal-inst-bits",
Arg.Set P.config_mtval_has_illegal_inst_bits,
" mtval stores instruction bits on an illegal instruction exception");
+ ("-disable-rvc",
+ Arg.Clear P.config_enable_rvc,
+ " disable the RVC extension on boot");
+ ("-disable-writable-misa-c",
+ Arg.Clear P.config_enable_writable_misa,
+ " leave misa hardwired to its initial value");
("-ram-size",
Arg.Int PI.set_dram_size,
" size of physical ram memory to use (in MB)");
diff --git a/os-boot/README.md b/os-boot/README.md
index 7077b4a..4d80d39 100644
--- a/os-boot/README.md
+++ b/os-boot/README.md
@@ -7,6 +7,9 @@ output port similar to Spike's HTIF (host-target interface) mechanism,
and an interrupt controller based on Spike's CLINT (core-local
interrupt controller). Console input is not currently supported.
+32-bit OS boots require a workaround for the 64-bit HTIF interface,
+which is currently not supported.
+
Booting Linux with the C backend
--------------------------------
generated by cgit v1.1 at 2024-10-13 03:57:37 +0000