Skip to content

Commit

Permalink
Svadu support
Browse files Browse the repository at this point in the history
Co-authored-by: Aaron Durbin <[email protected]>
  • Loading branch information
adlr and adurbin-rivos committed Jun 3, 2023
1 parent 17a9929 commit 647d418
Show file tree
Hide file tree
Showing 19 changed files with 92 additions and 11 deletions.
3 changes: 3 additions & 0 deletions c_emulator/riscv_platform.c
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,9 @@ bool sys_enable_writable_misa(unit u)
bool plat_enable_dirty_update(unit u)
{ return rv_enable_dirty_update; }

bool plat_enable_svadu(unit u)
{ return rv_enable_svadu; }

bool plat_enable_misaligned_access(unit u)
{ return rv_enable_misaligned; }

Expand Down
1 change: 1 addition & 0 deletions c_emulator/riscv_platform.h
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ bool sys_enable_zfinx(unit);
bool sys_enable_writable_misa(unit);

bool plat_enable_dirty_update(unit);
bool plat_enable_svadu(unit);
bool plat_enable_misaligned_access(unit);
bool plat_mtval_has_illegal_inst_bits(unit);
bool plat_enable_pmp(unit);
Expand Down
1 change: 1 addition & 0 deletions c_emulator/riscv_platform_impl.c
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ bool rv_enable_writable_misa = true;
bool rv_enable_fdext = true;

bool rv_enable_dirty_update = false;
bool rv_enable_svadu = false;
bool rv_enable_misaligned = false;
bool rv_mtval_has_illegal_inst_bits = false;

Expand Down
1 change: 1 addition & 0 deletions c_emulator/riscv_platform_impl.h
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@ extern bool rv_enable_next;
extern bool rv_enable_fdext;
extern bool rv_enable_writable_misa;
extern bool rv_enable_dirty_update;
extern bool rv_enable_svadu;
extern bool rv_enable_misaligned;
extern bool rv_mtval_has_illegal_inst_bits;

Expand Down
10 changes: 10 additions & 0 deletions c_emulator/riscv_sim.c
Original file line number Diff line number Diff line change
Expand Up @@ -109,6 +109,7 @@ char *sailcov_file = NULL;

static struct option options[] = {
{"enable-dirty-update", no_argument, 0, 'd'},
{"enable-svadu", no_argument, 0, 'u'},
{"enable-misaligned", no_argument, 0, 'm'},
{"enable-pmp", no_argument, 0, 'P'},
{"enable-next", no_argument, 0, 'N'},
Expand Down Expand Up @@ -220,6 +221,7 @@ char *process_args(int argc, char **argv)
c = getopt_long(argc, argv,
"a"
"d"
"u"
"m"
"P"
"C"
Expand Down Expand Up @@ -255,6 +257,10 @@ char *process_args(int argc, char **argv)
fprintf(stderr, "enabling dirty update.\n");
rv_enable_dirty_update = true;
break;
case 'u':
fprintf(stderr, "enabling svadu.\n");
rv_enable_svadu = true;
break;
case 'm':
fprintf(stderr, "enabling misaligned access.\n");
rv_enable_misaligned = true;
Expand Down Expand Up @@ -350,6 +356,10 @@ char *process_args(int argc, char **argv)
break;
}
}
if (rv_enable_svadu && rv_enable_dirty_update) {
fprintf(stderr, "Can't enable dirty update and Svadu simultaneously.\n");
exit(1);
}
if (do_dump_dts) dump_dts();
#ifdef RVFI_DII
if (optind > argc || (optind == argc && !rvfi_dii)) print_usage(argv[0], 0);
Expand Down
4 changes: 4 additions & 0 deletions handwritten_support/0.11/riscv_extras.lem
Original file line number Diff line number Diff line change
Expand Up @@ -119,6 +119,10 @@ val plat_enable_dirty_update : unit -> bool
let plat_enable_dirty_update () = false
declare ocaml target_rep function plat_enable_dirty_update = `Platform.enable_dirty_update`

val plat_enable_svadu : unit -> bool
let plat_enable_svadu () = false
declare ocaml target_rep function plat_enable_svadu = `Platform.enable_svadu`

val plat_enable_misaligned_access : unit -> bool
let plat_enable_misaligned_access () = false
declare ocaml target_rep function plat_enable_misaligned_access = `Platform.enable_misaligned_access`
Expand Down
4 changes: 4 additions & 0 deletions handwritten_support/0.11/riscv_extras_sequential.lem
Original file line number Diff line number Diff line change
Expand Up @@ -111,6 +111,10 @@ val plat_enable_dirty_update : unit -> bool
let plat_enable_dirty_update () = false
declare ocaml target_rep function plat_enable_dirty_update = `Platform.enable_dirty_update`

val plat_enable_svadu : unit -> bool
let plat_enable_svadu () = false
declare ocaml target_rep function plat_enable_svadu = `Platform.enable_svadu`

val plat_enable_misaligned_access : unit -> bool
let plat_enable_misaligned_access () = false
declare ocaml target_rep function plat_enable_misaligned_access = `Platform.enable_misaligned_access`
Expand Down
4 changes: 4 additions & 0 deletions handwritten_support/riscv_extras.lem
Original file line number Diff line number Diff line change
Expand Up @@ -189,6 +189,10 @@ val plat_enable_dirty_update : unit -> bool
let plat_enable_dirty_update () = false
declare ocaml target_rep function plat_enable_dirty_update = `Platform.enable_dirty_update`

val plat_enable_svadu : unit -> bool
let plat_enable_svadu () = false
declare ocaml target_rep function plat_enable_svadu = `Platform.enable_svadu`

val plat_enable_misaligned_access : unit -> bool
let plat_enable_misaligned_access () = false
declare ocaml target_rep function plat_enable_misaligned_access = `Platform.enable_misaligned_access`
Expand Down
4 changes: 4 additions & 0 deletions handwritten_support/riscv_extras_sequential.lem
Original file line number Diff line number Diff line change
Expand Up @@ -181,6 +181,10 @@ val plat_enable_dirty_update : unit -> bool
let plat_enable_dirty_update () = false
declare ocaml target_rep function plat_enable_dirty_update = `Platform.enable_dirty_update`

val plat_enable_svadu : unit -> bool
let plat_enable_svadu () = false
declare ocaml target_rep function plat_enable_svadu = `Platform.enable_svadu`

val plat_enable_misaligned_access : unit -> bool
let plat_enable_misaligned_access () = false
declare ocaml target_rep function plat_enable_misaligned_access = `Platform.enable_misaligned_access`
Expand Down
3 changes: 3 additions & 0 deletions model/riscv_csr_map.sail
Original file line number Diff line number Diff line change
Expand Up @@ -165,6 +165,9 @@ mapping clause csr_name_map = 0x7a0 <-> "tselect"
mapping clause csr_name_map = 0x7a1 <-> "tdata1"
mapping clause csr_name_map = 0x7a2 <-> "tdata2"
mapping clause csr_name_map = 0x7a3 <-> "tdata3"
/* menvcfg */
mapping clause csr_name_map = 0x30A <-> "menvcfg"
mapping clause csr_name_map = 0x31A <-> "menvcfgh"

val csr_name : csreg -> string
overload to_str = {csr_name}
Expand Down
6 changes: 6 additions & 0 deletions model/riscv_insts_zicsr.sail
Original file line number Diff line number Diff line change
Expand Up @@ -160,6 +160,10 @@ function readCSR csr : csreg -> xlenbits = {
(0xC81, 32) => mtime[63 .. 32],
(0xC82, 32) => minstret[63 .. 32],

/* menvcfg */
(0x30A, _) => menvcfg.bits()[(sizeof(xlen) - 1) .. 0],
(0x31A, 32) => menvcfg.bits()[63 .. 32],

/* user mode: Zkr */
(0x015, _) => read_seed_csr(),

Expand All @@ -186,6 +190,8 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = {
(0x304, _) => { mie = legalize_mie(mie, value); Some(mie.bits()) },
(0x305, _) => { Some(set_mtvec(value)) },
(0x306, _) => { mcounteren = legalize_mcounteren(mcounteren, value); Some(EXTZ(mcounteren.bits())) },
(0x30A, _) => { menvcfg = legalize_menvcfg(menvcfg, value); Some(menvcfg.bits()[sizeof(xlen) - 1 .. 0]) },
(0x31A, 32) => { menvcfg = legalize_menvcfg_high(menvcfg, value); Some(menvcfg.bits()[63 .. 32]) },
(0x310, 32) => { Some(mstatush.bits()) }, // ignore writes for now
(0x320, _) => { mcountinhibit = legalize_mcountinhibit(mcountinhibit, value); Some(EXTZ(mcountinhibit.bits())) },
(0x340, _) => { mscratch = value; Some(mscratch) },
Expand Down
31 changes: 31 additions & 0 deletions model/riscv_sys_regs.sail
Original file line number Diff line number Diff line change
Expand Up @@ -573,6 +573,37 @@ function retire_instruction() -> unit = {
if minstret_increment then minstret = minstret + 1;
}

/*
* NOTE: This would be better placed in riscv_platform.sail, but that file
* appears _after_ this one in the compile order meaning the valspec
* for this function is unavailable when it's first encountered here.
* Hence it appears here.
*/
val plat_enable_svadu = {ocaml: "Platform.enable_svadu",
interpreter: "Platform.enable_svadu",
c: "plat_enable_svadu",
lem: "plat_enable_svadu"} : unit -> bool

bitfield MEnvCfg : bits(64) = {
HADE : 61
/* Fill in other fields when adding support for them */
}
register menvcfg : MEnvCfg

function legalize_menvcfg_high(c : MEnvCfg, value : bits(32)) -> MEnvCfg = {
/* Subtract 32 from bit offsets as we only have high half here */
if plat_enable_svadu()
then update_HADE(c, [value[61 - 32]])
else c
}

function legalize_menvcfg(c : MEnvCfg, value : xlenbits) -> MEnvCfg = {
if sizeof(xlen) == 64 then
legalize_menvcfg_high(c, value[63..32])
else
c
}

/* informational registers */
register mvendorid : bits(32)
register mimpid : xlenbits
Expand Down
4 changes: 2 additions & 2 deletions model/riscv_vmem_sv32.sail
Original file line number Diff line number Diff line change
Expand Up @@ -199,7 +199,7 @@ function translate32(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) =
match update_PTE_Bits(pteBits, ac, ext_pte) {
None() => TR_Address(ent.pAddr | EXTZ(vAddr & ent.vAddrMask), ext_ptw),
Some(pbits, ext) => {
if not(plat_enable_dirty_update())
if not(should_update_PTE_bits())
then {
/* pte needs dirty/accessed update but that is not enabled */
TR_Failure(PTW_PTE_Update(), ext_ptw)
Expand Down Expand Up @@ -232,7 +232,7 @@ function translate32(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) =
TR_Address(pAddr, ext_ptw)
},
Some(pbits, ext) =>
if not(plat_enable_dirty_update())
if not(should_update_PTE_bits())
then {
/* pte needs dirty/accessed update but that is not enabled */
TR_Failure(PTW_PTE_Update(), ext_ptw)
Expand Down
4 changes: 2 additions & 2 deletions model/riscv_vmem_sv39.sail
Original file line number Diff line number Diff line change
Expand Up @@ -193,7 +193,7 @@ function translate39(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) =
match update_PTE_Bits(pteBits, ac, ext_pte) {
None() => TR_Address(ent.pAddr | EXTZ(vAddr & ent.vAddrMask), ext_ptw),
Some(pbits, ext) => {
if not(plat_enable_dirty_update())
if not(should_update_PTE_bits())
then {
/* pte needs dirty/accessed update but that is not enabled */
TR_Failure(PTW_PTE_Update(), ext_ptw)
Expand Down Expand Up @@ -226,7 +226,7 @@ function translate39(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) =
TR_Address(pAddr, ext_ptw)
},
Some(pbits, ext) =>
if not(plat_enable_dirty_update())
if not(should_update_PTE_bits())
then {
/* pte needs dirty/accessed update but that is not enabled */
TR_Failure(PTW_PTE_Update(), ext_ptw)
Expand Down
2 changes: 1 addition & 1 deletion model/riscv_vmem_sv48.sail
Original file line number Diff line number Diff line change
Expand Up @@ -190,7 +190,7 @@ function translate48(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) =
TR_Address(pAddr, ext_ptw)
},
Some(pbits, ext) =>
if not(plat_enable_dirty_update())
if not(should_update_PTE_bits())
then {
/* pte needs dirty/accessed update but that is not enabled */
TR_Failure(PTW_PTE_Update(), ext_ptw)
Expand Down
4 changes: 4 additions & 0 deletions model/riscv_vmem_tlb.sail
Original file line number Diff line number Diff line change
Expand Up @@ -122,3 +122,7 @@ function flush_TLB_Entry(e, asid, addr) = {
& not(e.global))
}
}

function should_update_PTE_bits() -> bool = {
plat_enable_dirty_update() | (plat_enable_svadu() & menvcfg.HADE() == 0b1)
}
2 changes: 2 additions & 0 deletions ocaml_emulator/platform.ml
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ let config_enable_rvc = ref true
let config_enable_next = ref false
let config_enable_writable_misa = ref true
let config_enable_dirty_update = ref false
let config_enable_svadu = ref false
let config_enable_misaligned_access = ref false
let config_mtval_has_illegal_inst_bits = ref false
let config_enable_pmp = ref false
Expand Down Expand Up @@ -79,6 +80,7 @@ let enable_rvc () = !config_enable_rvc
let enable_next () = !config_enable_next
let enable_fdext () = false
let enable_dirty_update () = !config_enable_dirty_update
let enable_svadu () = !config_enable_svadu
let enable_misaligned_access () = !config_enable_misaligned_access
let mtval_has_illegal_inst_bits () = !config_mtval_has_illegal_inst_bits
let enable_pmp () = !config_enable_pmp
Expand Down
3 changes: 3 additions & 0 deletions ocaml_emulator/riscv_ocaml_sim.ml
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,9 @@ let options = Arg.align ([("-dump-dts",
("-enable-dirty-update",
Arg.Set P.config_enable_dirty_update,
" enable dirty-bit update during page-table walks");
("-enable-svadu",
Arg.Set P.config_enable_svadu,
" enable svadu extension HW updating PTE bits");
("-enable-misaligned-access",
Arg.Set P.config_enable_misaligned_access,
" enable misaligned accesses without M-mode traps");
Expand Down
12 changes: 6 additions & 6 deletions test/run_tests.sh
Original file line number Diff line number Diff line change
Expand Up @@ -55,7 +55,7 @@ cd $RISCVDIR
make clean

printf "Building 32-bit RISCV specification...\n"
if ARCH=RV32 make ocaml_emulator/riscv_ocaml_sim_RV32 ;
if ARCH=RV32 make -j ocaml_emulator/riscv_ocaml_sim_RV32 ;
then
green "Building 32-bit RISCV OCaml emulator" "ok"
else
Expand All @@ -81,7 +81,7 @@ done
finish_suite "32-bit RISCV OCaml tests"


if ARCH=RV32 make c_emulator/riscv_sim_RV32;
if ARCH=RV32 make -j c_emulator/riscv_sim_RV32;
then
green "Building 32-bit RISCV C emulator" "ok"
else
Expand All @@ -102,7 +102,7 @@ make clean

printf "Building 64-bit RISCV specification...\n"

if make ocaml_emulator/riscv_ocaml_sim_RV64 ;
if make -j ocaml_emulator/riscv_ocaml_sim_RV64 ;
then
green "Building 64-bit RISCV OCaml emulator" "ok"
else
Expand All @@ -127,7 +127,7 @@ for test in $DIR/riscv-tests/rv64*.elf; do
done
finish_suite "64-bit RISCV OCaml tests"

if make c_emulator/riscv_sim_RV64;
if make -j c_emulator/riscv_sim_RV64;
then
green "Building 64-bit RISCV C emulator" "ok"
else
Expand All @@ -146,7 +146,7 @@ finish_suite "64-bit RISCV C tests"
# Do 'make clean' to avoid cross-arch pollution.
make clean

if ARCH=RV32 make c_emulator/riscv_rvfi_RV32;
if ARCH=RV32 make -j c_emulator/riscv_rvfi_RV32;
then
green "Building 32-bit RISCV RVFI C emulator" "ok"
else
Expand All @@ -157,7 +157,7 @@ finish_suite "32-bit RISCV RVFI C tests"
# Do 'make clean' to avoid cross-arch pollution.
make clean

if ARCH=RV64 make c_emulator/riscv_rvfi_RV64;
if ARCH=RV64 make -j c_emulator/riscv_rvfi_RV64;
then
green "Building 64-bit RISCV RVFI C emulator" "ok"
else
Expand Down

0 comments on commit 647d418

Please sign in to comment.