From 64e50eaf58e9c96e85a13e2974d488999cf4a7d1 Mon Sep 17 00:00:00 2001 From: Ved Shanbhogue Date: Tue, 28 May 2024 12:01:07 -0500 Subject: [PATCH] Add Smctr, Ssctr, Smcsrind, Sscsrind, Smstateen --- Makefile | 2 + c_emulator/riscv_platform.c | 13 +- c_emulator/riscv_platform.h | 4 + c_emulator/riscv_platform_impl.c | 4 + c_emulator/riscv_platform_impl.h | 4 + c_emulator/riscv_sim.c | 24 ++++ model/riscv_csr_map.sail | 27 ++++ model/riscv_ctr_regs.sail | 210 ++++++++++++++++++++++++++++++ model/riscv_insts_base.sail | 12 +- model/riscv_insts_ctr.sail | 209 +++++++++++++++++++++++++++++ model/riscv_insts_zicsr.sail | 49 +++++++ model/riscv_jalr_rmem.sail | 4 + model/riscv_jalr_seq.sail | 4 + model/riscv_platform.sail | 4 + model/riscv_sys_control.sail | 52 ++++++++ model/riscv_sys_regs.sail | 191 +++++++++++++++++++++++++++ ocaml_emulator/platform.ml | 8 ++ ocaml_emulator/riscv_ocaml_sim.ml | 11 +- 18 files changed, 829 insertions(+), 3 deletions(-) create mode 100644 model/riscv_ctr_regs.sail create mode 100644 model/riscv_insts_ctr.sail diff --git a/Makefile b/Makefile index ea6244a43..246affcaa 100644 --- a/Makefile +++ b/Makefile @@ -28,6 +28,7 @@ SAIL_DEFAULT_INST += riscv_insts_fext.sail riscv_insts_cfext.sail SAIL_DEFAULT_INST += riscv_insts_dext.sail riscv_insts_cdext.sail SAIL_DEFAULT_INST += riscv_insts_svinval.sail +SAIL_DEFAULT_INST += riscv_insts_ctr.sail SAIL_DEFAULT_INST += riscv_insts_zba.sail SAIL_DEFAULT_INST += riscv_insts_zbb.sail @@ -68,6 +69,7 @@ SAIL_RMEM_INST_SRCS = riscv_insts_begin.sail $(SAIL_RMEM_INST) riscv_insts_end.s SAIL_SYS_SRCS = riscv_csr_map.sail SAIL_SYS_SRCS += riscv_vext_control.sail # helpers for the 'V' extension SAIL_SYS_SRCS += riscv_next_regs.sail +SAIL_SYS_SRCS += riscv_ctr_regs.sail SAIL_SYS_SRCS += riscv_sys_exceptions.sail # default basic helpers for exception handling SAIL_SYS_SRCS += riscv_sync_exception.sail # define the exception structure used in the model SAIL_SYS_SRCS += riscv_next_control.sail # helpers for the 'N' extension diff --git a/c_emulator/riscv_platform.c b/c_emulator/riscv_platform.c index 2fdb63f92..aa321326e 100644 --- a/c_emulator/riscv_platform.c +++ b/c_emulator/riscv_platform.c @@ -71,7 +71,18 @@ bool sys_enable_writable_misa(unit u) { return rv_enable_writable_misa; } - +uint64_t sys_valid_ctr_depth(unit u) +{ + return rv_valid_ctr_depth; +} +bool sys_enable_ssctr(unit u) +{ + return rv_enable_ssctr; +} +bool sys_enable_smctr(unit u) +{ + return rv_enable_smctr; +} 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 341bd5964..df2591d11 100644 --- a/c_emulator/riscv_platform.h +++ b/c_emulator/riscv_platform.h @@ -11,6 +11,10 @@ bool sys_enable_writable_misa(unit); bool sys_enable_writable_fiom(unit); bool sys_enable_vext(unit); +uint64_t sys_valid_ctr_depth(unit u); +bool sys_enable_ssctr(unit u); +bool sys_enable_smctr(unit u); + uint64_t sys_pmp_count(unit); uint64_t sys_pmp_grain(unit); diff --git a/c_emulator/riscv_platform_impl.c b/c_emulator/riscv_platform_impl.c index 077fc50dc..51b40c8fe 100644 --- a/c_emulator/riscv_platform_impl.c +++ b/c_emulator/riscv_platform_impl.c @@ -6,6 +6,10 @@ uint64_t rv_pmp_count = 0; uint64_t rv_pmp_grain = 0; +uint64_t rv_valid_ctr_depth = 0x1F; +bool rv_enable_smctr = true; +bool rv_enable_ssctr = true; + bool rv_enable_svinval = false; bool rv_enable_zcb = false; bool rv_enable_zfinx = false; diff --git a/c_emulator/riscv_platform_impl.h b/c_emulator/riscv_platform_impl.h index c4289e679..7d3450037 100644 --- a/c_emulator/riscv_platform_impl.h +++ b/c_emulator/riscv_platform_impl.h @@ -11,6 +11,10 @@ extern uint64_t rv_pmp_count; extern uint64_t rv_pmp_grain; +extern uint64_t rv_valid_ctr_depth; +extern bool rv_enable_smctr; +extern bool rv_enable_ssctr; + extern bool rv_enable_svinval; extern bool rv_enable_zcb; extern bool rv_enable_zfinx; diff --git a/c_emulator/riscv_sim.c b/c_emulator/riscv_sim.c index 3a9bfc08d..dd278951c 100644 --- a/c_emulator/riscv_sim.c +++ b/c_emulator/riscv_sim.c @@ -54,6 +54,9 @@ const char *RV32ISA = "RV32IMAC"; #define OPT_PMP_COUNT 1002 #define OPT_PMP_GRAIN 1003 #define OPT_ENABLE_SVINVAL 1004 +#define OPT_ENABLE_SMCTR 1005 +#define OPT_ENABLE_SSCTR 1006 +#define OPT_VALID_CTR_DEPTH 1007 #define OPT_ENABLE_ZCB 10014 static bool do_dump_dts = false; @@ -149,6 +152,9 @@ static struct option options[] = { {"enable-writable-fiom", no_argument, 0, OPT_ENABLE_WRITABLE_FIOM}, {"enable-svinval", no_argument, 0, OPT_ENABLE_SVINVAL }, {"enable-zcb", no_argument, 0, OPT_ENABLE_ZCB }, + {"valid-ctr-depth", required_argument, 0, OPT_VALID_CTR_DEPTH }, + {"enable-smctr", no_argument, 0, OPT_ENABLE_SMCTR }, + {"enable-ssctr", no_argument, 0, OPT_ENABLE_SSCTR }, #ifdef SAILCOV {"sailcov-file", required_argument, 0, 'c' }, #endif @@ -245,6 +251,8 @@ static int process_args(int argc, char **argv) uint64_t ram_size = 0; uint64_t pmp_count = 0; uint64_t pmp_grain = 0; + uint64_t valid_ctr_depth = 0; + while (true) { c = getopt_long(argc, argv, "a" @@ -394,6 +402,22 @@ static int process_args(int argc, char **argv) fprintf(stderr, "enabling Zcb extension.\n"); rv_enable_zcb = true; break; + case OPT_ENABLE_SMCTR: + fprintf(stderr, "enabling Smctr extension.\n"); + rv_enable_smctr = true; + break; + case OPT_ENABLE_SSCTR: + fprintf(stderr, "enabling Ssctr extension.\n"); + rv_enable_ssctr = true; + break; + case OPT_VALID_CTR_DEPTH: + rv_valid_ctr_depth = atol(optarg); + fprintf(stderr, "Valid CTR depth: %" PRIu64 "\n", rv_valid_ctr_depth); + if (rv_valid_ctr_depth > 0x1F) { + fprintf(stderr, "invalid CTR depth"); + exit(1); + } + break; case 'x': fprintf(stderr, "enabling Zfinx support.\n"); rv_enable_zfinx = true; diff --git a/model/riscv_csr_map.sail b/model/riscv_csr_map.sail index 22cffd5a6..cc9530d65 100644 --- a/model/riscv_csr_map.sail +++ b/model/riscv_csr_map.sail @@ -49,8 +49,22 @@ mapping clause csr_name_map = 0x141 <-> "sepc" mapping clause csr_name_map = 0x142 <-> "scause" mapping clause csr_name_map = 0x143 <-> "stval" mapping clause csr_name_map = 0x144 <-> "sip" +/* Supervisor Control Transfer Records Control Register */ +mapping clause csr_name_map = 0x14E <-> "sctrctl" +/* Supervisor Control Transfer Records Status Register */ +mapping clause csr_name_map = 0x14F <-> "sctrstatus" /* supervisor protection and translation */ mapping clause csr_name_map = 0x180 <-> "satp" +/* supervisor indirect register select and alias CSRs */ +mapping clause csr_name_map = 0x150 <-> "siselect" +mapping clause csr_name_map = 0x151 <-> "sireg" +mapping clause csr_name_map = 0x152 <-> "sireg2" +mapping clause csr_name_map = 0x153 <-> "sireg3" +mapping clause csr_name_map = 0x155 <-> "sireg4" +mapping clause csr_name_map = 0x156 <-> "sireg5" +mapping clause csr_name_map = 0x157 <-> "sireg6" +/* Supervisor Control Transfer Records Depth Register */ +mapping clause csr_name_map = 0x15F <-> "sctrdepth" /* supervisor envcfg */ mapping clause csr_name_map = 0x10A <-> "senvcfg" /* machine information registers */ @@ -70,12 +84,25 @@ mapping clause csr_name_map = 0x306 <-> "mcounteren" mapping clause csr_name_map = 0x320 <-> "mcountinhibit" /* machine envcfg */ mapping clause csr_name_map = 0x30A <-> "menvcfg" +/* Smstateen csrs */ +mapping clause csr_name_map = 0x30C <-> "mstateen0" +mapping clause csr_name_map = 0x31C <-> "mstateen0h" /* machine trap handling */ mapping clause csr_name_map = 0x340 <-> "mscratch" mapping clause csr_name_map = 0x341 <-> "mepc" mapping clause csr_name_map = 0x342 <-> "mcause" mapping clause csr_name_map = 0x343 <-> "mtval" mapping clause csr_name_map = 0x344 <-> "mip" +/* Machine Control Transfer Records Control Register */ +mapping clause csr_name_map = 0x34E <-> "mctrctl" +/* Machine indirect register select and alias CSRs */ +mapping clause csr_name_map = 0x350 <-> "miselect" +mapping clause csr_name_map = 0x351 <-> "mireg" +mapping clause csr_name_map = 0x352 <-> "mireg2" +mapping clause csr_name_map = 0x353 <-> "mireg3" +mapping clause csr_name_map = 0x355 <-> "mireg4" +mapping clause csr_name_map = 0x356 <-> "mireg5" +mapping clause csr_name_map = 0x357 <-> "mireg6" /* machine protection and translation */ mapping clause csr_name_map = 0x3A0 <-> "pmpcfg0" mapping clause csr_name_map = 0x3A1 <-> "pmpcfg1" diff --git a/model/riscv_ctr_regs.sail b/model/riscv_ctr_regs.sail new file mode 100644 index 000000000..1c88e55f3 --- /dev/null +++ b/model/riscv_ctr_regs.sail @@ -0,0 +1,210 @@ +/*=======================================================================================*/ +/* This Sail RISC-V architecture model, comprising all files and */ +/* directories except where otherwise noted is subject the BSD */ +/* two-clause license in the LICENSE file. */ +/* */ +/* SPDX-License-Identifier: BSD-2-Clause */ +/*=======================================================================================*/ + +/* Support CTR depths - if bit n is set then CTR depth 2^n is supported */ +val sys_valid_ctr_depth = {c: "sys_valid_ctr_depth", ocaml: "Platform.valid_ctr_depth", _: "sys_valid_ctr_depth"} : unit -> bits(64) + +/* Architectural state for the Ssctr and Smctr standard extension. */ +bitfield Mctrctl : bits(64) = { + DIRLJMPINH : 47, + INDLJMPINH : 46, + RETINH : 45, + CORSWAPINH : 44, + DIRJMPINH : 43, + INDJMPINH : 42, + DIRCALLINH : 41, + INDCALLINH : 40, + TKBRINH : 37, + NTBREN : 36, + TRETINH : 35, + INTRINH : 34, + EXCINH : 33, + + LCOFIFRZ : 12, + BPFRZ : 11, + + MTE : 9, + STE : 8, + + RASEMU : 7, + + M : 2, + S : 1, + U : 0 +} +bitfield Sctrctl : bits(64) = { + DIRLJMPINH : 47, + INDLJMPINH : 46, + RETINH : 45, + CORSWAPINH : 44, + DIRJMPINH : 43, + INDJMPINH : 42, + DIRCALLINH : 41, + INDCALLINH : 40, + TKBRINH : 37, + NTBREN : 36, + TRETINH : 35, + INTRINH : 34, + EXCINH : 33, + + LCOFIFRZ : 12, + BPFRZ : 11, + + STE : 8, + + RASEMU : 7, + + S : 1, + U : 0 +} +bitfield Sctrdepth : bits(32) = { + DEPTH : 2 .. 0 +} +bitfield Sctrstatus : bits(32) = { + FROZEN : 31, + WRPTR : 7 .. 0 +} +bitfield Ctrsource : xlenbits = { + PC : xlen - 1 .. 1, + V : 0 +} +bitfield Ctrtarget : xlenbits = { + PC : xlen - 1 .. 1, + MISP : 0 +} +bitfield Ctrdata : bits(64) = { + CCE : 31 .. 28, + CCM : 27 .. 16, + CCV : 15, + TYPE : 3 .. 0 +} + +register sctrstatus : Sctrstatus +register sctrdepth : Sctrdepth +register mctrctl : Mctrctl +register ctrsource : vector(256, dec, Ctrsource) +register ctrtarget : vector(256, dec, Ctrtarget) +register ctrdata : vector(256, dec, Ctrdata) +/* Should parameterize the cycle counter to support wider counters */ +register ctr_cycle_counter : bits(13) +register ctr_cycle_counter_valid : bool + +function legalize_mctrctl(o : Mctrctl, v : xlenbits) -> Mctrctl = { + let m : Mctrctl = Mk_Mctrctl(zero_extend(v)); + m +} + +function lower_sctrctl(m : Mctrctl) -> Sctrctl = { + let s = Mk_Sctrctl(m.bits); + s +} + +function legalize_sctrctl(m : Mctrctl, v : xlenbits) -> Mctrctl = { + let o = Mk_Mctrctl(zero_extend(v)); + let o = [o with M = m[M], MTE = m[MTE]]; + o +} + + +function get_wrptr_mask(d : Sctrdepth) -> bits(8) = + match(d[DEPTH]) { + 0b000 => 0b00001111, + 0b001 => 0b00011111, + 0b010 => 0b00111111, + 0b011 => 0b01111111, + 0b100 => 0b11111111, + _ => internal_error(__FILE__, __LINE__, "Unexpected DEPTH encoding") + } + +function legalize_sctrdepth(s : Sctrdepth, v : xlenbits) -> Sctrdepth = { + let valid_ctr_depth : bits(64) = sys_valid_ctr_depth(); + let depth : bits(3) = match(v[2 .. 0]) { + 0b000 => if bit_to_bool(valid_ctr_depth[0]) then v[2 .. 0] else s[DEPTH], + 0b001 => if bit_to_bool(valid_ctr_depth[1]) then v[2 .. 0] else s[DEPTH], + 0b010 => if bit_to_bool(valid_ctr_depth[2]) then v[2 .. 0] else s[DEPTH], + 0b011 => if bit_to_bool(valid_ctr_depth[3]) then v[2 .. 0] else s[DEPTH], + 0b100 => if bit_to_bool(valid_ctr_depth[4]) then v[2 .. 0] else s[DEPTH], + _ => s[DEPTH] + }; + let o = Mk_Sctrdepth(zero_extend(depth)); + + /* On depth change WRPTR assumes an unspecified but legal value */ + sctrstatus[WRPTR] = sctrstatus[WRPTR] & get_wrptr_mask(o); + + o +} +function legalize_sctrstatus(s : Sctrstatus, v : xlenbits) -> Sctrstatus = { + let wrptr_mask : bits(8) = get_wrptr_mask(sctrdepth); + let o = Mk_Sctrstatus(zeros()); + let o = [o with WRPTR = (v[7 .. 0] & wrptr_mask), FROZEN = v[31 .. 31]]; + o +} +function number_of_ctr() -> int = { + let valid_ctr_depth : bits(64) = sys_valid_ctr_depth(); + let num = if bit_to_bool(valid_ctr_depth[0]) then 16 else 0; + let num = if bit_to_bool(valid_ctr_depth[1]) then 32 else num; + let num = if bit_to_bool(valid_ctr_depth[2]) then 64 else num; + let num = if bit_to_bool(valid_ctr_depth[3]) then 128 else num; + let num = if bit_to_bool(valid_ctr_depth[4]) then 256 else num; + num +} +function isValidCtrMiselect() -> bool = { + let ctr_select = miselect.bits[7 .. 0]; + haveSmctr() & (unsigned(ctr_select) < number_of_ctr()) +} +function isValidCtrSiselect() -> bool = { + let ctr_select = siselect.bits[7 .. 0]; + haveSsctr() & (unsigned(ctr_select) < number_of_ctr()) +} +/* Logical entry N, selected by *iselect value of (0x200 | N), is + * physically at ((WRPTR - N - 1) % depth) where depth = 2^(DEPTH+4) + */ +function get_ctr_idx(iselect : SMiselect) -> bits(8) = { + let ctr_idx = sctrstatus[WRPTR] - iselect.bits[7 .. 0] - 1; + ctr_idx & get_wrptr_mask(sctrdepth); +} + +function get_ctr_mireg() -> xlenbits = + ctrsource[unsigned(get_ctr_idx(miselect))].bits + +function get_ctr_mireg2() -> xlenbits = + ctrtarget[unsigned(get_ctr_idx(miselect))].bits + +function get_ctr_mireg3() -> xlenbits = + if sizeof(xlen) == 32 + then ctrdata[unsigned(get_ctr_idx(miselect))].bits[31 .. 0] + else ctrdata[unsigned(get_ctr_idx(miselect))].bits[63 .. 0] + +function set_ctr_mireg(v: xlenbits) -> unit = + ctrsource[unsigned(get_ctr_idx(miselect))] = Mk_Ctrsource(v) + +function set_ctr_mireg2(v: xlenbits) -> unit = + ctrtarget[unsigned(get_ctr_idx(miselect))] = Mk_Ctrtarget(v) + +function set_ctr_mireg3(v: xlenbits) -> unit = + ctrdata[unsigned(get_ctr_idx(miselect))] = Mk_Ctrdata(zero_extend(v)) + +function get_ctr_sireg() -> xlenbits = + ctrsource[unsigned(get_ctr_idx(siselect))].bits + +function get_ctr_sireg2() -> xlenbits = + ctrtarget[unsigned(get_ctr_idx(siselect))].bits + +function get_ctr_sireg3() -> xlenbits = + if sizeof(xlen) == 32 + then ctrdata[unsigned(get_ctr_idx(miselect))].bits[31 .. 0] + else ctrdata[unsigned(get_ctr_idx(miselect))].bits[63 .. 0] + +function set_ctr_sireg(v: xlenbits) -> unit = + ctrsource[unsigned(get_ctr_idx(siselect))] = Mk_Ctrsource(v) + +function set_ctr_sireg2(v: xlenbits) -> unit = + ctrtarget[unsigned(get_ctr_idx(siselect))] = Mk_Ctrtarget(v) + +function set_ctr_sireg3(v: xlenbits) -> unit = + ctrdata[unsigned(get_ctr_idx(siselect))] = Mk_Ctrdata(zero_extend(v)) diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail index 8d86804ed..bb7763149 100644 --- a/model/riscv_insts_base.sail +++ b/model/riscv_insts_base.sail @@ -57,6 +57,7 @@ match bv { but this is difficult */ +val update_ctr_jal : regidx -> unit function clause execute (RISCV_JAL(imm, rd)) = { let t : xlenbits = PC + sign_extend(imm); /* Extensions get the first checks on the prospective target address. */ @@ -74,6 +75,8 @@ function clause execute (RISCV_JAL(imm, rd)) = { } else { X(rd) = get_next_pc(); set_next_pc(target); + /* update control transfer record if Ssctr/Smctr is active */ + update_ctr_jal(rd); RETIRE_SUCCESS } } @@ -111,6 +114,7 @@ mapping encdec_bop : bop <-> bits(3) = { mapping clause encdec = BTYPE(imm7_6 @ imm5_0 @ imm7_5_0 @ imm5_4_1 @ 0b0, rs2, rs1, op) <-> imm7_6 : bits(1) @ imm7_5_0 : bits(6) @ rs2 @ rs1 @ encdec_bop(op) @ imm5_4_1 : bits(4) @ imm5_0 : bits(1) @ 0b1100011 +val update_ctr_conditional: (bool) -> unit function clause execute (BTYPE(imm, rs2, rs1, op)) = { let rs1_val = X(rs1); let rs2_val = X(rs2); @@ -136,11 +140,17 @@ function clause execute (BTYPE(imm, rs2, rs1, op)) = { RETIRE_FAIL; } else { set_next_pc(target); + /* Update control transfer record if Smctr/Ssctr is active */ + update_ctr_conditional(true); RETIRE_SUCCESS } } } - } else RETIRE_SUCCESS + } else { + /* Update control transfer record if Smctr/Ssctr is active */ + update_ctr_conditional(false); + RETIRE_SUCCESS + } } mapping btype_mnemonic : bop <-> string = { diff --git a/model/riscv_insts_ctr.sail b/model/riscv_insts_ctr.sail new file mode 100644 index 000000000..39942d40a --- /dev/null +++ b/model/riscv_insts_ctr.sail @@ -0,0 +1,209 @@ +/*=======================================================================================*/ +/* This Sail RISC-V architecture model, comprising all files and */ +/* directories except where otherwise noted is subject the BSD */ +/* two-clause license in the LICENSE file. */ +/* */ +/* SPDX-License-Identifier: BSD-2-Clause */ +/*=======================================================================================*/ + +/* ***************************************************************************/ +/* This file specifies the instruction added by the 'Smctr/Ssctr' extension. */ + +union clause ast = SCTRCLR : unit + +mapping clause encdec = SCTRCLR() + <-> 0b000100000100 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 + +function clause execute SCTRCLR() = { + let sctrclr_illegal : bool = match cur_privilege { + User => true, + Supervisor => not(haveSsctr()) | mstateen0[CTR] == 0b0, + Machine => not(haveSmctr()) + }; + if sctrclr_illegal + then { handle_illegal(); RETIRE_FAIL } + else { + foreach (i from 0 to 255) { + ctrsource[i] = Mk_Ctrsource(zeros()); + ctrtarget[i] = Mk_Ctrtarget(zeros()); + ctrdata[i] = Mk_Ctrdata(zeros()); + }; + ctr_cycle_counter = zeros(); + ctr_cycle_counter_valid = false; + RETIRE_SUCCESS + } +} + +mapping clause assembly = SCTRCLR() <-> "sctrclr" +/* ***************************************************************************/ + +val get_wrptr_mask : Sctrdepth -> bits(8) + +/* The following functions are extensions to JAL/JALR instructions to + * update control transfer records + */ +enum ctr_xfer_type = { + EXCEPTION, + INTERRUPT, + TRAP_RETURN, + NOT_TAKEN_BRANCH, + TAKEN_BRANCH, + INDIRECT_CALL, + DIRECT_CALL, + INDIRECT_JUMP_NO_LINKAGE, + DIRECT_JUMP_NO_LINKAGE, + COROUTINE_SWAP, + FUNCTION_RETURN, + OTHER_INDIRECT_JUMP_WITH_LINKAGE, + OTHER_DIRECT_JUMP_WITH_LINKAGE + } + +mapping encdec_ctr_xfer_type : ctr_xfer_type <-> bits(4) = { + EXCEPTION <-> 0b0001, + INTERRUPT <-> 0b0010, + TRAP_RETURN <-> 0b0011, + NOT_TAKEN_BRANCH <-> 0b0100, + TAKEN_BRANCH <-> 0b0101, + INDIRECT_CALL <-> 0b1000, + DIRECT_CALL <-> 0b1001, + INDIRECT_JUMP_NO_LINKAGE <-> 0b1010, + DIRECT_JUMP_NO_LINKAGE <-> 0b1011, + COROUTINE_SWAP <-> 0b1100, + FUNCTION_RETURN <-> 0b1101, + OTHER_INDIRECT_JUMP_WITH_LINKAGE <-> 0b1110, + OTHER_DIRECT_JUMP_WITH_LINKAGE <-> 0b1111 +} + +function isSsctrEnabled() -> bool = + match(haveSmstateen(), mstateen0[CTR]) { + (false, _) => false, + (true, 0b0) => false, + (true, 0b1) => haveSsctr() + } + +function is_ctr_active(priv : Privilege) -> bool = + match priv { + User => isSsctrEnabled() & mctrctl[U] == 0b1 & sctrstatus[FROZEN] == 0b0, + Supervisor => isSsctrEnabled() & mctrctl[S] == 0b1 & sctrstatus[FROZEN] == 0b0, + Machine => haveSmctr() & mctrctl[M] == 0b1 & sctrstatus[FROZEN] == 0b0 + } + + +function update_ctr(transfer_type : ctr_xfer_type, src_recorded : bool, dst_recorded : bool) -> unit = { + let src_pc : xlenbits = if src_recorded then get_arch_pc() else zeros(); + let tgt_pc : xlenbits = if dst_recorded then get_next_pc() else zeros(); + let ras_emu : bool = mctrctl[RASEMU] == 0b1; + let cce : bits(1) = ctr_cycle_counter[12 .. 12]; + let ccm : bits(12) = ctr_cycle_counter[11 .. 0]; + let ccv : bits(1) = if ctr_cycle_counter_valid & not(ras_emu) then 0b1 else 0b0; + + /* Transfer type filtering */ + let is_transfer_type_enabled : bool = match transfer_type { + EXCEPTION => mctrctl[EXCINH] == 0b0 & not(ras_emu), + INTERRUPT => mctrctl[INTRINH] == 0b0 & not(ras_emu), + TRAP_RETURN => mctrctl[TRETINH] == 0b0 & not(ras_emu), + NOT_TAKEN_BRANCH => mctrctl[NTBREN] == 0b1 & not(ras_emu), + TAKEN_BRANCH => mctrctl[TKBRINH] == 0b0 & not(ras_emu), + INDIRECT_CALL => mctrctl[INDCALLINH] == 0b0 | ras_emu, + DIRECT_CALL => mctrctl[DIRCALLINH] == 0b0 | ras_emu, + INDIRECT_JUMP_NO_LINKAGE => mctrctl[INDJMPINH] == 0b0 & not(ras_emu), + DIRECT_JUMP_NO_LINKAGE => mctrctl[DIRJMPINH] == 0b0 & not(ras_emu), + COROUTINE_SWAP => mctrctl[CORSWAPINH] == 0b0 | not(ras_emu), + FUNCTION_RETURN => mctrctl[RETINH] == 0b0 | ras_emu, + OTHER_INDIRECT_JUMP_WITH_LINKAGE => mctrctl[INDLJMPINH] == 0b0 & not(ras_emu), + OTHER_DIRECT_JUMP_WITH_LINKAGE => mctrctl[DIRLJMPINH] == 0b0 & not(ras_emu), + }; + + /* In RAS emulation, function returns pop but coroutine swaps pop and then push */ + if ras_emu & (transfer_type == FUNCTION_RETURN | transfer_type == COROUTINE_SWAP) then { + sctrstatus[WRPTR] = (sctrstatus[WRPTR] - 1) & get_wrptr_mask(sctrdepth); + ctrsource[unsigned(sctrstatus[WRPTR])] = [ctrsource[unsigned(sctrstatus[WRPTR])] with V = 0b0]; + }; + + let do_push : bool = is_transfer_type_enabled & (not(ras_emu) | (ras_emu & transfer_type != FUNCTION_RETURN)); + + if do_push then { + cycle_counter_valid = false; + ctr_cycle_counter = zeros(); + ctrsource[unsigned(sctrstatus[WRPTR])] = Mk_Ctrsource(src_pc[(sizeof(xlen) - 1) .. 1] @ 0b1); + ctrtarget[unsigned(sctrstatus[WRPTR])] = Mk_Ctrtarget(tgt_pc[(sizeof(xlen) - 1) .. 1] @ 0b0); + ctrdata[unsigned(sctrstatus[WRPTR])] = + Mk_Ctrdata(zero_extend(cce @ ccm @ ccv @ 0b00000000000 @ encdec_ctr_xfer_type(transfer_type))); + sctrstatus[WRPTR] = (sctrstatus[WRPTR] + 1) & get_wrptr_mask(sctrdepth); + } +} + +function update_ctr_jal(rd : regidx) -> unit = { + if rd == 0b00000 & is_ctr_active(cur_privilege) + then update_ctr(DIRECT_JUMP_NO_LINKAGE, true, true) + else if (rd == 0b00001 | rd == 0b00101) & is_ctr_active(cur_privilege) + then update_ctr(DIRECT_CALL, true, true) + else if is_ctr_active(cur_privilege) + then update_ctr(OTHER_DIRECT_JUMP_WITH_LINKAGE, true, true); +} + +function update_ctr_jalr(rs1 : regidx, rd : regidx) -> unit = { + if ((rs1 != 0b00101 & rd == 0b00001) | (rs1 != 0b00001 & rd == 0b00101)) & is_ctr_active(cur_privilege) + then update_ctr(INDIRECT_CALL, true, true) + else if (rs1 != 0b00101 & rs1 != 0b00001 & rd == 0b00000) & is_ctr_active(cur_privilege) + then update_ctr(INDIRECT_JUMP_NO_LINKAGE, true, true) + else if ((rs1 == 0b00001 & rd == 0b00101) | (rs1 == 0b00101 & rd == 0b00001)) & is_ctr_active(cur_privilege) + then update_ctr(COROUTINE_SWAP, true, true) + else if is_ctr_active(cur_privilege) + then update_ctr(OTHER_INDIRECT_JUMP_WITH_LINKAGE, true, true); +} + +function update_ctr_conditional(taken : bool) -> unit = { + if taken & is_ctr_active(cur_privilege) + then update_ctr(TAKEN_BRANCH, true, true) + else if is_ctr_active(cur_privilege) + then update_ctr(NOT_TAKEN_BRANCH, true, true); +} + +function update_ctr_traps(intr : bool, del_priv : Privilege) -> unit = { + let is_src_ctr_enabled : bool = is_ctr_active(cur_privilege); + let is_dst_ctr_enabled : bool = is_ctr_active(del_priv); + let transfer_type : ctr_xfer_type = if intr then INTERRUPT else EXCEPTION; + + let effective_xte : bool = match (cur_privilege, del_priv) { + (User, Supervisor) => mctrctl[STE] == 0b1, + (User, Machine) => mctrctl[STE] == 0b1 & mctrctl[MTE] == 0b1, + (Supervisor, Machine) => mctrctl[MTE] == 0b1, + (_, _) => false + }; + /* Traps between enabled privilege modes are recorded as normal. + * Traps from a disabled privilege mode to an enabled privilege mode + * are partially recorded, such that the ctrsource.PC is 0. Traps from + * an enabled mode to a disabled mode, known as external traps, are + * recorded with ctrtarget.PC as 0 if the effective xTE bit is 1 + */ + if is_src_ctr_enabled & is_dst_ctr_enabled + then update_ctr(transfer_type, true, true) + else if not(is_src_ctr_enabled) & is_dst_ctr_enabled + then update_ctr(transfer_type, false, true) + else if is_src_ctr_enabled & not(is_dst_ctr_enabled) & effective_xte + then update_ctr(transfer_type, true, false) +} + +function update_ctr_trap_return(prev_priv : Privilege) -> unit = { + let is_src_ctr_enabled : bool = is_ctr_active(prev_priv); + let is_dst_ctr_enabled : bool = is_ctr_active(cur_privilege); + + /* Trap returns between enabled privilege modes are recorded + * as normal. Trap returns from an enabled mode back to a disabled mode are + * partially recorded, such that ctrtarget.PC is 0. Trap returns from a + * disabled mode to an enabled mode are not recorded. + */ + if is_src_ctr_enabled & is_dst_ctr_enabled + then update_ctr(TRAP_RETURN, true, true) + else if is_src_ctr_enabled & not(is_dst_ctr_enabled) + then update_ctr(TRAP_RETURN, true, false) +} +/* model implements a 13-bit cycle counter */ +function count_ctr_cycles() -> unit = { + if is_ctr_active(cur_privilege) then { + if unsigned(ctr_cycle_counter) < 8191 + then ctr_cycle_counter = ctr_cycle_counter + 1; + ctr_cycle_counter_valid = true; + } +} diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail index f2980fb9e..6dabd6385 100644 --- a/model/riscv_insts_zicsr.sail +++ b/model/riscv_insts_zicsr.sail @@ -38,8 +38,10 @@ function readCSR csr : csreg -> xlenbits = { (0x305, _) => get_mtvec(), (0x306, _) => zero_extend(mcounteren.bits), (0x30A, _) => menvcfg.bits[sizeof(xlen) - 1 .. 0], + (0x30C, _) => mstateen0.bits[sizeof(xlen) - 1 .. 0], (0x310, 32) => mstatush.bits, (0x31A, 32) => menvcfg.bits[63 .. 32], + (0x31C, 32) => mstateen0.bits[63 .. 32], (0x320, _) => zero_extend(mcountinhibit.bits), (0x340, _) => mscratch, @@ -48,6 +50,16 @@ function readCSR csr : csreg -> xlenbits = { (0x343, _) => mtval, (0x344, _) => mip.bits, + (0x34E, _) => mctrctl.bits[sizeof(xlen) - 1 .. 0], + + (0x350, _) => miselect.bits, + (0x351, _) => get_mireg(), + (0x352, _) => get_mireg2(), + (0x353, _) => get_mireg3(), + (0x355, _) => get_mireg4(), + (0x356, _) => get_mireg5(), + (0x357, _) => get_mireg6(), + // pmpcfgN (0x3A @ idx : bits(4), _) if idx[0] == bitzero | sizeof(xlen) == 32 => pmpReadCfgReg(unsigned(idx)), // pmpaddrN. Unfortunately the PMP index does not nicely align with the CSR index bits. @@ -87,6 +99,16 @@ function readCSR csr : csreg -> xlenbits = { (0x142, _) => scause.bits, (0x143, _) => stval, (0x144, _) => lower_mip(mip, mideleg).bits, + (0x14E, _) => lower_sctrctl(mctrctl).bits[sizeof(xlen) - 1 .. 0], + (0x14F, _) => zero_extend(sctrstatus.bits), + (0x150, _) => siselect.bits(), + (0x151, _) => get_sireg(), + (0x152, _) => get_sireg2(), + (0x153, _) => get_sireg3(), + (0x155, _) => get_sireg4(), + (0x156, _) => get_sireg5(), + (0x157, _) => get_sireg6(), + (0x15F, _) => zero_extend(sctrdepth.bits), (0x180, _) => satp, /* user mode counters */ @@ -125,8 +147,11 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = { (0x306, _) => { mcounteren = legalize_mcounteren(mcounteren, value); Some(zero_extend(mcounteren.bits)) }, (0x30A, 32) => { menvcfg = legalize_menvcfg(menvcfg, menvcfg.bits[63 .. 32] @ value); Some(menvcfg.bits[31 .. 0]) }, (0x30A, 64) => { menvcfg = legalize_menvcfg(menvcfg, value); Some(menvcfg.bits) }, + (0x30C, 32) => { mstateen0 = legalize_mstateen0(mstateen0, mstateen0.bits[63 .. 32] @ value); Some(mstateen0.bits[31 .. 0]) }, + (0x30C, 64) => { mstateen0 = legalize_mstateen0(mstateen0, value); Some(mstateen0.bits) }, (0x310, 32) => { Some(mstatush.bits) }, // ignore writes for now (0x31A, 32) => { menvcfg = legalize_menvcfg(menvcfg, value @ menvcfg.bits[31 .. 0]); Some(menvcfg.bits[63 .. 32]) }, + (0x31C, 32) => { mstateen0 = legalize_mstateen0(mstateen0, value @ mstateen0.bits[31 .. 0]); Some(mstateen0.bits[63 .. 32]) }, (0x320, _) => { mcountinhibit = legalize_mcountinhibit(mcountinhibit, value); Some(zero_extend(mcountinhibit.bits)) }, (0x340, _) => { mscratch = value; Some(mscratch) }, (0x341, _) => { Some(set_xret_target(Machine, value)) }, @@ -134,6 +159,16 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = { (0x343, _) => { mtval = value; Some(mtval) }, (0x344, _) => { mip = legalize_mip(mip, value); Some(mip.bits) }, + (0x34E, _) => { mctrctl = legalize_mctrctl(mctrctl, value); Some(mctrctl.bits[sizeof(xlen) - 1 .. 0]) }, + + (0x350, _) => { miselect = legalize_iselect(miselect, value); Some(miselect.bits) }, + (0x351, _) => { set_mireg(value); Some(get_mireg()) }, + (0x352, _) => { set_mireg2(value); Some(get_mireg2()) }, + (0x353, _) => { set_mireg3(value); Some(get_mireg3()) }, + (0x355, _) => { set_mireg4(value); Some(get_mireg4()) }, + (0x356, _) => { set_mireg5(value); Some(get_mireg5()) }, + (0x357, _) => { set_mireg6(value); Some(get_mireg6()) }, + // pmpcfgN (0x3A @ idx : bits(4), _) if idx[0] == bitzero | sizeof(xlen) == 32 => { let idx = unsigned(idx); @@ -168,6 +203,20 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = { (0x142, _) => { scause.bits = value; Some(scause.bits) }, (0x143, _) => { stval = value; Some(stval) }, (0x144, _) => { mip = legalize_sip(mip, mideleg, value); Some(mip.bits) }, + + (0x14E, _) => { mctrctl = legalize_sctrctl(mctrctl, value); Some(mctrctl.bits[sizeof(xlen) - 1 .. 0]) }, + (0x14F, _) => { sctrstatus = legalize_sctrstatus(sctrstatus, value); Some(zero_extend(sctrstatus.bits)) }, + + (0x150, _) => { siselect = legalize_iselect(siselect, value); Some(siselect.bits) }, + (0x151, _) => { set_sireg(value); Some(get_sireg()) }, + (0x152, _) => { set_sireg2(value); Some(get_sireg2()) }, + (0x153, _) => { set_sireg3(value); Some(get_sireg3()) }, + (0x155, _) => { set_sireg4(value); Some(get_sireg4()) }, + (0x156, _) => { set_sireg5(value); Some(get_sireg5()) }, + (0x157, _) => { set_sireg6(value); Some(get_sireg6()) }, + + (0x15F, _) => { sctrdepth = legalize_sctrdepth(sctrdepth, value); Some(zero_extend(sctrdepth.bits)) }, + (0x180, _) => { satp = legalize_satp(cur_Architecture(), satp, value); Some(satp) }, /* user mode: seed (entropy source). writes are ignored */ diff --git a/model/riscv_jalr_rmem.sail b/model/riscv_jalr_rmem.sail index d628630af..0e7f5352f 100644 --- a/model/riscv_jalr_rmem.sail +++ b/model/riscv_jalr_rmem.sail @@ -8,11 +8,15 @@ /* The definition for the memory model. */ +val update_ctr_jalr : (regidx, regidx) -> unit + function clause execute (RISCV_JALR(imm, rs1, rd)) = { /* FIXME: this does not check for a misaligned target address. See riscv_jalr_seq.sail. */ /* write rd before anything else to prevent unintended strength */ X(rd) = nextPC; /* compatible with JALR, C.JR and C.JALR */ let newPC : xlenbits = X(rs1) + sign_extend(imm); nextPC = [newPC with 0 = bitzero]; /* Clear newPC[0] */ + /* update control transfer record if Ssctr/Smctr is active */ + update_ctr_jalr(rs1, rd); RETIRE_SUCCESS } diff --git a/model/riscv_jalr_seq.sail b/model/riscv_jalr_seq.sail index 497a44178..a99c0a829 100644 --- a/model/riscv_jalr_seq.sail +++ b/model/riscv_jalr_seq.sail @@ -8,6 +8,8 @@ /* The definition for the sequential model. */ +val update_ctr_jalr : (regidx, regidx) -> unit + function clause execute (RISCV_JALR(imm, rs1, rd)) = { /* For the sequential model, the memory-model definition doesn't work directly * if rs1 = rd. We would effectively have to keep a regfile for reads and another for @@ -30,6 +32,8 @@ function clause execute (RISCV_JALR(imm, rs1, rd)) = { } else { X(rd) = get_next_pc(); set_next_pc(target); + /* update control transfer record if Ssctr/Smctr is active */ + update_ctr_jalr(rs1, rd); RETIRE_SUCCESS } } diff --git a/model/riscv_platform.sail b/model/riscv_platform.sail index 19e3d30ae..106ecaa01 100644 --- a/model/riscv_platform.sail +++ b/model/riscv_platform.sail @@ -250,11 +250,15 @@ function clint_store(addr, width, data) = { } } +val count_ctr_cycles : unit -> unit val tick_clock : unit -> unit function tick_clock() = { if mcountinhibit[CY] == 0b0 then mcycle = mcycle + 1; + /* Smctr/Ssctr - update CTR cycles */ + count_ctr_cycles(); + mtime = mtime + 1; clint_dispatch() } diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index 1baa33701..c466ccd7d 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -9,6 +9,8 @@ /* Machine-mode and supervisor-mode functionality. */ +val isSsctrEnabled : (unit) -> bool + /* CSR access control */ function csrAccess(csr : csreg) -> csrRW = csr[11..10] @@ -31,8 +33,10 @@ function is_CSR_defined (csr : csreg, p : Privilege) -> bool = 0x305 => p == Machine, // mtvec 0x306 => p == Machine & haveUsrMode(), // mcounteren 0x30A => p == Machine & haveUsrMode(), // menvcfg + 0x30C => p == Machine & haveSupMode() & haveSmstateen(), // mstateen0 0x310 => p == Machine & (sizeof(xlen) == 32), // mstatush 0x31A => p == Machine & haveUsrMode() & (sizeof(xlen) == 32), // menvcfgh + 0x31C => p == Machine & haveSupMode() & (sizeof(xlen) == 32) & haveSmstateen(), // mstateen0h 0x320 => p == Machine, // mcountinhibit /* machine mode: trap handling */ 0x340 => p == Machine, // mscratch @@ -40,6 +44,16 @@ function is_CSR_defined (csr : csreg, p : Privilege) -> bool = 0x342 => p == Machine, // mcause 0x343 => p == Machine, // mtval 0x344 => p == Machine, // mip + /* machine mode: Machine Control Transfer Records Control Register */ + 0x34E => p == Machine & haveSmctr(), // mctrctl + /* machine mode: indirect register select and alias CSRs */ + 0x350 => p == Machine & haveSmcsrind(), // miselect + 0x351 => p == Machine & haveSmcsrind() & isValidMiselect(), // mireg + 0x352 => p == Machine & haveSmcsrind() & isValidMiselect(), // mireg2 + 0x353 => p == Machine & haveSmcsrind() & isValidMiselect(), // mireg3 + 0x355 => p == Machine & haveSmcsrind() & isValidMiselect(), // mireg4 + 0x356 => p == Machine & haveSmcsrind() & isValidMiselect(), // mireg5 + 0x357 => p == Machine & haveSmcsrind() & isValidMiselect(), // mireg6 // pmpcfgN 0x3A @ idx : bits(4) => p == Machine & sys_pmp_count() > unsigned(idx) & (idx[0] == bitzero | sizeof(xlen) == 32), @@ -74,6 +88,30 @@ function is_CSR_defined (csr : csreg, p : Privilege) -> bool = 0x143 => haveSupMode() & (p == Machine | p == Supervisor), // stval 0x144 => haveSupMode() & (p == Machine | p == Supervisor), // sip + /* supervisor mode: Machine Control Transfer Records Control Register */ + 0x14E => haveSsctr() & (p == Machine | (p == Supervisor & isSsctrEnabled())), // sctrctl + /* supervisor mode: Machine Control Transfer Records Status Register */ + 0x14F => haveSsctr() & (p == Machine | (p == Supervisor & isSsctrEnabled())), // sctrstatus + + /* supervisor mode: indirect register select and alias CSRs */ + 0x150 => haveSupMode() & haveSscsrind() & + (p == Machine | (p == Supervisor & isSscsrindEnabled())), // siselect + 0x151 => haveSupMode() & haveSscsrind() & isValidSiselect() & + (p == Machine | (p == Supervisor & isSscsrindEnabled())), // sireg + 0x152 => haveSupMode() & haveSscsrind() & isValidSiselect() & + (p == Machine | (p == Supervisor & isSscsrindEnabled())), // sireg2 + 0x153 => haveSupMode() & haveSscsrind() & isValidSiselect() & + (p == Machine | (p == Supervisor & isSscsrindEnabled())), // sireg3 + 0x155 => haveSupMode() & haveSscsrind() & isValidSiselect() & + (p == Machine | (p == Supervisor & isSscsrindEnabled())), // sireg4 + 0x156 => haveSupMode() & haveSscsrind() & isValidSiselect() & + (p == Machine | (p == Supervisor & isSscsrindEnabled())), // sireg5 + 0x157 => haveSupMode() & haveSscsrind() & isValidSiselect() & + (p == Machine | (p == Supervisor & isSscsrindEnabled())), // sireg6 + + /* supervisor mode: Machine Control Transfer Records Depth Register */ + 0x15F => haveSsctr() & (p == Machine | (p == Supervisor & isSsctrEnabled())), // sctrdepth + /* supervisor mode: address translation */ 0x180 => haveSupMode() & (p == Machine | p == Supervisor), // satp @@ -314,6 +352,7 @@ function rvfi_trap () = () $endif /* handle exceptional ctl flow by updating nextPC and operating privilege */ +val update_ctr_traps : (bool, Privilege) -> unit function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlenbits, info : option(xlenbits), ext : option(ext_exception)) -> xlenbits = { @@ -325,6 +364,9 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen cancel_reservation(); + /* Update control transfer records when Smctr/Ssctr is implemented */ + update_ctr_traps(intr, del_priv); + match (del_priv) { Machine => { mcause[IsInterrupt] = bool_to_bits(intr); @@ -393,6 +435,7 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen }; } +val update_ctr_trap_return : (Privilege) -> unit function exception_handler(cur_priv : Privilege, ctl : ctl_result, pc: xlenbits) -> xlenbits = { match (cur_priv, ctl) { @@ -418,6 +461,8 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result, then print_platform("ret-ing from " ^ to_str(prev_priv) ^ " to " ^ to_str(cur_privilege)); cancel_reservation(); + /* Update control transfer records when Smctr/Ssctr is implemented */ + update_ctr_trap_return(prev_priv); prepare_xret_target(Machine) & pc_alignment_mask() }, (_, CTL_SRET()) => { @@ -436,6 +481,8 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result, ^ " to " ^ to_str(cur_privilege)); cancel_reservation(); + /* Update control transfer records when Smctr/Ssctr is implemented */ + update_ctr_trap_return(prev_priv); prepare_xret_target(Supervisor) & pc_alignment_mask() }, (_, CTL_URET()) => { @@ -528,6 +575,11 @@ function init_sys() -> unit = { menvcfg.bits = zero_extend(0b0); senvcfg.bits = zero_extend(0b0); + mstateen0.bits = zero_extend(0b0); + + /* Smctr/Ssctr cycle counter */ + ctr_cycle_counter_valid = false; + /* initialize vector csrs */ elen = 0b1; /* ELEN=64 as the common case */ vlen = 0b0100; /* VLEN=512 as a default value */ diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index 6c66492b4..7e3ef443f 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -95,6 +95,10 @@ val sys_enable_next = {c: "sys_enable_next", ocaml: "Platform.enable_next", _: " /* Whether FIOM bit of menvcfg/senvcfg is enabled. It must be enabled if supervisor mode is implemented and non-bare addressing modes are supported. */ val sys_enable_writable_fiom = {c: "sys_enable_writable_fiom", ocaml: "Platform.enable_writable_fiom", _: "sys_enable_writable_fiom"} : unit -> bool +/* whether Ssctr is enabled */ +val sys_enable_ssctr = {c: "sys_enable_ssctr", ocaml: "Platform.enable_ssctr", _: "sys_enable_ssctr"} : unit -> bool +/* whether Smctr is enabled */ +val sys_enable_smctr = {c: "sys_enable_smctr", ocaml: "Platform.enable_smctr", _: "sys_enable_smctr"} : unit -> bool /* How many PMP entries are implemented. This must be 0, 16 or 64 (this is checked at runtime). */ val sys_pmp_count = {c: "sys_pmp_count", ocaml: "Platform.pmp_count", _: "sys_pmp_count"} : unit -> range(0, 64) @@ -164,6 +168,21 @@ function haveZmmul() -> bool = true /* Zicond extension support */ function haveZicond() -> bool = true +/* Smstateen extension support */ +function haveSmstateen() -> bool = true + +/* Sscsrind extension support */ +function haveSscsrind() -> bool = true + +/* Smcsrind extension support */ +function haveSmcsrind() -> bool = true + +/* Smctr extension support - Smctr depends on S-mode, and Smcsrind */ +function haveSmctr() -> bool = haveSupMode() & sys_enable_smctr() & haveSmcsrind() + +/* Ssctr extension support - Ssctr depends on S-mode, Smctr, and Sscsrind */ +function haveSsctr() -> bool = haveSupMode() & sys_enable_ssctr() & haveSmctr() & haveSscsrind() + bitfield Mstatush : bits(32) = { MBE : 5, SBE : 4 @@ -835,6 +854,44 @@ function is_fiom_active() -> bool = { User => (menvcfg[FIOM] | senvcfg[FIOM]) == 0b1, } } + +/* Smstateen */ +bitfield Mstateen0 : bits(64) = { + SE0 : 63, // Controls access to hstateen0/h and sstateen0 + ENVCFG : 62, // Controls access to henvcfg/h and senvcfg + WPRI_1 : 61, + CSRIND : 60, // controls access to the siselect, sireg*, vsiselect, + // and the vsireg* CSRs provided by the Sscsrind extensions + AIA : 59, // Controls access to Ssaia state not + // controlled by CSRIND or IMSIC + IMSIC : 58, // Controls access IMSIC state - including + // stopei and vstopei + CONTEXT : 57, // Controls access to scontext and hcontext + PRIV_V1P13 : 56, // Controls access to hedelegh + WPRI_1 : 55, + CTR : 54, // Controls Ssctr state + WPRI_0 : 53 .. 3, + JVT : 2, // Controls access to the jvt CSR + FCSR : 1, // Controls access to the fcsr + C : 0 // Controls access to any and all custom state +} + +register mstateen0 : Mstateen0 + +function isSscsrindEnabled() -> bool = + match(haveSmstateen(), mstateen0[CSRIND]) { + (false, _) => true, + (true, 0b0) => false, + (true, 0b1) => true + } + +function legalize_mstateen0(o : Mstateen0, v : bits(64)) -> Mstateen0 = { + let v = Mk_Mstateen0(v); + let o = [o with CSRIND = if haveSscsrind() then v[CSRIND] else 0b0]; + // Other extensions are not implemented yet so all other fields are read only zero. + o +} + /* vector csrs */ register vstart : bits(16) /* use the largest possible length of vstart */ register vxsat : bits(1) @@ -919,3 +976,137 @@ function get_vtype_vma() = decode_agtype(vtype[vma]) val get_vtype_vta : unit -> agtype function get_vtype_vta() = decode_agtype(vtype[vta]) + +bitfield SMiselect : xlenbits = { + REG : 11 .. 0 +} + +register siselect : SMiselect +register miselect : SMiselect + +function legalize_iselect(s : SMiselect, v: xlenbits) -> SMiselect = { + let s = Mk_SMiselect(v); + s +} + +val isValidCtrMiselect: unit -> bool +val isValidCtrSiselect: unit -> bool +function isValidMiselect() -> bool = { + /* The behavior upon accessing mireg* from M-mode, + * while miselect holds a value that is not implemented, + * is UNSPECIFIED. It is expected that implementations + * will typically raise an illegal instruction exception + */ + if unsigned(miselect[REG]) >= 512 & unsigned(miselect[REG]) <= 767 + then isValidCtrMiselect() /* 0x200 - 0x2FF is designated for Smctr */ + else false; +} +function isValidSiselect() -> bool = { + /* The behavior upon accessing sireg* from M/S-mode, + * while siselect holds a value that is not implemented, + * is UNSPECIFIED. It is expected that implementations + * will typically raise an illegal instruction exception + */ + if unsigned(siselect[REG]) >= 512 & unsigned(siselect[REG]) <= 767 + then isValidCtrSiselect() /* 0x200 - 0x2FF is designated for Ssctr */ + else false; +} +val get_ctr_mireg : unit -> xlenbits +val get_ctr_mireg2 : unit -> xlenbits +val get_ctr_mireg3 : unit -> xlenbits +val set_ctr_mireg : xlenbits -> unit +val set_ctr_mireg2 : xlenbits -> unit +val set_ctr_mireg3 : xlenbits -> unit +function get_mireg() -> xlenbits = { + if unsigned(miselect[REG]) >= 512 & unsigned(miselect[REG]) <= 767 + then get_ctr_mireg() + else zeros() +} +function get_mireg2() -> xlenbits = { + if unsigned(miselect[REG]) >= 512 & unsigned(miselect[REG]) <= 767 + then get_ctr_mireg2() + else zeros() +} +function get_mireg3() -> xlenbits = { + if unsigned(miselect[REG]) >= 512 & unsigned(miselect[REG]) <= 767 + then get_ctr_mireg3() + else zeros() +} +function get_mireg4() -> xlenbits = { + zeros() +} +function get_mireg5() -> xlenbits = { + zeros() +} +function get_mireg6() -> xlenbits = { + zeros() +} + +function set_mireg(v: xlenbits) -> unit = { + let ctr_idx = miselect.bits[7 .. 0]; + if unsigned(miselect[REG]) >= 512 & unsigned(miselect[REG]) <= 767 + then set_ctr_mireg(v) +} +function set_mireg2(v: xlenbits) -> unit = { + let ctr_idx = miselect.bits[7 .. 0]; + if unsigned(miselect[REG]) >= 512 & unsigned(miselect[REG]) <= 767 + then set_ctr_mireg2(v) +} +function set_mireg3(v: xlenbits) -> unit = { + let ctr_idx = miselect.bits[7 .. 0]; + if unsigned(miselect[REG]) >= 512 & unsigned(miselect[REG]) <= 767 + then set_ctr_mireg3(v) +} +function set_mireg4(v: xlenbits) -> unit = () +function set_mireg5(v: xlenbits) -> unit = () +function set_mireg6(v: xlenbits) -> unit = () + +val get_ctr_sireg : unit -> xlenbits +val get_ctr_sireg2 : unit -> xlenbits +val get_ctr_sireg3 : unit -> xlenbits +val set_ctr_sireg : xlenbits -> unit +val set_ctr_sireg2 : xlenbits -> unit +val set_ctr_sireg3 : xlenbits -> unit +function get_sireg() -> xlenbits = { + if unsigned(siselect[REG]) >= 512 & unsigned(siselect[REG]) <= 767 + then get_ctr_sireg() + else zeros() +} +function get_sireg2() -> xlenbits = { + if unsigned(siselect[REG]) >= 512 & unsigned(siselect[REG]) <= 767 + then get_ctr_sireg2() + else zeros() +} +function get_sireg3() -> xlenbits = { + if unsigned(siselect[REG]) >= 512 & unsigned(siselect[REG]) <= 767 + then get_ctr_sireg3() + else zeros() +} +function get_sireg4() -> xlenbits = { + zeros() +} +function get_sireg5() -> xlenbits = { + zeros() +} +function get_sireg6() -> xlenbits = { + zeros() +} + +function set_sireg(v: xlenbits) -> unit = { + let ctr_idx = siselect.bits[7 .. 0]; + if unsigned(siselect[REG]) >= 512 & unsigned(siselect[REG]) <= 767 + then set_ctr_sireg(v) +} +function set_sireg2(v: xlenbits) -> unit = { + let ctr_idx = siselect.bits[7 .. 0]; + if unsigned(siselect[REG]) >= 512 & unsigned(siselect[REG]) <= 767 + then set_ctr_sireg2(v) +} +function set_sireg3(v: xlenbits) -> unit = { + let ctr_idx = siselect.bits[7 .. 0]; + if unsigned(siselect[REG]) >= 512 & unsigned(siselect[REG]) <= 767 + then set_ctr_sireg3(v) +} +function set_sireg4(v: xlenbits) -> unit = () +function set_sireg5(v: xlenbits) -> unit = () +function set_sireg6(v: xlenbits) -> unit = () diff --git a/ocaml_emulator/platform.ml b/ocaml_emulator/platform.ml index 69f271496..afd491eee 100644 --- a/ocaml_emulator/platform.ml +++ b/ocaml_emulator/platform.ml @@ -12,6 +12,9 @@ let config_enable_misaligned_access = ref false let config_mtval_has_illegal_inst_bits = ref false let config_enable_svinval = ref false let config_enable_zcb = ref false +let config_enable_smctr = ref false +let config_enable_ssctr = ref false +let config_valid_ctr_depth = ref Int.zero let config_enable_writable_fiom = ref true let config_enable_vext = ref true let config_pmp_count = ref Big_int.zero @@ -20,6 +23,8 @@ let config_pmp_grain = ref Big_int.zero let set_config_pmp_count x = config_pmp_count := Big_int.of_int x let set_config_pmp_grain x = config_pmp_grain := Big_int.of_int x +let set_valid_ctr_depth x = config_valid_ctr_depth := x + let platform_arch = ref P.RV64 (* logging *) @@ -92,6 +97,9 @@ let enable_misaligned_access () = !config_enable_misaligned_access let mtval_has_illegal_inst_bits () = !config_mtval_has_illegal_inst_bits let enable_svinval () = !config_enable_svinval let enable_zcb () = !config_enable_zcb +let enable_smctr () = !config_enable_smctr +let enable_ssctr () = !config_enable_ssctr +let valid_ctr_depth () = arch_bits_of_int !config_valid_ctr_depth let enable_zfinx () = false let enable_writable_fiom () = !config_enable_writable_fiom let pmp_count () = !config_pmp_count diff --git a/ocaml_emulator/riscv_ocaml_sim.ml b/ocaml_emulator/riscv_ocaml_sim.ml index 56be8d8a8..d3ff62fc4 100644 --- a/ocaml_emulator/riscv_ocaml_sim.ml +++ b/ocaml_emulator/riscv_ocaml_sim.ml @@ -88,7 +88,16 @@ let options = Arg.align ([("-dump-dts", " requested isa"); ("-with-dtc", Arg.String PI.set_dtc, - " full path to dtc to use") + " full path to dtc to use"); + ("-enable-smctr", + Arg.Set P.config_enable_smctr, + " enable Smctr extension"); + ("-enable-ssctr", + Arg.Set P.config_enable_ssctr, + " enable Ssctr extension"); + ("-valid-ctr-depth", + Arg.Int P.set_valid_ctr_depth, + " valid CTR depths"); ]) let usage_msg = "RISC-V platform options:"