Skip to content

Commit

Permalink
Update register reads/writes to use range and type aliases instead of…
Browse files Browse the repository at this point in the history 
… forall 'n

Replace forall 'n, 0 < 'n <= * with range(0, *) for register access. With this change, many of them can also switch to using the already defined type aliases.

Fixes riscv#426
  • Loading branch information
@jordancarlin
jordancarlin authored Jul 4, 2024
1 parent 0b8935e commit eeb9270
Show file tree
Hide file tree
Showing 4 changed files with 33 additions and 42 deletions.
38 changes: 18 additions & 20 deletions model/riscv_fdext_regs.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -112,8 +112,7 @@ function dirty_fd_context_if_present() -> unit = {
if sys_enable_fdext() then dirty_fd_context()
}

val rF : forall 'n, 0 <= 'n < 32. regno('n) -> flenbits
function rF r = {
function rF (r : regno) -> flenbits = {
assert(sys_enable_fdext());
let v : fregtype =
match r {
Expand Down Expand Up @@ -154,8 +153,7 @@ function rF r = {
fregval_from_freg(v)
}

val wF : forall 'n, 0 <= 'n < 32. (regno('n), flenbits) -> unit
function wF (r, in_v) = {
function wF (r : regno, in_v : flenbits) -> unit = {
assert(sys_enable_fdext());
let v = fregval_into_freg(in_v);
match r {
Expand Down Expand Up @@ -202,50 +200,50 @@ function wF (r, in_v) = {
print_reg("f" ^ dec_str(r) ^ " <- " ^ FRegStr(v));
}

function rF_bits(i: bits(5)) -> flenbits = rF(unsigned(i))
function rF_bits(i: regidx) -> flenbits = rF(unsigned(i))

function wF_bits(i: bits(5), data: flenbits) -> unit = {
function wF_bits(i: regidx, data: flenbits) -> unit = {
wF(unsigned(i)) = data
}

overload F = {rF_bits, wF_bits, rF, wF}

val rF_H : bits(5) -> bits(16)
val rF_H : regidx -> bits(16)
function rF_H(i) = {
assert(sizeof(flen) >= 16);
assert(sys_enable_fdext() & not(sys_enable_zfinx()));
nan_unbox(F(i))
}

val wF_H : (bits(5), bits(16)) -> unit
val wF_H : (regidx, bits(16)) -> unit
function wF_H(i, data) = {
assert(sizeof(flen) >= 16);
assert(sys_enable_fdext() & not(sys_enable_zfinx()));
F(i) = nan_box(data)
}

val rF_S : bits(5) -> bits(32)
val rF_S : regidx -> bits(32)
function rF_S(i) = {
assert(sizeof(flen) >= 32);
assert(sys_enable_fdext() & not(sys_enable_zfinx()));
nan_unbox(F(i))
}

val wF_S : (bits(5), bits(32)) -> unit
val wF_S : (regidx, bits(32)) -> unit
function wF_S(i, data) = {
assert(sizeof(flen) >= 32);
assert(sys_enable_fdext() & not(sys_enable_zfinx()));
F(i) = nan_box(data)
}

val rF_D : bits(5) -> bits(64)
val rF_D : regidx -> bits(64)
function rF_D(i) = {
assert(sizeof(flen) >= 64);
assert(sys_enable_fdext() & not(sys_enable_zfinx()));
F(i)
}

val wF_D : (bits(5), bits(64)) -> unit
val wF_D : (regidx, bits(64)) -> unit
function wF_D(i, data) = {
assert(sizeof(flen) >= 64);
assert(sys_enable_fdext() & not(sys_enable_zfinx()));
Expand All @@ -256,7 +254,7 @@ overload F_H = { rF_H, wF_H }
overload F_S = { rF_S, wF_S }
overload F_D = { rF_D, wF_D }

val rF_or_X_H : bits(5) -> bits(16)
val rF_or_X_H : regidx -> bits(16)
function rF_or_X_H(i) = {
assert(sizeof(flen) >= 16);
assert(sys_enable_fdext() != sys_enable_zfinx());
Expand All @@ -265,7 +263,7 @@ function rF_or_X_H(i) = {
else X(i)[15..0]
}

val rF_or_X_S : bits(5) -> bits(32)
val rF_or_X_S : regidx -> bits(32)
function rF_or_X_S(i) = {
assert(sizeof(flen) >= 32);
assert(sys_enable_fdext() != sys_enable_zfinx());
Expand All @@ -274,7 +272,7 @@ function rF_or_X_S(i) = {
else X(i)[31..0]
}

val rF_or_X_D : bits(5) -> bits(64)
val rF_or_X_D : regidx -> bits(64)
function rF_or_X_D(i) = {
assert(sizeof(flen) >= 64);
assert(sys_enable_fdext() != sys_enable_zfinx());
Expand All @@ -288,7 +286,7 @@ function rF_or_X_D(i) = {
}
}

val wF_or_X_H : (bits(5), bits(16)) -> unit
val wF_or_X_H : (regidx, bits(16)) -> unit
function wF_or_X_H(i, data) = {
assert(sizeof(flen) >= 16);
assert(sys_enable_fdext() != sys_enable_zfinx());
Expand All @@ -297,7 +295,7 @@ function wF_or_X_H(i, data) = {
else X(i) = sign_extend(data)
}

val wF_or_X_S : (bits(5), bits(32)) -> unit
val wF_or_X_S : (regidx, bits(32)) -> unit
function wF_or_X_S(i, data) = {
assert(sizeof(flen) >= 32);
assert(sys_enable_fdext() != sys_enable_zfinx());
Expand All @@ -306,7 +304,7 @@ function wF_or_X_S(i, data) = {
else X(i) = sign_extend(data)
}

val wF_or_X_D : (bits(5), bits(64)) -> unit
val wF_or_X_D : (regidx, bits(64)) -> unit
function wF_or_X_D(i, data) = {
assert (sizeof(flen) >= 64);
assert(sys_enable_fdext() != sys_enable_zfinx());
Expand All @@ -329,7 +327,7 @@ overload F_or_X_D = { rF_or_X_D, wF_or_X_D }

/* mappings for assembly */

val freg_name : bits(5) <-> string
val freg_name : regidx <-> string
mapping freg_name = {
0b00000 <-> "ft0",
0b00001 <-> "ft1",
Expand Down Expand Up @@ -365,7 +363,7 @@ mapping freg_name = {
0b11111 <-> "ft11"
}

val freg_or_reg_name : bits(5) <-> string
val freg_or_reg_name : regidx <-> string
mapping freg_or_reg_name = {
reg if sys_enable_fdext() <-> freg_name(reg) if sys_enable_fdext(),
reg if sys_enable_zfinx() <-> reg_name(reg) if sys_enable_zfinx()
Expand Down
20 changes: 8 additions & 12 deletions model/riscv_regs.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -48,8 +48,7 @@ register x29 : regtype
register x30 : regtype
register x31 : regtype

val rX : forall 'n, 0 <= 'n < 32. regno('n) -> xlenbits
function rX r = {
function rX (r : regno) -> xlenbits = {
let v : regtype =
match r {
0 => zero_reg,
Expand Down Expand Up @@ -90,19 +89,16 @@ function rX r = {
}

$ifdef RVFI_DII
val rvfi_wX : forall 'n, 0 <= 'n < 32. (regno('n), xlenbits) -> unit
function rvfi_wX (r,v) = {
function rvfi_wX (r : regno, v : xlenbits) -> unit = {
rvfi_int_data[rvfi_rd_wdata] = zero_extend(v);
rvfi_int_data[rvfi_rd_addr] = to_bits(8,r);
rvfi_int_data_present = true;
}
$else
val rvfi_wX : forall 'n, 0 <= 'n < 32. (regno('n), xlenbits) -> unit
function rvfi_wX (r,v) = ()
function rvfi_wX (r : regno, v : xlenbits) -> unit = ()
$endif

val wX : forall 'n, 0 <= 'n < 32. (regno('n), xlenbits) -> unit
function wX (r, in_v) = {
function wX (r : regno, in_v : xlenbits) -> unit = {
let v = regval_into_reg(in_v);
match r {
0 => (),
Expand Down Expand Up @@ -146,17 +142,17 @@ function wX (r, in_v) = {
}
}

function rX_bits(i: bits(5)) -> xlenbits = rX(unsigned(i))
function rX_bits(i: regidx) -> xlenbits = rX(unsigned(i))

function wX_bits(i: bits(5), data: xlenbits) -> unit = {
function wX_bits(i: regidx, data: xlenbits) -> unit = {
wX(unsigned(i)) = data
}

overload X = {rX_bits, wX_bits, rX, wX}

/* mappings for assembly */

val reg_name : bits(5) <-> string
val reg_name : regidx <-> string
mapping reg_name = {
0b00000 <-> "zero",
0b00001 <-> "ra",
Expand Down Expand Up @@ -192,7 +188,7 @@ mapping reg_name = {
0b11111 <-> "t6"
}

mapping creg_name : bits(3) <-> string = {
mapping creg_name : cregidx <-> string = {
0b000 <-> "s0",
0b001 <-> "s1",
0b010 <-> "a0",
Expand Down
5 changes: 2 additions & 3 deletions model/riscv_types.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -28,10 +28,9 @@ type csreg = bits(12) /* CSR addressing */

/* register file indexing */

type regno ('n : Int), 0 <= 'n < 32 = int('n)
type regno = range(0, 31)

val regidx_to_regno : bits(5) -> {'n, 0 <= 'n < 32. regno('n)}
function regidx_to_regno b = let 'r = unsigned(b) in r
function regidx_to_regno (b : regidx) -> regno = unsigned(b)

/* mapping RVC register indices into normal indices */
val creg2reg_idx : cregidx -> regidx
Expand Down
12 changes: 5 additions & 7 deletions model/riscv_vext_regs.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,7 @@ register vr29 : vregtype
register vr30 : vregtype
register vr31 : vregtype

val vreg_name : bits(5) <-> string
val vreg_name : regidx <-> string
mapping vreg_name = {
0b00000 <-> "v0",
0b00001 <-> "v1",
Expand Down Expand Up @@ -86,8 +86,7 @@ function dirty_v_context_if_present() -> unit = {
if sys_enable_vext() then dirty_v_context()
}

val rV : forall 'n, 0 <= 'n < 32. regno('n) -> vregtype
function rV r = {
function rV (r : regno) -> vregtype = {
let zero_vreg : vregtype = zeros();
let v : vregtype =
match r {
Expand Down Expand Up @@ -128,8 +127,7 @@ function rV r = {
v
}

val wV : forall 'n, 0 <= 'n < 32. (regno('n), vregtype) -> unit
function wV (r, in_v) = {
function wV (r : regno, in_v : vregtype) -> unit = {
let v = in_v;
match r {
0 => vr0 = v,
Expand Down Expand Up @@ -175,9 +173,9 @@ function wV (r, in_v) = {
then print_reg("v" ^ dec_str(r) ^ " <- " ^ BitStr(v[VLEN - 1 .. 0]));
}

function rV_bits(i: bits(5)) -> vregtype = rV(unsigned(i))
function rV_bits(i: regidx) -> vregtype = rV(unsigned(i))

function wV_bits(i: bits(5), data: vregtype) -> unit = {
function wV_bits(i: regidx, data: vregtype) -> unit = {
wV(unsigned(i)) = data
}

Expand Down

0 comments on commit eeb9270

Please sign in to comment.