Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Initial introduction of zfinx #75

Merged
merged 16 commits into from
Nov 17, 2021
Merged

Initial introduction of zfinx #75

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
16 commits
Select commit Hold shift + click to select a range
c0bc650
Adds Zfinx enable flag
Oct 26, 2021
8120e35
Hardwire misa.{f,d} and mstats.FS to 0
Oct 26, 2021
5695f97
Moving nan boxing functions to fdext_reg
Oct 26, 2021
aaf1ac2
Swaps register names for floating point instructions
Oct 26, 2021
f57e46d
Disable Floating point loads, stores and moves
Oct 26, 2021
24d0dc3
Add X_or_F_s and X_or_F_d functions, and use them to access all regis…
Oct 26, 2021
4148ed0
Formatting
Oct 27, 2021
8f027c4
Fix inconsistent indentation in insts_dext file
Oct 27, 2021
f53672f
Fix spacing in fdext_regs
Oct 27, 2021
13fd5a8
Remove redundant comparasion with true/ false
Oct 27, 2021
ebbcd78
Constistant tuples spacing and removes couple of unnecessary parens.
Oct 27, 2021
903e24a
Consistent functions declaration & calls spacing and removes couple o…
Oct 27, 2021
430decf
Consistent spacing and removes couple of unnecessary comparasion with…
Oct 27, 2021
b9995b1
Make spacing consistent
Oct 27, 2021
af0d8f0
Remove checks from execution stage
Nov 16, 2021
ee1f224
Add checks to encdec stage
Nov 16, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
3 changes: 3 additions & 0 deletions c_emulator/riscv_platform.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,9 @@ bool sys_enable_next(unit u)
bool sys_enable_fdext(unit u)
{ return rv_enable_fdext; }

bool sys_enable_zfinx(unit u)
{ return rv_enable_zfinx; }

bool sys_enable_writable_misa(unit u)
{ return rv_enable_writable_misa; }

Expand Down
1 change: 1 addition & 0 deletions c_emulator/riscv_platform.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@
bool sys_enable_rvc(unit);
bool sys_enable_next(unit);
bool sys_enable_fdext(unit);
bool sys_enable_zfinx(unit);
bool sys_enable_writable_misa(unit);

bool plat_enable_dirty_update(unit);
Expand Down
1 change: 1 addition & 0 deletions c_emulator/riscv_platform_impl.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@

/* Settings of the platform implementation, with common defaults. */
bool rv_enable_pmp = false;
bool rv_enable_zfinx = false;
bool rv_enable_rvc = true;
bool rv_enable_next = false;
bool rv_enable_writable_misa = true;
Expand Down
1 change: 1 addition & 0 deletions c_emulator/riscv_platform_impl.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@
#define DEFAULT_RSTVEC 0x00001000

extern bool rv_enable_pmp;
extern bool rv_enable_zfinx;
extern bool rv_enable_rvc;
extern bool rv_enable_next;
extern bool rv_enable_fdext;
Expand Down
6 changes: 6 additions & 0 deletions c_emulator/riscv_sim.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -127,6 +127,7 @@ static struct option options[] = {
{"trace", optional_argument, 0, 'v'},
{"no-trace", optional_argument, 0, 'V'},
{"inst-limit", required_argument, 0, 'l'},
{"enable-zfinx", no_argument, 0, 'x'},
#ifdef SAILCOV
{"sailcov-file", required_argument, 0, 'c'},
#endif
Expand Down Expand Up @@ -236,6 +237,7 @@ char *process_args(int argc, char **argv)
"V::"
"v::"
"l:"
"x"
#ifdef SAILCOV
"c:"
#endif
Expand Down Expand Up @@ -325,6 +327,10 @@ char *process_args(int argc, char **argv)
case 'l':
insn_limit = atoi(optarg);
break;
case 'x':
fprintf(stderr, "enabling Zfinx support.\n");
rv_enable_zfinx = true;
break;
#ifdef SAILCOV
case 'c':
sailcov_file = strdup(optarg);
Expand Down
4 changes: 4 additions & 0 deletions handwritten_support/0.11/riscv_extras.lem
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -87,6 +87,10 @@ val sys_enable_fdext : unit -> bool
let sys_enable_fdext () = true
declare ocaml target_rep function sys_enable_fdext = `Platform.enable_fdext`

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

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`
Expand Down
4 changes: 4 additions & 0 deletions handwritten_support/0.11/riscv_extras_sequential.lem
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -75,6 +75,10 @@ val sys_enable_rvc : unit -> bool
let sys_enable_rvc () = true
declare ocaml target_rep function sys_enable_rvc = `Platform.enable_rvc`

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

val sys_enable_next : unit -> bool
let sys_enable_next () = true
declare ocaml target_rep function sys_enable_next = `Platform.enable_next`
Expand Down
4 changes: 4 additions & 0 deletions handwritten_support/riscv_extras.lem
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -155,6 +155,10 @@ val sys_enable_fdext : unit -> bool
let sys_enable_fdext () = true
declare ocaml target_rep function sys_enable_fdext = `Platform.enable_fdext`

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

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`
Expand Down
4 changes: 4 additions & 0 deletions handwritten_support/riscv_extras_sequential.lem
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -143,6 +143,10 @@ val sys_enable_rvc : unit -> bool
let sys_enable_rvc () = true
declare ocaml target_rep function sys_enable_rvc = `Platform.enable_rvc`

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

val sys_enable_next : unit -> bool
let sys_enable_next () = true
declare ocaml target_rep function sys_enable_next = `Platform.enable_next`
Expand Down
99 changes: 96 additions & 3 deletions model/riscv_fdext_regs.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -73,6 +73,41 @@

/* Original version written by Rishiyur S. Nikhil, Sept-Oct 2019 */

/* **************************************************************** */
/* NaN boxing/unboxing. */
/* When 32-bit floats (single-precision) are stored in 64-bit regs */
/* they must be 'NaN boxed' (upper 32b all ones). */
/* When 32-bit floats (single-precision) are read from 64-bit regs */
/* they must be 'NaN unboxed'. */

function canonical_NaN_S() -> bits(32) = 0x_7fc0_0000
function canonical_NaN_D() -> bits(64) = 0x_7ff8_0000_0000_0000

val nan_unbox_do : (bool, bits(64)) -> bits(32)
function nan_unbox_do (zfinx_en, regval) =
if zfinx_en
then regval [31..0]
else if regval [63..32] == 0x_FFFF_FFFF
then regval [31..0]
else canonical_NaN_S()

val nan_unbox_pass : (bool, bits(32)) -> bits(32)
function nan_unbox_pass (zfinx_en, regval) =
regval

val nan_box_do : (bool, bits(32)) -> bits(64)
function nan_box_do (zfinx_en, regval) =
0x_FFFF_FFFF @ regval


val nan_box_pass : (bool, bits(32)) -> bits(32)
function nan_box_pass (zfinx_en, regval) =
regval

overload nan_unbox = { nan_unbox_do, nan_unbox_pass }
overload nan_box = { nan_box_do, nan_box_pass }


/* **************************************************************** */
/* Floating point register file */

Expand Down Expand Up @@ -210,6 +245,58 @@ function wF_bits(i: bits(5), data: flenbits) -> unit = {

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

/* ---- Register Read/ Writes */

val rX_or_F_32 : (bool, bits(5)) -> bits(32) effect {escape, rreg}
function rX_or_F_32(zfinx_en, i) = {
if zfinx_en then
nan_unbox(zfinx_en, rX(unsigned(i)))
else
nan_unbox(zfinx_en, rF(unsigned(i)))
}

val rX_or_F_64 : (bool, bits(5)) -> bits(64) effect {escape, rreg}
function rX_or_F_64(zfinx_en, i) = {
assert (zfinx_en | sizeof(flen) == 64);
if zfinx_en & sizeof (xlen) == 32 then {
assert (i[0] == bitzero);
if i == 0b00000 then
sail_zeros(64)
else rX(unsigned(i+1)) @ rX(unsigned(i))
}
else if zfinx_en & sizeof(xlen) == 64 then
rX(unsigned(i))
else
rF(unsigned(i))
}

val wX_or_F_64 : (bool, bits(5), bits(64)) -> unit effect {escape, wreg}
function wX_or_F_64(zfinx_en: bool, i: bits(5), data: bits(64)) = {
assert (zfinx_en | sizeof(flen) == 64);
if zfinx_en & sizeof(xlen) == 32 then {
assert (i[0] == bitzero);
if i != 0b00000 then {
wX(unsigned(i)) = data[31..0];
wX(unsigned(i+1)) = data[63..32];
}
}
else if zfinx_en & sizeof (xlen) == 64 then
wX(unsigned(i)) = data
else if ~ (zfinx_en) & sizeof (flen) == 64 then
wF(unsigned(i)) = data
}

val wX_or_F_32 : (bool, bits(5), bits(32)) -> unit effect {escape, wreg}
function wX_or_F_32(zfinx_en: bool, i: bits(5), data : bits(32)) = {
if zfinx_en then
wX(unsigned(i)) = nan_box(zfinx_en, data)
else
wF(unsigned(i)) = nan_box(zfinx_en, data)
}

overload X_or_F_S = { rX_or_F_32, wX_or_F_32 }
overload X_or_F_D = { rX_or_F_64, wX_or_F_64 }

/* register names */

val freg_name_abi : regidx <-> string
Expand Down Expand Up @@ -289,6 +376,12 @@ mapping freg_name = {
0b11111 <-> "ft11"
}

val reg_or_freg_name : bits(5) <-> string
mapping reg_or_freg_name = {
reg if sys_enable_zfinx() <-> reg_name(reg) if sys_enable_zfinx(),
reg if ~ (sys_enable_zfinx()) <-> freg_name(reg) if ~ (sys_enable_zfinx())
}

val init_fdext_regs : unit -> unit effect {wreg}
function init_fdext_regs () = {
f0 = zero_freg;
Expand Down Expand Up @@ -344,13 +437,13 @@ function ext_write_fcsr (frm, fflags) = {
fcsr->FRM() = frm; /* Note: frm can be an illegal value, 101, 110, 111 */
fcsr->FFLAGS() = fflags;
update_softfloat_fflags(fflags);
dirty_fd_context();
if ~ (sys_enable_zfinx()) then dirty_fd_context();
}

/* called for softfloat paths (softfloat flags are consistent) */
val write_fflags : (bits(5)) -> unit effect {rreg, wreg}
function write_fflags(fflags) = {
if fcsr.FFLAGS() != fflags
if fcsr.FFLAGS() != fflags & ~ (sys_enable_zfinx())
then dirty_fd_context();
fcsr->FFLAGS() = fflags;
}
Expand All @@ -363,6 +456,6 @@ function accrue_fflags(flags) = {
then {
fcsr->FFLAGS() = f;
update_softfloat_fflags(f);
dirty_fd_context();
if ~ (sys_enable_zfinx()) then dirty_fd_context();
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There are three places here that consider sys_enable_zfinx() before calling dirty_fd_context(); could that qualification be inside dirty_fd_context() instead?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think both are ok, I could go either way on it, though I think I prefer this, since there is no FD context on Zfinx and there should probably be an assert in dirty_fd_context that it's not Zfinx (haven't checked if this patch adds it or not).

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Rename the function to dirty_fd_context_if_exists() then? It's not great to keep repeating the conditional like this. Whether those bits exist or not should be defined in exactly one place.

}
}
16 changes: 8 additions & 8 deletions model/riscv_insts_cdext.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -77,9 +77,9 @@
union clause ast = C_FLDSP : (bits(6), regidx)

mapping clause encdec_compressed = C_FLDSP(ui86 @ ui5 @ ui43, rd)
if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt()
if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt() & ~ (sys_enable_zfinx())
<-> 0b001 @ ui5 : bits(1) @ rd : regidx @ ui43 : bits(2) @ ui86 : bits(3) @ 0b10
if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt()
if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt() & ~ (sys_enable_zfinx())

function clause execute (C_FLDSP(uimm, rd)) = {
let imm : bits(12) = EXTZ(uimm @ 0b000);
Expand All @@ -95,9 +95,9 @@ mapping clause assembly = C_FLDSP(uimm, rd)
union clause ast = C_FSDSP : (bits(6), regidx)

mapping clause encdec_compressed = C_FSDSP(ui86 @ ui53, rs2)
if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt()
if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt() & ~ (sys_enable_zfinx())
<-> 0b101 @ ui53 : bits(3) @ ui86 : bits(3) @ rs2 : regidx @ 0b10
if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt()
if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt() & ~ (sys_enable_zfinx())

function clause execute (C_FSDSP(uimm, rs2)) = {
let imm : bits(12) = EXTZ(uimm @ 0b000);
Expand All @@ -113,9 +113,9 @@ mapping clause assembly = C_FSDSP(uimm, rs2)
union clause ast = C_FLD : (bits(5), cregidx, cregidx)

mapping clause encdec_compressed = C_FLD(ui76 @ ui53, rs1, rd)
if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt()
if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt() & ~ (sys_enable_zfinx())
<-> 0b001 @ ui53 : bits(3) @ rs1 : cregidx @ ui76 : bits(2) @ rd : cregidx @ 0b00
if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt()
if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt() & ~ (sys_enable_zfinx())

function clause execute (C_FLD(uimm, rsc, rdc)) = {
let imm : bits(12) = EXTZ(uimm @ 0b000);
Expand All @@ -133,9 +133,9 @@ mapping clause assembly = C_FLD(uimm, rsc, rdc)
union clause ast = C_FSD : (bits(5), cregidx, cregidx)

mapping clause encdec_compressed = C_FSD(ui76 @ ui53, rs1, rs2)
if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt()
if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt() & ~ (sys_enable_zfinx())
<-> 0b101 @ ui53 : bits(3) @ rs1 : bits(3) @ ui76 : bits(2) @ rs2 : bits(3) @ 0b00
if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt()
if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt() & ~ (sys_enable_zfinx())

function clause execute (C_FSD(uimm, rsc1, rsc2)) = {
let imm : bits(12) = EXTZ(uimm @ 0b000);
Expand Down
16 changes: 8 additions & 8 deletions model/riscv_insts_cfext.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -77,9 +77,9 @@
union clause ast = C_FLWSP : (bits(6), regidx)

mapping clause encdec_compressed = C_FLWSP(ui76 @ ui5 @ ui42, rd)
if sizeof(xlen) == 32 & haveRVC() & haveFExt()
if sizeof(xlen) == 32 & haveRVC() & haveFExt() & ~ (sys_enable_zfinx())
<-> 0b011 @ ui5 : bits(1) @ rd : regidx @ ui42 : bits(3) @ ui76 : bits(2) @ 0b10
if sizeof(xlen) == 32 & haveRVC() & haveFExt()
if sizeof(xlen) == 32 & haveRVC() & haveFExt() & ~ (sys_enable_zfinx())

function clause execute (C_FLWSP(imm, rd)) = {
let imm : bits(12) = EXTZ(imm @ 0b00);
Expand All @@ -95,9 +95,9 @@ mapping clause assembly = C_FLWSP(imm, rd)
union clause ast = C_FSWSP : (bits(6), regidx)

mapping clause encdec_compressed = C_FSWSP(ui76 @ ui52, rs2)
if sizeof(xlen) == 32 & haveRVC() & haveFExt()
if sizeof(xlen) == 32 & haveRVC() & haveFExt() & ~ (sys_enable_zfinx())
<-> 0b111 @ ui52 : bits(4) @ ui76 : bits(2) @ rs2 : regidx @ 0b10
if sizeof(xlen) == 32 & haveRVC() & haveFExt()
if sizeof(xlen) == 32 & haveRVC() & haveFExt() & ~ (sys_enable_zfinx())

function clause execute (C_FSWSP(uimm, rs2)) = {
let imm : bits(12) = EXTZ(uimm @ 0b00);
Expand All @@ -113,9 +113,9 @@ mapping clause assembly = C_FSWSP(uimm, rd)
union clause ast = C_FLW : (bits(5), cregidx, cregidx)

mapping clause encdec_compressed = C_FLW(ui6 @ ui53 @ ui2, rs1, rd)
if sizeof(xlen) == 32 & haveRVC() & haveFExt()
if sizeof(xlen) == 32 & haveRVC() & haveFExt() & ~ (sys_enable_zfinx())
<-> 0b011 @ ui53 : bits(3) @ rs1 : cregidx @ ui2 : bits(1) @ ui6 : bits(1) @ rd : cregidx @ 0b00
if sizeof(xlen) == 32 & haveRVC() & haveFExt()
if sizeof(xlen) == 32 & haveRVC() & haveFExt() & ~ (sys_enable_zfinx())

function clause execute (C_FLW(uimm, rsc, rdc)) = {
let imm : bits(12) = EXTZ(uimm @ 0b00);
Expand All @@ -133,9 +133,9 @@ mapping clause assembly = C_FLW(uimm, rsc, rdc)
union clause ast = C_FSW : (bits(5), cregidx, cregidx)

mapping clause encdec_compressed = C_FSW(ui6 @ ui53 @ ui2, rs1, rs2)
if sizeof(xlen) == 32 & haveRVC() & haveFExt()
if sizeof(xlen) == 32 & haveRVC() & haveFExt() & ~ (sys_enable_zfinx())
<-> 0b111 @ ui53 : bits(3) @ rs1 : cregidx @ ui2 : bits(1) @ ui6 : bits(1) @ rs2 : cregidx @ 0b00
if sizeof(xlen) == 32 & haveRVC() & haveFExt()
if sizeof(xlen) == 32 & haveRVC() & haveFExt() & ~ (sys_enable_zfinx())

function clause execute (C_FSW(uimm, rsc1, rsc2)) = {
let imm : bits(12) = EXTZ(uimm @ 0b00);
Expand Down