Skip to content

Big endianness Support added #751

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.

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

Open
wants to merge 20 commits into
base: master
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
20 commits
Select commit Hold shift + click to select a range
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -126,6 +126,7 @@ Supported RISC-V ISA features
- Svinval extension for fine-grained address-translation cache invalidation, v1.0
- Sv32, Sv39, Sv48 and Sv57 page-based virtual-memory systems
- Physical Memory Protection (PMP)
- Endianness control

<!-- Uncomment the following section when unratified extensions are added
The following unratified extensions are supported and can be enabled using the `--enable-experimental-extensions` flag:
Expand Down
5 changes: 5 additions & 0 deletions model/prelude.sail
Original file line number Diff line number Diff line change
Expand Up @@ -239,5 +239,10 @@ type max_mem_access : Int = 4096
// Type used for memory access widths. Zero byte accesses are not allowed.
type mem_access_width = range(1, max_mem_access)

// Function to reverse endianness.
// Currently, not able to import reverse_endianness.sail library because of type compatibility issue.
val reverse_endianness = pure {c: "reverse_endianness"} : forall 'n . bits(8 * 'n) -> bits(8 * 'n)

// Enable unratified extensions
val sys_enable_experimental_extensions = pure "sys_enable_experimental_extensions" : unit -> bool

25 changes: 19 additions & 6 deletions model/riscv_mem.sail
Original file line number Diff line number Diff line change
Expand Up @@ -63,8 +63,17 @@ function write_kind_of_flags (aq : bool, rl : bool, con : bool) -> write_kind =
(true, false, true) => throw(Error_not_implemented("sc.aq"))
}

function get_endianness(typ : AccessType(ext_access_type)) -> Endianness = {
match (typ, effectivePrivilege(typ, mstatus, cur_privilege)) {
(Execute(), _) => LittleEndian,
(_, Machine) => if bits_to_bool(mstatus[MBE]) then BigEndian else LittleEndian,
(_, Supervisor) => if bits_to_bool(mstatus[SBE]) then BigEndian else LittleEndian,
(_, User) => if bits_to_bool(mstatus[UBE]) then BigEndian else LittleEndian,
}
}

// only used for actual memory regions, to avoid MMIO effects
function phys_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_access_type), paddr : physaddr, width : int('n), aq : bool, rl: bool, res : bool, meta : bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) = {
function phys_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_access_type), paddr : physaddr, width : int('n), aq : bool, rl: bool, res : bool, meta : bool, current_endianness: Endianness) -> MemoryOpResult((bits(8 * 'n), mem_meta)) = {
let result = (match read_kind_of_flags(aq, rl, res) {
Some(rk) => Some(read_ram(rk, paddr, width, meta)),
None() => None()
Expand All @@ -73,9 +82,12 @@ function phys_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext
(Execute(), None()) => Err(E_Fetch_Access_Fault()),
(Read(Data), None()) => Err(E_Load_Access_Fault()),
(_, None()) => Err(E_SAMO_Access_Fault()),
(_, Some(v, m)) => { if get_config_print_mem()
then print_mem("mem[" ^ to_str(t) ^ "," ^ BitStr(physaddr_bits(paddr)) ^ "] -> " ^ BitStr(v));
Ok(v, m) }
(_, Some(v, m)) => {
let v = endianness_conversion(v, current_endianness);
if get_config_print_mem()
then print_mem("mem[" ^ to_str(t) ^ "," ^ BitStr(physaddr_bits(paddr)) ^ "] -> " ^ BitStr(v));
Ok(v, m)
},
}
}

Expand All @@ -102,10 +114,10 @@ function checked_mem_read forall 'n, 0 < 'n <= max_mem_access . (
Some(e) => Err(e),
None() => {
if within_mmio_readable(paddr, width)
then MemoryOpResult_add_meta(mmio_read(t, paddr, width), default_meta)
then MemoryOpResult_add_meta(mmio_read(t, paddr, width, get_endianness(t)), default_meta)
else if within_phys_mem(paddr, width)
then match ext_check_phys_mem_read(t, paddr, width, aq, rl, res, meta) {
Ext_PhysAddr_OK() => phys_mem_read(t, paddr, width, aq, rl, res, meta),
Ext_PhysAddr_OK() => phys_mem_read(t, paddr, width, aq, rl, res, meta, get_endianness(t)),
Ext_PhysAddr_Error(e) => Err(e)
} else match t {
Execute() => Err(E_Fetch_Access_Fault()),
Expand Down Expand Up @@ -217,6 +229,7 @@ function checked_mem_write forall 'n, 0 < 'n <= max_mem_access . (
match phys_access_check(typ, priv, paddr, width) {
Some(e) => Err(e),
None() => {
let data = endianness_conversion(data, get_endianness(typ));
if within_mmio_writable(paddr, width)
then mmio_write(paddr, width, data)
else if within_phys_mem(paddr, width)
Expand Down
67 changes: 43 additions & 24 deletions model/riscv_platform.sail
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,12 @@ val elf_entry = pure {
c: "elf_entry"
} : unit -> int

function endianness_conversion forall 'n, 0 < 'n <= max_mem_access . (data : bits(8 * 'n), current_endianness: Endianness) -> bits(8 * 'n) =
match current_endianness {
LittleEndian => data,
BigEndian => reverse_endianness(data),
}

// Cache block size is 2^cache_block_size_exp. Max is `max_mem_access` (4096)
// because this model performs `cbo.zero` with a single write, and the behaviour
// with cache blocks larger than a page is not clearly defined.
Expand Down Expand Up @@ -137,8 +143,17 @@ let MTIMECMP_BASE_HI : physaddrbits = zero_extend(0x04004)
let MTIME_BASE : physaddrbits = zero_extend(0x0bff8)
let MTIME_BASE_HI : physaddrbits = zero_extend(0x0bffc)

val clint_load : forall 'n, 'n > 0. (AccessType(ext_access_type), physaddr, int('n)) -> MemoryOpResult(bits(8 * 'n))
function clint_load(t, Physaddr(addr), width) = {
val clint_load : forall 'n, 'n > 0. (AccessType(ext_access_type), physaddr, int('n), Endianness) -> MemoryOpResult(bits(8 * 'n))
function clint_load(t, Physaddr(addr), width, current_endianness) = {
//these two registers are 64 bits, so simple conversion is not accurate.
//consider 0x78563412 stored at mtime/cmp and when reading in big endian format,
//we change it to 0x1234567800000000. So position for mtime and mtime_hi are reversed. (not for ld)
var converted_mtime = endianness_conversion(mtime, current_endianness);
var converted_mtimecmp = endianness_conversion(mtimecmp, current_endianness);
if ((current_endianness == BigEndian) & 'n == 4) then {
converted_mtime = converted_mtime[31..0] @ converted_mtime[63..32];
converted_mtimecmp = converted_mtimecmp[31..0] @ converted_mtimecmp[63..32];
};
let addr = addr - plat_clint_base ();
/* FIXME: For now, only allow exact aligned access. */
if addr == MSIP_BASE & ('n == 8 | 'n == 4)
Expand All @@ -150,41 +165,41 @@ function clint_load(t, Physaddr(addr), width) = {
else if addr == MTIMECMP_BASE & ('n == 4)
then {
if get_config_print_platform()
then print_platform("clint<4>[" ^ BitStr(addr) ^ "] -> " ^ BitStr(mtimecmp[31..0]));
then print_platform("clint<4>[" ^ BitStr(addr) ^ "] -> " ^ BitStr(converted_mtimecmp[31..0]));
/* FIXME: Redundant zero_extend currently required by Lem backend */
Ok(zero_extend(32, mtimecmp[31..0]))
Ok(zero_extend(32, converted_mtimecmp[31..0]))
}
else if addr == MTIMECMP_BASE & ('n == 8)
then {
if get_config_print_platform()
then print_platform("clint<8>[" ^ BitStr(addr) ^ "] -> " ^ BitStr(mtimecmp));
then print_platform("clint<8>[" ^ BitStr(addr) ^ "] -> " ^ BitStr(converted_mtimecmp));
/* FIXME: Redundant zero_extend currently required by Lem backend */
Ok(zero_extend(64, mtimecmp))
Ok(zero_extend(64, converted_mtimecmp))
}
else if addr == MTIMECMP_BASE_HI & ('n == 4)
then {
if get_config_print_platform()
then print_platform("clint-hi<4>[" ^ BitStr(addr) ^ "] -> " ^ BitStr(mtimecmp[63..32]));
then print_platform("clint-hi<4>[" ^ BitStr(addr) ^ "] -> " ^ BitStr(converted_mtimecmp[63..32]));
/* FIXME: Redundant zero_extend currently required by Lem backend */
Ok(zero_extend(32, mtimecmp[63..32]))
Ok(zero_extend(32, converted_mtimecmp[63..32]))
}
else if addr == MTIME_BASE & ('n == 4)
then {
if get_config_print_platform()
then print_platform("clint[" ^ BitStr(addr) ^ "] -> " ^ BitStr(mtime));
Ok(zero_extend(32, mtime[31..0]))
then print_platform("clint[" ^ BitStr(addr) ^ "] -> " ^ BitStr(converted_mtime));
Ok(zero_extend(32, converted_mtime[31..0]))
}
else if addr == MTIME_BASE & ('n == 8)
then {
if get_config_print_platform()
then print_platform("clint[" ^ BitStr(addr) ^ "] -> " ^ BitStr(mtime));
Ok(zero_extend(64, mtime))
then print_platform("clint[" ^ BitStr(addr) ^ "] -> " ^ BitStr(converted_mtime));
Ok(zero_extend(64, converted_mtime))
}
else if addr == MTIME_BASE_HI & ('n == 4)
then {
if get_config_print_platform()
then print_platform("clint[" ^ BitStr(addr) ^ "] -> " ^ BitStr(mtime));
Ok(zero_extend(32, mtime[63..32]))
then print_platform("clint[" ^ BitStr(addr) ^ "] -> " ^ BitStr(converted_mtime));
Ok(zero_extend(32, converted_mtime[63..32]))
}
else {
if get_config_print_platform()
Expand Down Expand Up @@ -308,17 +323,20 @@ function reset_htif () -> unit = {
* dispatched the address.
*/

val htif_load : forall 'n, 'n > 0. (AccessType(ext_access_type), physaddr, int('n)) -> MemoryOpResult(bits(8 * 'n))
function htif_load(t, Physaddr(paddr), width) = {
val htif_load : forall 'n, 'n > 0. (AccessType(ext_access_type), physaddr, int('n), Endianness) -> MemoryOpResult(bits(8 * 'n))
function htif_load(t, Physaddr(paddr), width, current_endianness) = {
var converted_htif_tohost = endianness_conversion(htif_tohost, current_endianness);
//htif_tohost is a 64 bit register, same logic as of mtime, mtimecmp for handling big endianness conversion.
if ((current_endianness == BigEndian) & width == 4) then converted_htif_tohost = converted_htif_tohost[31..0] @ converted_htif_tohost[63..32];
if get_config_print_platform()
then print_platform("htif[" ^ BitStr(paddr) ^ "] -> " ^ BitStr(htif_tohost));
then print_platform("htif[" ^ BitStr(paddr) ^ "] -> " ^ BitStr(converted_htif_tohost));
/* FIXME: For now, only allow the expected access widths. */
if width == 8 & (paddr == plat_htif_tohost())
then Ok(zero_extend(64, htif_tohost)) /* FIXME: Redundant zero_extend currently required by Lem backend */
then Ok(zero_extend(64, converted_htif_tohost)) /* FIXME: Redundant zero_extend currently required by Lem backend */
else if width == 4 & paddr == plat_htif_tohost()
then Ok(zero_extend(32, htif_tohost[31..0])) /* FIXME: Redundant zero_extend currently required by Lem backend */
then Ok(zero_extend(32, converted_htif_tohost[31..0])) /* FIXME: Redundant zero_extend currently required by Lem backend */
else if width == 4 & paddr == plat_htif_tohost() + 4
then Ok(zero_extend(32, htif_tohost[63..32])) /* FIXME: Redundant zero_extend currently required by Lem backend */
then Ok(zero_extend(32, converted_htif_tohost[63..32])) /* FIXME: Redundant zero_extend currently required by Lem backend */
else match t {
Execute() => Err(E_Fetch_Access_Fault()),
Read(Data) => Err(E_Load_Access_Fault()),
Expand Down Expand Up @@ -406,24 +424,25 @@ $else
function within_mmio_writable forall 'n, 0 < 'n <= max_mem_access . (addr : physaddr, width : int('n)) -> bool = false
$endif

function mmio_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_access_type), paddr : physaddr, width : int('n)) -> MemoryOpResult(bits(8 * 'n)) =
function mmio_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_access_type), paddr : physaddr, width : int('n), current_endianness : Endianness) -> MemoryOpResult(bits(8 * 'n)) =
if within_clint(paddr, width)
then clint_load(t, paddr, width)
then clint_load(t, paddr, width, current_endianness)
else if within_htif_readable(paddr, width) & (1 <= 'n)
then htif_load(t, paddr, width)
then htif_load(t, paddr, width, current_endianness)
else match t {
Execute() => Err(E_Fetch_Access_Fault()),
Read(Data) => Err(E_Load_Access_Fault()),
_ => Err(E_SAMO_Access_Fault())
}

function mmio_write forall 'n, 0 <'n <= max_mem_access . (paddr : physaddr, width : int('n), data: bits(8 * 'n)) -> MemoryOpResult(bool) =
function mmio_write forall 'n, 0 <'n <= max_mem_access . (paddr : physaddr, width : int('n), data: bits(8 * 'n)) -> MemoryOpResult(bool) = {
if within_clint(paddr, width)
then clint_store(paddr, width, data)
else if within_htif_writable(paddr, width) & 'n <= 8
then htif_store(paddr, width, data)
else Err(E_SAMO_Access_Fault())

}
/* Platform initialization and ticking. */

function init_platform() -> unit = {
Expand Down
5 changes: 1 addition & 4 deletions model/riscv_sys_control.sail
Original file line number Diff line number Diff line change
Expand Up @@ -341,10 +341,7 @@ function reset_sys() -> unit = {

// "If little-endian memory accesses are supported, the mstatus/mstatush field
// MBE is reset to 0."
// TODO: The handling of mstatush is a bit awkward currently, but the model
// currently only supports little endian so MBE is always 0.
// See https://github.com/riscv/sail-riscv/issues/639
// mstatus[MBE] = 0b0;
mstatus[MBE] = 0b0;

// "The misa register is reset to enable the maximal set of supported extensions"
reset_misa();
Expand Down
11 changes: 8 additions & 3 deletions model/riscv_sys_regs.sail
Original file line number Diff line number Diff line change
Expand Up @@ -187,6 +187,7 @@ bitfield Mstatus : bits(64) = {
SPP : 8,

MPIE : 7,
UBE : 6,
SPIE : 5,

MIE : 3,
Expand Down Expand Up @@ -223,9 +224,8 @@ function legalize_mstatus(o : Mstatus, v : bits(64)) -> Mstatus = {
// MPELP = v[MPELP],
// MPV = v[MPV],
// GVA = v[GVA],
/* We don't currently support changing MBE and SBE. */
// MBE = v[MBE],
// SBE = v[SBE],
MBE = v[MBE],
SBE = if currentlyEnabled(Ext_S) then v[SBE] else 0b0,
/* We don't support dynamic changes to SXL and UXL. */
// SXL = if xlen == 64 then v[SXL] else o[SXL],
// UXL = if xlen == 64 then v[UXL] else o[UXL],
Expand All @@ -249,6 +249,7 @@ function legalize_mstatus(o : Mstatus, v : bits(64)) -> Mstatus = {
SPP = if currentlyEnabled(Ext_S) then v[SPP] else 0b0,
VS = v[VS],
MPIE = v[MPIE],
UBE = if currentlyEnabled(Ext_U) then v[UBE] else 0b0,
SPIE = if currentlyEnabled(Ext_S) then v[SPIE] else 0b0,
MIE = v[MIE],
SIE = if currentlyEnabled(Ext_S) then v[SIE] else 0b0,
Expand All @@ -274,6 +275,7 @@ register mstatus : Mstatus = {
}

mapping clause csr_name_map = 0x300 <-> "mstatus"
mapping clause csr_name_map = 0x310 <-> "mstatush"

function clause is_CSR_defined(0x300) = true // mstatus
function clause is_CSR_defined(0x310) = xlen == 32 // mstatush
Expand Down Expand Up @@ -683,6 +685,7 @@ bitfield Sstatus : bits(64) = {
FS : 14 .. 13,
VS : 10 .. 9,
SPP : 8,
UBE : 6,
SPIE : 5,
SIE : 1,
}
Expand All @@ -702,6 +705,7 @@ function lower_mstatus(m : Mstatus) -> Sstatus = {
FS = m[FS],
VS = m[VS],
SPP = m[SPP],
UBE = m[UBE],
SPIE = m[SPIE],
SIE = m[SIE],
]
Expand All @@ -722,6 +726,7 @@ function lift_sstatus(m : Mstatus, s : Sstatus) -> Mstatus = {
FS = s[FS],
VS = s[VS],
SPP = s[SPP],
UBE = s[UBE],
SPIE = s[SPIE],
SIE = s[SIE],
]
Expand Down
3 changes: 3 additions & 0 deletions model/riscv_types.sail
Original file line number Diff line number Diff line change
Expand Up @@ -341,6 +341,9 @@ enum extop_zbb = {RISCV_SEXTB, RISCV_SEXTH, RISCV_ZEXTH}

enum zicondop = {RISCV_CZERO_EQZ, RISCV_CZERO_NEZ}

//Endianness type.
enum Endianness = { BigEndian, LittleEndian }

// Get the bit encoding of word_width.
mapping size_enc : word_width <-> bits(2) = {
BYTE <-> 0b00,
Expand Down
1 change: 1 addition & 0 deletions test/first_party/CMakeLists.txt
Original file line number Diff line number Diff line change
Expand Up @@ -85,6 +85,7 @@ set(tests
"test_hello_world.c"
"test_max_pmp.c"
"test_minstret.S"
"test_endianness.S"
)

foreach (xlen IN ITEMS 32 64)
Expand Down
Loading
Loading