Skip to content

Commit

Permalink
riscv_ctr_regs.sail
Browse files Browse the repository at this point in the history
  • Loading branch information
ved-rivos committed May 30, 2024
1 parent 64e50ea commit 58c914e
Show file tree
Hide file tree
Showing 11 changed files with 25 additions and 47 deletions.
4 changes: 0 additions & 4 deletions c_emulator/riscv_platform.c
Original file line number Diff line number Diff line change
Expand Up @@ -75,10 +75,6 @@ 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;
Expand Down
1 change: 0 additions & 1 deletion c_emulator/riscv_platform.h
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,6 @@ 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);
Expand Down
1 change: 0 additions & 1 deletion c_emulator/riscv_platform_impl.c
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,6 @@ 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;
Expand Down
1 change: 0 additions & 1 deletion c_emulator/riscv_platform_impl.h
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,6 @@ 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;
Expand Down
12 changes: 5 additions & 7 deletions c_emulator/riscv_sim.c
Original file line number Diff line number Diff line change
Expand Up @@ -55,8 +55,7 @@ const char *RV32ISA = "RV32IMAC";
#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_VALID_CTR_DEPTH 1006
#define OPT_ENABLE_ZCB 10014

static bool do_dump_dts = false;
Expand Down Expand Up @@ -154,7 +153,6 @@ static struct option options[] = {
{"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
Expand Down Expand Up @@ -406,15 +404,15 @@ static int process_args(int argc, char **argv)
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");
fprintf(stderr,
"CTR depth should be specified as a bitmap where \n"
"bit position i being 1 indicates CTR depth of \n"
"2^(i+4) is valid and implemented\n");
exit(1);
}
break;
Expand Down
7 changes: 2 additions & 5 deletions model/riscv_ctr_regs.sail
Original file line number Diff line number Diff line change
Expand Up @@ -96,6 +96,7 @@ register ctr_cycle_counter_valid : bool

function legalize_mctrctl(o : Mctrctl, v : xlenbits) -> Mctrctl = {
let m : Mctrctl = Mk_Mctrctl(zero_extend(v));
let m = [m with LCOFIFRZ = if haveSmcofpmf() then m[LCOFIFRZ] else 0b0];
m
}

Expand Down Expand Up @@ -153,13 +154,9 @@ function number_of_ctr() -> int = {
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())
haveSmctr() & (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)
Expand Down
18 changes: 6 additions & 12 deletions model/riscv_insts_ctr.sail
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ mapping clause encdec = SCTRCLR()
function clause execute SCTRCLR() = {
let sctrclr_illegal : bool = match cur_privilege {
User => true,
Supervisor => not(haveSsctr()) | mstateen0[CTR] == 0b0,
Supervisor => not(haveSmctr()) | mstateen0[CTR] == 0b0,
Machine => not(haveSmctr())
};
if sctrclr_illegal
Expand Down Expand Up @@ -74,18 +74,11 @@ mapping encdec_ctr_xfer_type : ctr_xfer_type <-> bits(4) = {
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
User => mctrctl[U] == 0b1 & sctrstatus[FROZEN] == 0b0,
Supervisor => mctrctl[S] == 0b1 & sctrstatus[FROZEN] == 0b0,
Machine => mctrctl[M] == 0b1 & sctrstatus[FROZEN] == 0b0
}


Expand Down Expand Up @@ -114,7 +107,8 @@ function update_ctr(transfer_type : ctr_xfer_type, src_recorded : bool, dst_reco
OTHER_DIRECT_JUMP_WITH_LINKAGE => mctrctl[DIRLJMPINH] == 0b0 & not(ras_emu),
};

/* In RAS emulation, function returns pop but coroutine swaps pop and then push */
/* In RAS emulation, function returns only pop */
/* In RAS emulation, 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];
Expand Down
9 changes: 4 additions & 5 deletions model/riscv_sys_control.sail
Original file line number Diff line number Diff line change
Expand Up @@ -9,8 +9,6 @@
/* Machine-mode and supervisor-mode functionality. */


val isSsctrEnabled : (unit) -> bool

/* CSR access control */

function csrAccess(csr : csreg) -> csrRW = csr[11..10]
Expand Down Expand Up @@ -89,9 +87,9 @@ function is_CSR_defined (csr : csreg, p : Privilege) -> bool =
0x144 => haveSupMode() & (p == Machine | p == Supervisor), // sip

/* supervisor mode: Machine Control Transfer Records Control Register */
0x14E => haveSsctr() & (p == Machine | (p == Supervisor & isSsctrEnabled())), // sctrctl
0x14E => haveSmctr() & (p == Machine | (p == Supervisor & mstateen0[CTR] == 0b1)), // sctrctl
/* supervisor mode: Machine Control Transfer Records Status Register */
0x14F => haveSsctr() & (p == Machine | (p == Supervisor & isSsctrEnabled())), // sctrstatus
0x14F => haveSmctr() & (p == Machine | (p == Supervisor & mstateen0[CTR] == 0b1)), // sctrstatus

/* supervisor mode: indirect register select and alias CSRs */
0x150 => haveSupMode() & haveSscsrind() &
Expand All @@ -110,7 +108,7 @@ function is_CSR_defined (csr : csreg, p : Privilege) -> bool =
(p == Machine | (p == Supervisor & isSscsrindEnabled())), // sireg6

/* supervisor mode: Machine Control Transfer Records Depth Register */
0x15F => haveSsctr() & (p == Machine | (p == Supervisor & isSsctrEnabled())), // sctrdepth
0x15F => haveSmctr() & (p == Machine | (p == Supervisor & mstateen0[CTR] == 0b1)), // sctrdepth

/* supervisor mode: address translation */
0x180 => haveSupMode() & (p == Machine | p == Supervisor), // satp
Expand Down Expand Up @@ -576,6 +574,7 @@ function init_sys() -> unit = {
menvcfg.bits = zero_extend(0b0);
senvcfg.bits = zero_extend(0b0);
mstateen0.bits = zero_extend(0b0);
mctrctl.bits = zero_extend(0b0);

/* Smctr/Ssctr cycle counter */
ctr_cycle_counter_valid = false;
Expand Down
14 changes: 8 additions & 6 deletions model/riscv_sys_regs.sail
Original file line number Diff line number Diff line change
Expand Up @@ -177,11 +177,14 @@ 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()
/* Smctr extension support - Smctr depends on S-mode, and Sscsrind */
function haveSmctr() -> bool = haveSupMode() & sys_enable_smctr() & haveSscsrind()

/* Ssctr extension support - Ssctr depends on S-mode, Smctr, and Sscsrind */
function haveSsctr() -> bool = haveSupMode() & sys_enable_ssctr() & haveSmctr() & haveSscsrind()
function haveSsctr() -> bool = haveSupMode() & haveSmctr() & haveSscsrind()

/* Smcofpmf extension support */
function haveSmcofpmf() -> bool = false

bitfield Mstatush : bits(32) = {
MBE : 5,
Expand Down Expand Up @@ -997,10 +1000,9 @@ function isValidMiselect() -> bool = {
* 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;
false
}

function isValidSiselect() -> bool = {
/* The behavior upon accessing sireg* from M/S-mode,
* while siselect holds a value that is not implemented,
Expand Down
2 changes: 0 additions & 2 deletions ocaml_emulator/platform.ml
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,6 @@ 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
Expand Down Expand Up @@ -98,7 +97,6 @@ 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
Expand Down
3 changes: 0 additions & 3 deletions ocaml_emulator/riscv_ocaml_sim.ml
Original file line number Diff line number Diff line change
Expand Up @@ -92,9 +92,6 @@ let options = Arg.align ([("-dump-dts",
("-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");
Expand Down

0 comments on commit 58c914e

Please sign in to comment.