diff options
| -rw-r--r-- | Makefile | 7 | ||||
| -rw-r--r-- | model/main.sail | 63 | ||||
| -rw-r--r-- | model/prelude.sail | 2 | ||||
| -rw-r--r-- | model/prelude_mem.sail | 131 | ||||
| -rw-r--r-- | model/riscv_analysis.sail | 367 | ||||
| -rw-r--r-- | model/riscv_insts_aext.sail | 337 | ||||
| -rw-r--r-- | model/riscv_insts_base.sail | 70 | ||||
| -rw-r--r-- | model/riscv_insts_mext.sail | 160 | ||||
| -rw-r--r-- | model/riscv_insts_vext_vset.sail | 2 | ||||
| -rw-r--r-- | model/riscv_pc_access.sail | 1 | ||||
| -rw-r--r-- | model/riscv_step.sail | 7 | ||||
| -rw-r--r-- | model/riscv_vmem.sail | 35 |
12 files changed, 439 insertions, 743 deletions
@@ -109,16 +109,13 @@ SAIL_ARCH_SRCS += riscv_types_kext.sail # Shared/common code for the cryptogr SAIL_STEP_SRCS = riscv_step_common.sail riscv_step_ext.sail riscv_decode_ext.sail riscv_fetch.sail riscv_step.sail RVFI_STEP_SRCS = riscv_step_common.sail riscv_step_rvfi.sail riscv_decode_ext.sail riscv_fetch_rvfi.sail riscv_step.sail -# Control inclusion of 64-bit only riscv_analysis -ifeq ($(ARCH),RV32) SAIL_OTHER_SRCS = $(SAIL_STEP_SRCS) +ifeq ($(ARCH),RV32) SAIL_OTHER_COQ_SRCS = riscv_termination_common.sail riscv_termination_rv32.sail else -SAIL_OTHER_SRCS = $(SAIL_STEP_SRCS) riscv_analysis.sail -SAIL_OTHER_COQ_SRCS = riscv_termination_common.sail riscv_termination_rv64.sail riscv_analysis.sail +SAIL_OTHER_COQ_SRCS = riscv_termination_common.sail riscv_termination_rv64.sail endif - PRELUDE_SRCS = $(addprefix model/,$(PRELUDE)) SAIL_SRCS = $(addprefix model/,$(SAIL_ARCH_SRCS) $(SAIL_SEQ_INST_SRCS) $(SAIL_OTHER_SRCS)) SAIL_RMEM_SRCS = $(addprefix model/,$(SAIL_ARCH_SRCS) $(SAIL_RMEM_INST_SRCS) $(SAIL_OTHER_SRCS)) diff --git a/model/main.sail b/model/main.sail index c545e27..1422635 100644 --- a/model/main.sail +++ b/model/main.sail @@ -6,19 +6,74 @@ /* SPDX-License-Identifier: BSD-2-Clause */ /*=======================================================================================*/ -function main () : unit -> unit = { +// When the symbolic execution is running a litmus test, it sets a +// different entry point for each thread in the compiled litmus test. + +val get_entry_point : unit -> xlenbits + +$ifdef SYMBOLIC + +$include <elf.sail> + +function get_entry_point() = to_bits(sizeof(xlen), elf_entry()) + +$else + +function get_entry_point() = zero_extend(0x1000) + +$endif + +function main() : unit -> unit = { // initialize extensions - ext_init (); + ext_init(); - // PC = __GetSlice_int(64, elf_entry(), 0); - PC = sail_zero_extend(0x1000, sizeof(xlen)); + PC = get_entry_point(); print_bits("PC = ", PC); try { init_model(); + sail_end_cycle(); loop() } catch { Error_not_implemented(s) => print_string("Error: Not implemented: ", s), Error_internal_error() => print("Error: internal error") } } + +// For symbolic execution using Isla, we need an entry point that +// allows us to execute a single instruction. +$ifdef SYMBOLIC + +$include <isla.sail> + +val isla_footprint_no_init : forall 'n, 'n in {16, 32}. bits('n) -> bool + +function isla_footprint_no_init(opcode) = { + try { + isla_reset_registers(); + sail_end_cycle(); + + let instr = if length(opcode) == 16 then { + ext_decode_compressed(opcode) + } else { + ext_decode(opcode) + }; + let _ = execute(instr); + true + } catch { + _ => false + } +} + +val isla_footprint : forall 'n, 'n in {16, 32}. bits('n) -> bool + +function isla_footprint(opcode) = { + try { + init_model(); + isla_footprint_no_init(opcode) + } catch { + _ => false + } +} + +$endif diff --git a/model/prelude.sail b/model/prelude.sail index 028af21..b876b4f 100644 --- a/model/prelude.sail +++ b/model/prelude.sail @@ -14,11 +14,9 @@ $include <arith.sail> $include <string.sail> $include "mapping.sail" $include <vector_dec.sail> -$include <regfp.sail> $include <generic_equality.sail> $include "hex_bits.sail" - val not_bit : bit -> bit function not_bit(b) = if b == bitone then bitzero else bitone diff --git a/model/prelude_mem.sail b/model/prelude_mem.sail index c4f3d07..345e78c 100644 --- a/model/prelude_mem.sail +++ b/model/prelude_mem.sail @@ -12,12 +12,68 @@ * They also depend on the type of metadata that is read and written * to physical memory. For models that do not require this metadata, * a unit type can be used. - * - * The underlying __read_mem and __write_mem functions are from the - * Sail library. The metadata primitives __{Read,Write}RAM_Meta are - * in prelude_mem_metadata. */ +$include <concurrency_interface.sail> + +enum write_kind = { + Write_plain, + Write_RISCV_release, + Write_RISCV_strong_release, + Write_RISCV_conditional, + Write_RISCV_conditional_release, + Write_RISCV_conditional_strong_release, +} + +enum read_kind = { + Read_plain, + Read_ifetch, + Read_RISCV_acquire, + Read_RISCV_strong_acquire, + Read_RISCV_reserved, + Read_RISCV_reserved_acquire, + Read_RISCV_reserved_strong_acquire, +} + +enum barrier_kind = { + Barrier_RISCV_rw_rw, + Barrier_RISCV_r_rw, + Barrier_RISCV_r_r, + Barrier_RISCV_rw_w, + Barrier_RISCV_w_w, + Barrier_RISCV_w_rw, + Barrier_RISCV_rw_r, + Barrier_RISCV_r_w, + Barrier_RISCV_w_r, + Barrier_RISCV_tso, + Barrier_RISCV_i, +} + +/* Most of the above read/write_kinds are understood natively by the + Sail concurrency interface, except for the strong acquire release + variants which require an architecture specific access kind. */ +struct RISCV_strong_access = { + variety : Access_variety, +} + +/* The Sail concurrency interface lets us have a physical address type + with additional information, provided we can supply a function that + converts it into a bitvector. Since we are just using xlenbits as a + physical address, we need the identity function for xlenbits. */ +val xlenbits_identity : xlenbits -> xlenbits + +function xlenbits_identity xs = xs + +instantiation sail_mem_write with + 'pa = xlenbits, + pa_bits = xlenbits_identity, + /* We don't have a relaxed-memory translation model for RISC-V, so + we just use unit as a dummy type. */ + 'translation_summary = unit, + 'arch_ak = RISCV_strong_access, + /* Similarly to translation_summary, we don't have a defined type for external + aborts, so just use unit here too */ + 'abort = unit /* This is a slightly arbitrary limit on the maximum number of bytes in a memory access. It helps to generate slightly better C code @@ -27,8 +83,25 @@ capabilities and SIMD / vector instructions will also need more. */ type max_mem_access : Int = 16 -val write_ram = {lem: "write_ram", coq: "write_ram"} : forall 'n, 0 < 'n <= max_mem_access . (write_kind, xlenbits, int('n), bits(8 * 'n), mem_meta) -> bool +val write_ram : forall 'n, 0 < 'n <= max_mem_access. (write_kind, xlenbits, int('n), bits(8 * 'n), mem_meta) -> bool + function write_ram(wk, addr, width, data, meta) = { + let request : Mem_write_request('n, 64, xlenbits, unit, RISCV_strong_access) = struct { + access_kind = match wk { + Write_plain => AK_explicit(struct { variety = AV_plain, strength = AS_normal }), + Write_RISCV_release => AK_explicit(struct { variety = AV_plain, strength = AS_rel_or_acq }), + Write_RISCV_strong_release => AK_arch(struct { variety = AV_plain }), + Write_RISCV_conditional => AK_explicit(struct { variety = AV_exclusive, strength = AS_normal }), + Write_RISCV_conditional_release => AK_explicit(struct { variety = AV_exclusive, strength = AS_rel_or_acq }), + Write_RISCV_conditional_strong_release => AK_arch(struct { variety = AV_exclusive }), + }, + va = None(), + pa = addr, + translation = (), + size = width, + value = Some(data), + tag = None(), + }; /* Write out metadata only if the value write succeeds. * It is assumed for now that this write always succeeds; * there is currently no return value. @@ -36,19 +109,47 @@ function write_ram(wk, addr, width, data, meta) = { * (not just for Lem) to consume the value along with the * metadata to ensure atomicity. */ - let ret : bool = __write_mem(wk, sizeof(xlen), addr, width, data); - if ret then __WriteRAM_Meta(addr, width, meta); - ret + match sail_mem_write(request) { + Ok(_) => { + __WriteRAM_Meta(addr, width, meta); + true + }, + Err() => false, + } } -val write_ram_ea : forall 'n, 0 < 'n <= max_mem_access . (write_kind, xlenbits, int('n)) -> unit -function write_ram_ea(wk, addr, width) = - __write_mem_ea(wk, sizeof(xlen), addr, width) +val write_ram_ea : forall 'n, 0 < 'n <= max_mem_access. (write_kind, xlenbits, int('n)) -> unit +function write_ram_ea(wk, addr, width) = () + +instantiation sail_mem_read with + pa_bits = xlenbits_identity + +val read_ram : forall 'n, 0 < 'n <= max_mem_access. (read_kind, xlenbits, int('n), bool) -> (bits(8 * 'n), mem_meta) +function read_ram(rk, addr, width, read_meta) = { + let meta = if read_meta then __ReadRAM_Meta(addr, width) else default_meta; + let request : Mem_read_request('n, 64, xlenbits, unit, RISCV_strong_access) = struct { + access_kind = match rk { + Read_plain => AK_explicit(struct { variety = AV_plain, strength = AS_normal }), + Read_ifetch => AK_ifetch(), + Read_RISCV_acquire => AK_explicit(struct { variety = AV_plain, strength = AS_rel_or_acq }), + Read_RISCV_strong_acquire => AK_arch(struct { variety = AV_plain }), + Read_RISCV_reserved => AK_explicit(struct { variety = AV_exclusive, strength = AS_normal }), + Read_RISCV_reserved_acquire => AK_explicit(struct { variety = AV_exclusive, strength = AS_rel_or_acq }), + Read_RISCV_reserved_strong_acquire => AK_arch(struct { variety = AV_exclusive }), + }, + va = None(), + pa = addr, + translation = (), + size = width, + tag = false, + }; + match sail_mem_read(request) { + Ok((value, _)) => (value, meta), + Err() => exit(), + } +} -val read_ram = {lem: "read_ram", coq: "read_ram"} : forall 'n, 0 < 'n <= max_mem_access . (read_kind, xlenbits, int('n), bool) -> (bits(8 * 'n), mem_meta) -function read_ram(rk, addr, width, read_meta) = - let meta = if read_meta then __ReadRAM_Meta(addr, width) else default_meta in - (__read_mem(rk, sizeof(xlen), addr, width), meta) +instantiation sail_barrier with 'barrier = barrier_kind val __TraceMemoryWrite : forall 'n 'm. (int('n), bits('m), bits(8 * 'n)) -> unit val __TraceMemoryRead : forall 'n 'm. (int('n), bits('m), bits(8 * 'n)) -> unit diff --git a/model/riscv_analysis.sail b/model/riscv_analysis.sail deleted file mode 100644 index 0d72bed..0000000 --- a/model/riscv_analysis.sail +++ /dev/null @@ -1,367 +0,0 @@ -/*=======================================================================================*/ -/* 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 */ -/*=======================================================================================*/ - -$include <regfp.sail> - -/* in reverse order because inc vectors don't seem to work (bug) */ -let GPRstrs : vector(32, dec, string) = [ "x31", "x30", "x29", "x28", "x27", "x26", "x25", "x24", "x23", "x22", "x21", - "x20", "x19", "x18", "x17", "x16", "x15", "x14", "x13", "x12", "x11", - "x10", "x9", "x8", "x7", "x6", "x5", "x4", "x3", "x2", "x1", "x0" - ] - -function GPRstr(i: bits(5)) -> string = GPRstrs[unsigned(i)] - -let CIA_fp = RFull("CIA") -let NIA_fp = RFull("NIA") - -$ifndef FEATURE_UNION_BARRIER - -function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,instruction_kind) = { - iR = [| |] : regfps; - oR = [| |] : regfps; - aR = [| |] : regfps; - ik = IK_simple() : instruction_kind; - Nias = [| NIAFP_successor() |] : niafps; - Dia = DIAFP_none() : diafp; - - match instr { - EBREAK() => (), - UTYPE(imm, rd, op) => { - if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR; - }, - RISCV_JAL(imm, rd) => { - if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR; - let offset : bits(64) = sign_extend(imm) in - Nias = [| NIAFP_concrete_address (PC + offset) |]; - ik = IK_branch(); - }, - RISCV_JALR(imm, rs, rd) => { - if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR; - if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR; - let offset : bits(64) = sign_extend(imm) in - Nias = [| NIAFP_indirect_address() |]; - ik = IK_branch(); - }, - BTYPE(imm, rs2, rs1, op) => { - if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR; - if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR; - ik = IK_branch(); - let offset : bits(64) = sign_extend(imm) in - Nias = [| NIAFP_concrete_address(PC + offset), NIAFP_successor() |]; - }, - ITYPE(imm, rs, rd, op) => { - if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR; - if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR; - }, - SHIFTIOP(imm, rs, rd, op) => { - if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR; - if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR; - }, - RTYPE(rs2, rs1, rd, op) => { - if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR; - if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR; - if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR; - }, - CSR(csr, rs1, rd, is_imm, op) => { - let isWrite : bool = match op { - CSRRW => true, - _ => if is_imm then unsigned(rs1) != 0 else unsigned(rs1) != 0 - }; - iR = RFull(csr_name(csr)) :: iR; - if not(is_imm) then { - iR = RFull(GPRstr(rs1)) :: iR; - }; - if isWrite then { - oR = RFull(csr_name(csr)) :: oR; - }; - oR = RFull(GPRstr(rd)) :: oR; - }, - LOAD(imm, rs, rd, unsign, width, aq, rl) => { /* XXX "unsigned" causes name conflict in lem shallow embedding... */ - if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR; - if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR; - aR = iR; - ik = - match (aq, rl) { - (false, false) => IK_mem_read (Read_plain), - (true, false) => IK_mem_read (Read_RISCV_acquire), - (true, true) => IK_mem_read (Read_RISCV_strong_acquire), - - _ => internal_error(__FILE__, __LINE__, "LOAD type not implemented in initial_analysis") - } - }, - STORE(imm, rs2, rs1, width, aq, rl) => { - if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR; - if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR; - if (rs1 == 0b00000) then () else aR = RFull(GPRstr(rs1)) :: aR; - ik = - match (aq, rl) { - (false, false) => IK_mem_write (Write_plain), - (false, true) => IK_mem_write (Write_RISCV_release), - (true, true) => IK_mem_write (Write_RISCV_strong_release), - - _ => internal_error(__FILE__, __LINE__, "STORE type not implemented in initial_analysis") - } - }, - ADDIW(imm, rs, rd) => { - if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR; - if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR; - }, - SHIFTIWOP(imm, rs, rd, op) => { - if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR; - if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR; - }, - RTYPEW(rs2, rs1, rd, op) => { - if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR; - if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR; - if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR; - }, - FENCE(pred, succ) => { - ik = - match (pred, succ) { - (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => IK_barrier (Barrier_RISCV_rw_rw), - (_ : bits(2) @ 0b10, _ : bits(2) @ 0b11) => IK_barrier (Barrier_RISCV_r_rw), - (_ : bits(2) @ 0b10, _ : bits(2) @ 0b10) => IK_barrier (Barrier_RISCV_r_r), - (_ : bits(2) @ 0b11, _ : bits(2) @ 0b01) => IK_barrier (Barrier_RISCV_rw_w), - (_ : bits(2) @ 0b01, _ : bits(2) @ 0b01) => IK_barrier (Barrier_RISCV_w_w), - (_ : bits(2) @ 0b01, _ : bits(2) @ 0b11) => IK_barrier (Barrier_RISCV_w_rw), - (_ : bits(2) @ 0b11, _ : bits(2) @ 0b10) => IK_barrier (Barrier_RISCV_rw_r), - (_ : bits(2) @ 0b10, _ : bits(2) @ 0b01) => IK_barrier (Barrier_RISCV_r_w), - (_ : bits(2) @ 0b01, _ : bits(2) @ 0b10) => IK_barrier (Barrier_RISCV_w_r), - - - (_ : bits(2) @ 0b00, _ : bits(2) @ 0b00) => IK_simple (), - - _ => internal_error(__FILE__, __LINE__, "barrier type not implemented in initial_analysis") - }; - }, - FENCE_TSO(pred, succ) => { - ik = - match (pred, succ) { - (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => IK_barrier (Barrier_RISCV_tso), - _ => internal_error(__FILE__, __LINE__, "barrier type not implemented in initial_analysis") - }; - }, - FENCEI() => { - ik = IK_simple (); // for RMEM, should morally be Barrier_RISCV_i - }, - LOADRES(aq, rl, rs1, width, rd) => { - if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR; - if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR; - aR = iR; - ik = match (aq, rl) { - (false, false) => IK_mem_read (Read_RISCV_reserved), - (true, false) => IK_mem_read (Read_RISCV_reserved_acquire), - (true, true) => IK_mem_read (Read_RISCV_reserved_strong_acquire), - (false, true) => internal_error(__FILE__, __LINE__, "LOADRES type not implemented in initial_analysis") - }; - }, - STORECON(aq, rl, rs2, rs1, width, rd) => { - if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR; - if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR; - if (rs1 == 0b00000) then () else aR = RFull(GPRstr(rs1)) :: aR; - if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR; - ik = match (aq, rl) { - (false, false) => IK_mem_write (Write_RISCV_conditional), - (false, true) => IK_mem_write (Write_RISCV_conditional_release), - (true, true) => IK_mem_write (Write_RISCV_conditional_strong_release), - - (true, false) => internal_error(__FILE__, __LINE__, "STORECON type not implemented in initial_analysis") - }; - }, - AMO(op, aq, rl, rs2, rs1, width, rd) => { - if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR; - if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR; - if (rs1 == 0b00000) then () else aR = RFull(GPRstr(rs1)) :: aR; - if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR; - ik = match (aq, rl) { - (false, false) => IK_mem_rmw (Read_RISCV_reserved, Write_RISCV_conditional), - (false, true) => IK_mem_rmw (Read_RISCV_reserved, Write_RISCV_conditional_release), - (true, false) => IK_mem_rmw (Read_RISCV_reserved_acquire, - Write_RISCV_conditional), - (true, true) => IK_mem_rmw (Read_RISCV_reserved_acquire, - Write_RISCV_conditional_release) - }; - }, - _ => () - }; - (iR,oR,aR,Nias,Dia,ik) -} - -$else - -function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,instruction_kind) = { - iR = [| |] : regfps; - oR = [| |] : regfps; - aR = [| |] : regfps; - ik = IK_simple() : instruction_kind; - Nias = [| NIAFP_successor() |] : niafps; - Dia = DIAFP_none() : diafp; - - match instr { - EBREAK() => (), - UTYPE(imm, rd, op) => { - if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR; - }, - RISCV_JAL(imm, rd) => { - if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR; - let offset : bits(64) = sign_extend(imm) in - Nias = [| NIAFP_concrete_address (PC + offset) |]; - ik = IK_branch(); - }, - RISCV_JALR(imm, rs, rd) => { - if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR; - if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR; - let offset : bits(64) = sign_extend(imm) in - Nias = [| NIAFP_indirect_address() |]; - ik = IK_branch(); - }, - BTYPE(imm, rs2, rs1, op) => { - if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR; - if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR; - ik = IK_branch(); - let offset : bits(64) = sign_extend(imm) in - Nias = [| NIAFP_concrete_address(PC + offset), NIAFP_successor() |]; - }, - ITYPE(imm, rs, rd, op) => { - if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR; - if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR; - }, - SHIFTIOP(imm, rs, rd, op) => { - if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR; - if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR; - }, - RTYPE(rs2, rs1, rd, op) => { - if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR; - if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR; - if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR; - }, - CSR(csr, rs1, rd, is_imm, op) => { - let isWrite : bool = match op { - CSRRW => true, - _ => if is_imm then unsigned(rs1) != 0 else unsigned(rs1) != 0 - }; - iR = RFull(csr_name(csr)) :: iR; - if not(is_imm) then { - iR = RFull(GPRstr(rs1)) :: iR; - }; - if isWrite then { - oR = RFull(csr_name(csr)) :: oR; - }; - oR = RFull(GPRstr(rd)) :: oR; - }, - LOAD(imm, rs, rd, unsign, width, aq, rl) => { /* XXX "unsigned" causes name conflict in lem shallow embedding... */ - if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR; - if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR; - aR = iR; - ik = - match (aq, rl) { - (false, false) => IK_mem_read (Read_plain), - (true, false) => IK_mem_read (Read_RISCV_acquire), - (true, true) => IK_mem_read (Read_RISCV_strong_acquire), - - _ => internal_error(__FILE__, __LINE__, "LOAD type not implemented in initial_analysis") - } - }, - STORE(imm, rs2, rs1, width, aq, rl) => { - if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR; - if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR; - if (rs1 == 0b00000) then () else aR = RFull(GPRstr(rs1)) :: aR; - ik = - match (aq, rl) { - (false, false) => IK_mem_write (Write_plain), - (false, true) => IK_mem_write (Write_RISCV_release), - (true, true) => IK_mem_write (Write_RISCV_strong_release), - - _ => internal_error(__FILE__, __LINE__, "STORE type not implemented in initial_analysis") - } - }, - ADDIW(imm, rs, rd) => { - if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR; - if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR; - }, - SHIFTIWOP(imm, rs, rd, op) => { - if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR; - if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR; - }, - RTYPEW(rs2, rs1, rd, op) => { - if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR; - if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR; - if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR; - }, - FENCE(pred, succ) => { - ik = - match (pred, succ) { - (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => IK_barrier (Barrier_RISCV_rw_rw ()), - (_ : bits(2) @ 0b10, _ : bits(2) @ 0b11) => IK_barrier (Barrier_RISCV_r_rw ()), - (_ : bits(2) @ 0b10, _ : bits(2) @ 0b10) => IK_barrier (Barrier_RISCV_r_r ()), - (_ : bits(2) @ 0b11, _ : bits(2) @ 0b01) => IK_barrier (Barrier_RISCV_rw_w ()), - (_ : bits(2) @ 0b01, _ : bits(2) @ 0b01) => IK_barrier (Barrier_RISCV_w_w ()), - (_ : bits(2) @ 0b01, _ : bits(2) @ 0b11) => IK_barrier (Barrier_RISCV_w_rw ()), - (_ : bits(2) @ 0b11, _ : bits(2) @ 0b10) => IK_barrier (Barrier_RISCV_rw_r ()), - (_ : bits(2) @ 0b10, _ : bits(2) @ 0b01) => IK_barrier (Barrier_RISCV_r_w ()), - (_ : bits(2) @ 0b01, _ : bits(2) @ 0b10) => IK_barrier (Barrier_RISCV_w_r ()), - - (_ : bits(2) @ 0b00, _ : bits(2) @ 0b00) => IK_simple (), - - _ => internal_error(__FILE__, __LINE__, "barrier type not implemented in initial_analysis") - }; - }, - FENCE_TSO(pred, succ) => { - ik = - match (pred, succ) { - (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => IK_barrier (Barrier_RISCV_tso ()), - _ => internal_error(__FILE__, __LINE__, "barrier type not implemented in initial_analysis") - }; - }, - FENCEI() => { - ik = IK_simple (); // for RMEM, should morally be Barrier_RISCV_i - }, - LOADRES(aq, rl, rs1, width, rd) => { - if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR; - if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR; - aR = iR; - ik = match (aq, rl) { - (false, false) => IK_mem_read (Read_RISCV_reserved), - (true, false) => IK_mem_read (Read_RISCV_reserved_acquire), - (true, true) => IK_mem_read (Read_RISCV_reserved_strong_acquire), - (false, true) => internal_error(__FILE__, __LINE__, "LOADRES type not implemented in initial_analysis") - }; - }, - STORECON(aq, rl, rs2, rs1, width, rd) => { - if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR; - if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR; - if (rs1 == 0b00000) then () else aR = RFull(GPRstr(rs1)) :: aR; - if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR; - ik = match (aq, rl) { - (false, false) => IK_mem_write (Write_RISCV_conditional), - (false, true) => IK_mem_write (Write_RISCV_conditional_release), - (true, true) => IK_mem_write (Write_RISCV_conditional_strong_release), - - (true, false) => internal_error(__FILE__, __LINE__, "STORECON type not implemented in initial_analysis") - }; - }, - AMO(op, aq, rl, rs2, rs1, width, rd) => { - if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR; - if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR; - if (rs1 == 0b00000) then () else aR = RFull(GPRstr(rs1)) :: aR; - if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR; - ik = match (aq, rl) { - (false, false) => IK_mem_rmw (Read_RISCV_reserved, Write_RISCV_conditional), - (false, true) => IK_mem_rmw (Read_RISCV_reserved, Write_RISCV_conditional_release), - (true, false) => IK_mem_rmw (Read_RISCV_reserved_acquire, - Write_RISCV_conditional), - (true, true) => IK_mem_rmw (Read_RISCV_reserved_acquire, - Write_RISCV_conditional_release) - }; - }, - _ => () - }; - (iR,oR,aR,Nias,Dia,ik) -} - -$endif diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail index 0f4da83..2e0eb9c 100644 --- a/model/riscv_insts_aext.sail +++ b/model/riscv_insts_aext.sail @@ -43,8 +43,8 @@ function amo_width_valid(size : word_width) -> bool = { /* ****************************************************************** */ union clause ast = LOADRES : (bool, bool, regidx, word_width, regidx) -mapping clause encdec = LOADRES(aq, rl, rs1, size, rd) if amo_width_valid(size) - <-> 0b00010 @ bool_bits(aq) @ bool_bits(rl) @ 0b00000 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 if amo_width_valid(size) +mapping clause encdec = LOADRES(aq, rl, rs1, size, rd) if haveAtomics() & amo_width_valid(size) + <-> 0b00010 @ bool_bits(aq) @ bool_bits(rl) @ 0b00000 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 if haveAtomics() & amo_width_valid(size) /* We could set load-reservations on physical or virtual addresses. @@ -61,44 +61,39 @@ function process_loadres(rd, addr, value, is_unsigned) = } function clause execute(LOADRES(aq, rl, rs1, width, rd)) = { - if haveAtomics() then { - /* Get the address, X(rs1) (no offset). - * Extensions might perform additional checks on address validity. - */ - match ext_data_get_addr(rs1, zeros(), Read(Data), width) { - Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, - Ext_DataAddr_OK(vaddr) => { - let aligned : bool = - /* BYTE and HALF would only occur due to invalid decodes, but it doesn't hurt - * to treat them as valid here; otherwise we'd need to throw an internal_error. - */ - match width { - BYTE => true, - HALF => vaddr[0..0] == 0b0, - WORD => vaddr[1..0] == 0b00, - DOUBLE => vaddr[2..0] == 0b000 - }; - /* "LR faults like a normal load, even though it's in the AMO major opcode space." - * - Andrew Waterman, isa-dev, 10 Jul 2018. - */ - if not(aligned) - then { handle_mem_exception(vaddr, E_Load_Addr_Align()); RETIRE_FAIL } - else match translateAddr(vaddr, Read(Data)) { - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, - TR_Address(addr, _) => - match (width, sizeof(xlen)) { - (BYTE, _) => process_loadres(rd, vaddr, mem_read(Read(Data), addr, 1, aq, aq & rl, true), false), - (HALF, _) => process_loadres(rd, vaddr, mem_read(Read(Data), addr, 2, aq, aq & rl, true), false), - (WORD, _) => process_loadres(rd, vaddr, mem_read(Read(Data), addr, 4, aq, aq & rl, true), false), - (DOUBLE, 64) => process_loadres(rd, vaddr, mem_read(Read(Data), addr, 8, aq, aq & rl, true), false), - _ => internal_error(__FILE__, __LINE__, "Unexpected AMO width") - } - } - } + /* Get the address, X(rs1) (no offset). + * Extensions might perform additional checks on address validity. + */ + match ext_data_get_addr(rs1, zeros(), Read(Data), width) { + Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, + Ext_DataAddr_OK(vaddr) => { + let aligned : bool = + /* BYTE and HALF would only occur due to invalid decodes, but it doesn't hurt + * to treat them as valid here; otherwise we'd need to throw an internal_error. + */ + match width { + BYTE => true, + HALF => vaddr[0..0] == 0b0, + WORD => vaddr[1..0] == 0b00, + DOUBLE => vaddr[2..0] == 0b000 + }; + /* "LR faults like a normal load, even though it's in the AMO major opcode space." + * - Andrew Waterman, isa-dev, 10 Jul 2018. + */ + if not(aligned) + then { handle_mem_exception(vaddr, E_Load_Addr_Align()); RETIRE_FAIL } + else match translateAddr(vaddr, Read(Data)) { + TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, + TR_Address(addr, _) => + match (width, sizeof(xlen)) { + (BYTE, _) => process_loadres(rd, vaddr, mem_read(Read(Data), addr, 1, aq, aq & rl, true), false), + (HALF, _) => process_loadres(rd, vaddr, mem_read(Read(Data), addr, 2, aq, aq & rl, true), false), + (WORD, _) => process_loadres(rd, vaddr, mem_read(Read(Data), addr, 4, aq, aq & rl, true), false), + (DOUBLE, 64) => process_loadres(rd, vaddr, mem_read(Read(Data), addr, 8, aq, aq & rl, true), false), + _ => internal_error(__FILE__, __LINE__, "Unexpected AMO width") + } + } } - } else { - handle_illegal(); - RETIRE_FAIL } } @@ -108,8 +103,8 @@ mapping clause assembly = LOADRES(aq, rl, rs1, size, rd) /* ****************************************************************** */ union clause ast = STORECON : (bool, bool, regidx, regidx, word_width, regidx) -mapping clause encdec = STORECON(aq, rl, rs2, rs1, size, rd) if amo_width_valid(size) - <-> 0b00011 @ bool_bits(aq) @ bool_bits(rl) @ rs2 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 if amo_width_valid(size) +mapping clause encdec = STORECON(aq, rl, rs2, rs1, size, rd) if haveAtomics() & amo_width_valid(size) + <-> 0b00011 @ bool_bits(aq) @ bool_bits(rl) @ rs2 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 if haveAtomics() & amo_width_valid(size) /* NOTE: Currently, we only EA if address translation is successful. This may need revisiting. */ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = { @@ -119,60 +114,58 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = { */ X(rd) = zero_extend(0b1); RETIRE_SUCCESS } else { - if haveAtomics() then { - /* normal non-rmem case - * rmem: SC is allowed to succeed (but might fail later) - */ - /* Get the address, X(rs1) (no offset). - * Extensions might perform additional checks on address validity. - */ - match ext_data_get_addr(rs1, zeros(), Write(Data), width) { - Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, - Ext_DataAddr_OK(vaddr) => { - let aligned : bool = - /* BYTE and HALF would only occur due to invalid decodes, but it doesn't hurt - * to treat them as valid here; otherwise we'd need to throw an internal_error. - */ - match width { - BYTE => true, - HALF => vaddr[0..0] == 0b0, - WORD => vaddr[1..0] == 0b00, - DOUBLE => vaddr[2..0] == 0b000 - }; - if not(aligned) - then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); RETIRE_FAIL } - else { - if match_reservation(vaddr) == false then { - /* cannot happen in rmem */ - X(rd) = zero_extend(0b1); cancel_reservation(); RETIRE_SUCCESS - } else { - match translateAddr(vaddr, Write(Data)) { /* Write and ReadWrite are equivalent here: - * both result in a SAMO exception */ - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, - TR_Address(addr, _) => { - let eares : MemoryOpResult(unit) = match (width, sizeof(xlen)) { - (BYTE, _) => mem_write_ea(addr, 1, aq & rl, rl, true), - (HALF, _) => mem_write_ea(addr, 2, aq & rl, rl, true), - (WORD, _) => mem_write_ea(addr, 4, aq & rl, rl, true), - (DOUBLE, 64) => mem_write_ea(addr, 8, aq & rl, rl, true), - _ => internal_error(__FILE__, __LINE__, "STORECON expected word or double") - }; - match (eares) { - MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, - MemValue(_) => { - rs2_val = X(rs2); - let res : MemoryOpResult(bool) = match (width, sizeof(xlen)) { - (BYTE, _) => mem_write_value(addr, 1, rs2_val[7..0], aq & rl, rl, true), - (HALF, _) => mem_write_value(addr, 2, rs2_val[15..0], aq & rl, rl, true), - (WORD, _) => mem_write_value(addr, 4, rs2_val[31..0], aq & rl, rl, true), - (DOUBLE, 64) => mem_write_value(addr, 8, rs2_val, aq & rl, rl, true), - _ => internal_error(__FILE__, __LINE__, "STORECON expected word or double") - }; - match (res) { - MemValue(true) => { X(rd) = zero_extend(0b0); cancel_reservation(); RETIRE_SUCCESS }, - MemValue(false) => { X(rd) = zero_extend(0b1); cancel_reservation(); RETIRE_SUCCESS }, - MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL } - } + /* normal non-rmem case + * rmem: SC is allowed to succeed (but might fail later) + */ + /* Get the address, X(rs1) (no offset). + * Extensions might perform additional checks on address validity. + */ + match ext_data_get_addr(rs1, zeros(), Write(Data), width) { + Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, + Ext_DataAddr_OK(vaddr) => { + let aligned : bool = + /* BYTE and HALF would only occur due to invalid decodes, but it doesn't hurt + * to treat them as valid here; otherwise we'd need to throw an internal_error. + */ + match width { + BYTE => true, + HALF => vaddr[0..0] == 0b0, + WORD => vaddr[1..0] == 0b00, + DOUBLE => vaddr[2..0] == 0b000 + }; + if not(aligned) + then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); RETIRE_FAIL } + else { + if match_reservation(vaddr) == false then { + /* cannot happen in rmem */ + X(rd) = zero_extend(0b1); cancel_reservation(); RETIRE_SUCCESS + } else { + match translateAddr(vaddr, Write(Data)) { /* Write and ReadWrite are equivalent here: + * both result in a SAMO exception */ + TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, + TR_Address(addr, _) => { + let eares : MemoryOpResult(unit) = match (width, sizeof(xlen)) { + (BYTE, _) => mem_write_ea(addr, 1, aq & rl, rl, true), + (HALF, _) => mem_write_ea(addr, 2, aq & rl, rl, true), + (WORD, _) => mem_write_ea(addr, 4, aq & rl, rl, true), + (DOUBLE, 64) => mem_write_ea(addr, 8, aq & rl, rl, true), + _ => internal_error(__FILE__, __LINE__, "STORECON expected word or double") + }; + match (eares) { + MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, + MemValue(_) => { + rs2_val = X(rs2); + let res : MemoryOpResult(bool) = match (width, sizeof(xlen)) { + (BYTE, _) => mem_write_value(addr, 1, rs2_val[7..0], aq & rl, rl, true), + (HALF, _) => mem_write_value(addr, 2, rs2_val[15..0], aq & rl, rl, true), + (WORD, _) => mem_write_value(addr, 4, rs2_val[31..0], aq & rl, rl, true), + (DOUBLE, 64) => mem_write_value(addr, 8, rs2_val, aq & rl, rl, true), + _ => internal_error(__FILE__, __LINE__, "STORECON expected word or double") + }; + match (res) { + MemValue(true) => { X(rd) = zero_extend(0b0); cancel_reservation(); RETIRE_SUCCESS }, + MemValue(false) => { X(rd) = zero_extend(0b1); cancel_reservation(); RETIRE_SUCCESS }, + MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL } } } } @@ -181,9 +174,6 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = { } } } - } else { - handle_illegal(); - RETIRE_FAIL } } } @@ -206,87 +196,85 @@ mapping encdec_amoop : amoop <-> bits(5) = { AMOMAXU <-> 0b11100 } -mapping clause encdec = AMO(op, aq, rl, rs2, rs1, size, rd) if amo_width_valid(size) - <-> encdec_amoop(op) @ bool_bits(aq) @ bool_bits(rl) @ rs2 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 if amo_width_valid(size) +mapping clause encdec = AMO(op, aq, rl, rs2, rs1, size, rd) if haveAtomics() & amo_width_valid(size) + <-> encdec_amoop(op) @ bool_bits(aq) @ bool_bits(rl) @ rs2 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 if haveAtomics() & amo_width_valid(size) /* NOTE: Currently, we only EA if address translation is successful. This may need revisiting. */ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = { - if haveAtomics() then { - /* Get the address, X(rs1) (no offset). - * Some extensions perform additional checks on address validity. - */ - match ext_data_get_addr(rs1, zeros(), ReadWrite(Data, Data), width) { - Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, - Ext_DataAddr_OK(vaddr) => { - match translateAddr(vaddr, ReadWrite(Data, Data)) { - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, - TR_Address(addr, _) => { - let eares : MemoryOpResult(unit) = match (width, sizeof(xlen)) { - (BYTE, _) => mem_write_ea(addr, 1, aq & rl, rl, true), - (HALF, _) => mem_write_ea(addr, 2, aq & rl, rl, true), - (WORD, _) => mem_write_ea(addr, 4, aq & rl, rl, true), - (DOUBLE, 64) => mem_write_ea(addr, 8, aq & rl, rl, true), - _ => internal_error(__FILE__, __LINE__, "Unexpected AMO width") - }; - let is_unsigned : bool = match op { - AMOMINU => true, - AMOMAXU => true, - _ => false - }; - let rs2_val : xlenbits = match width { - BYTE => if is_unsigned then zero_extend(X(rs2)[7..0]) else sign_extend(X(rs2)[7..0]), - HALF => if is_unsigned then zero_extend(X(rs2)[15..0]) else sign_extend(X(rs2)[15..0]), - WORD => if is_unsigned then zero_extend(X(rs2)[31..0]) else sign_extend(X(rs2)[31..0]), - DOUBLE => X(rs2) - }; - match (eares) { - MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, - MemValue(_) => { - let mval : MemoryOpResult(xlenbits) = match (width, sizeof(xlen)) { - (BYTE, _) => extend_value(is_unsigned, mem_read(ReadWrite(Data, Data), addr, 1, aq, aq & rl, true)), - (HALF, _) => extend_value(is_unsigned, mem_read(ReadWrite(Data, Data), addr, 2, aq, aq & rl, true)), - (WORD, _) => extend_value(is_unsigned, mem_read(ReadWrite(Data, Data), addr, 4, aq, aq & rl, true)), - (DOUBLE, 64) => extend_value(is_unsigned, mem_read(ReadWrite(Data, Data), addr, 8, aq, aq & rl, true)), - _ => internal_error(__FILE__, __LINE__, "Unexpected AMO width") - }; - match (mval) { - MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, - MemValue(loaded) => { - let result : xlenbits = - match op { - AMOSWAP => rs2_val, - AMOADD => rs2_val + loaded, - AMOXOR => rs2_val ^ loaded, - AMOAND => rs2_val & loaded, - AMOOR => rs2_val | loaded, + /* Get the address, X(rs1) (no offset). + * Some extensions perform additional checks on address validity. + */ + match ext_data_get_addr(rs1, zeros(), ReadWrite(Data, Data), width) { + Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, + Ext_DataAddr_OK(vaddr) => { + match translateAddr(vaddr, ReadWrite(Data, Data)) { + TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, + TR_Address(addr, _) => { + let eares : MemoryOpResult(unit) = match (width, sizeof(xlen)) { + (BYTE, _) => mem_write_ea(addr, 1, aq & rl, rl, true), + (HALF, _) => mem_write_ea(addr, 2, aq & rl, rl, true), + (WORD, _) => mem_write_ea(addr, 4, aq & rl, rl, true), + (DOUBLE, 64) => mem_write_ea(addr, 8, aq & rl, rl, true), + _ => internal_error(__FILE__, __LINE__, "Unexpected AMO width") + }; + let is_unsigned : bool = match op { + AMOMINU => true, + AMOMAXU => true, + _ => false + }; + let rs2_val : xlenbits = match width { + BYTE => if is_unsigned then zero_extend(X(rs2)[7..0]) else sign_extend(X(rs2)[7..0]), + HALF => if is_unsigned then zero_extend(X(rs2)[15..0]) else sign_extend(X(rs2)[15..0]), + WORD => if is_unsigned then zero_extend(X(rs2)[31..0]) else sign_extend(X(rs2)[31..0]), + DOUBLE => X(rs2) + }; + match (eares) { + MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, + MemValue(_) => { + let mval : MemoryOpResult(xlenbits) = match (width, sizeof(xlen)) { + (BYTE, _) => extend_value(is_unsigned, mem_read(ReadWrite(Data, Data), addr, 1, aq, aq & rl, true)), + (HALF, _) => extend_value(is_unsigned, mem_read(ReadWrite(Data, Data), addr, 2, aq, aq & rl, true)), + (WORD, _) => extend_value(is_unsigned, mem_read(ReadWrite(Data, Data), addr, 4, aq, aq & rl, true)), + (DOUBLE, 64) => extend_value(is_unsigned, mem_read(ReadWrite(Data, Data), addr, 8, aq, aq & rl, true)), + _ => internal_error(__FILE__, __LINE__, "Unexpected AMO width") + }; + match (mval) { + MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, + MemValue(loaded) => { + let result : xlenbits = + match op { + AMOSWAP => rs2_val, + AMOADD => rs2_val + loaded, + AMOXOR => rs2_val ^ loaded, + AMOAND => rs2_val & loaded, + AMOOR => rs2_val | loaded, - /* These operations convert bitvectors to integer values using [un]signed, - * and back using to_bits(). - */ - AMOMIN => to_bits(sizeof(xlen), min(signed(rs2_val), signed(loaded))), - AMOMAX => to_bits(sizeof(xlen), max(signed(rs2_val), signed(loaded))), - AMOMINU => to_bits(sizeof(xlen), min(unsigned(rs2_val), unsigned(loaded))), - AMOMAXU => to_bits(sizeof(xlen), max(unsigned(rs2_val), unsigned(loaded))) - }; - let rval : xlenbits = match width { - BYTE => sign_extend(loaded[7..0]), - HALF => sign_extend(loaded[15..0]), - WORD => sign_extend(loaded[31..0]), - DOUBLE => loaded + /* These operations convert bitvectors to integer values using [un]signed, + * and back using to_bits(). + */ + AMOMIN => to_bits(sizeof(xlen), min(signed(rs2_val), signed(loaded))), + AMOMAX => to_bits(sizeof(xlen), max(signed(rs2_val), signed(loaded))), + AMOMINU => to_bits(sizeof(xlen), min(unsigned(rs2_val), unsigned(loaded))), + AMOMAXU => to_bits(sizeof(xlen), max(unsigned(rs2_val), unsigned(loaded))) }; - let wval : MemoryOpResult(bool) = match (width, sizeof(xlen)) { - (BYTE, _) => mem_write_value(addr, 1, result[7..0], aq & rl, rl, true), - (HALF, _) => mem_write_value(addr, 2, result[15..0], aq & rl, rl, true), - (WORD, _) => mem_write_value(addr, 4, result[31..0], aq & rl, rl, true), - (DOUBLE, 64) => mem_write_value(addr, 8, result, aq & rl, rl, true), - _ => internal_error(__FILE__, __LINE__, "Unexpected AMO width") - }; - match (wval) { - MemValue(true) => { X(rd) = rval; RETIRE_SUCCESS }, - MemValue(false) => { internal_error(__FILE__, __LINE__, "AMO got false from mem_write_value") }, - MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL } - } + let rval : xlenbits = match width { + BYTE => sign_extend(loaded[7..0]), + HALF => sign_extend(loaded[15..0]), + WORD => sign_extend(loaded[31..0]), + DOUBLE => loaded + }; + let wval : MemoryOpResult(bool) = match (width, sizeof(xlen)) { + (BYTE, _) => mem_write_value(addr, 1, result[7..0], aq & rl, rl, true), + (HALF, _) => mem_write_value(addr, 2, result[15..0], aq & rl, rl, true), + (WORD, _) => mem_write_value(addr, 4, result[31..0], aq & rl, rl, true), + (DOUBLE, 64) => mem_write_value(addr, 8, result, aq & rl, rl, true), + _ => internal_error(__FILE__, __LINE__, "Unexpected AMO width") + }; + match (wval) { + MemValue(true) => { X(rd) = rval; RETIRE_SUCCESS }, + MemValue(false) => { internal_error(__FILE__, __LINE__, "AMO got false from mem_write_value") }, + MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL } } } } @@ -295,9 +283,6 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = { } } } - } else { - handle_illegal(); - RETIRE_FAIL } } diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail index 9c4630b..25891c9 100644 --- a/model/riscv_insts_base.sail +++ b/model/riscv_insts_base.sail @@ -544,9 +544,6 @@ function effective_fence_set(set : bits(4), fiom : bool) -> bits(4) = { } else set } -/* For future versions of Sail where barriers can be parameterised */ -$ifdef FEATURE_UNION_BARRIER - function clause execute (FENCE(pred, succ)) = { // If the FIOM bit in menvcfg/senvcfg is set then the I/O bits can imply R/W. let fiom = is_fiom_active(); @@ -554,15 +551,15 @@ function clause execute (FENCE(pred, succ)) = { let succ = effective_fence_set(succ, fiom); match (pred, succ) { - (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_rw_rw()), - (_ : bits(2) @ 0b10, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_r_rw()), - (_ : bits(2) @ 0b10, _ : bits(2) @ 0b10) => __barrier(Barrier_RISCV_r_r()), - (_ : bits(2) @ 0b11, _ : bits(2) @ 0b01) => __barrier(Barrier_RISCV_rw_w()), - (_ : bits(2) @ 0b01, _ : bits(2) @ 0b01) => __barrier(Barrier_RISCV_w_w()), - (_ : bits(2) @ 0b01, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_w_rw()), - (_ : bits(2) @ 0b11, _ : bits(2) @ 0b10) => __barrier(Barrier_RISCV_rw_r()), - (_ : bits(2) @ 0b10, _ : bits(2) @ 0b01) => __barrier(Barrier_RISCV_r_w()), - (_ : bits(2) @ 0b01, _ : bits(2) @ 0b10) => __barrier(Barrier_RISCV_w_r()), + (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => sail_barrier(Barrier_RISCV_rw_rw), + (_ : bits(2) @ 0b10, _ : bits(2) @ 0b11) => sail_barrier(Barrier_RISCV_r_rw), + (_ : bits(2) @ 0b10, _ : bits(2) @ 0b10) => sail_barrier(Barrier_RISCV_r_r), + (_ : bits(2) @ 0b11, _ : bits(2) @ 0b01) => sail_barrier(Barrier_RISCV_rw_w), + (_ : bits(2) @ 0b01, _ : bits(2) @ 0b01) => sail_barrier(Barrier_RISCV_w_w), + (_ : bits(2) @ 0b01, _ : bits(2) @ 0b11) => sail_barrier(Barrier_RISCV_w_rw), + (_ : bits(2) @ 0b11, _ : bits(2) @ 0b10) => sail_barrier(Barrier_RISCV_rw_r), + (_ : bits(2) @ 0b10, _ : bits(2) @ 0b01) => sail_barrier(Barrier_RISCV_r_w), + (_ : bits(2) @ 0b01, _ : bits(2) @ 0b10) => sail_barrier(Barrier_RISCV_w_r), (_ : bits(4) , _ : bits(2) @ 0b00) => (), (_ : bits(2) @ 0b00, _ : bits(4) ) => (), @@ -573,36 +570,6 @@ function clause execute (FENCE(pred, succ)) = { RETIRE_SUCCESS } -$else - -function clause execute (FENCE(pred, succ)) = { - // If the FIOM bit in menvcfg/senvcfg is set then the I/O bits can imply R/W. - let fiom = is_fiom_active(); - let pred = effective_fence_set(pred, fiom); - let succ = effective_fence_set(succ, fiom); - - match (pred, succ) { - (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_rw_rw), - (_ : bits(2) @ 0b10, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_r_rw), - (_ : bits(2) @ 0b10, _ : bits(2) @ 0b10) => __barrier(Barrier_RISCV_r_r), - (_ : bits(2) @ 0b11, _ : bits(2) @ 0b01) => __barrier(Barrier_RISCV_rw_w), - (_ : bits(2) @ 0b01, _ : bits(2) @ 0b01) => __barrier(Barrier_RISCV_w_w), - (_ : bits(2) @ 0b01, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_w_rw), - (_ : bits(2) @ 0b11, _ : bits(2) @ 0b10) => __barrier(Barrier_RISCV_rw_r), - (_ : bits(2) @ 0b10, _ : bits(2) @ 0b01) => __barrier(Barrier_RISCV_r_w), - (_ : bits(2) @ 0b01, _ : bits(2) @ 0b10) => __barrier(Barrier_RISCV_w_r), - - (_ : bits(4) , _ : bits(2) @ 0b00) => (), - (_ : bits(2) @ 0b00, _ : bits(4) ) => (), - - _ => { print("FIXME: unsupported fence"); - () } - }; - RETIRE_SUCCESS -} - -$endif - mapping bit_maybe_r : bits(1) <-> string = { 0b1 <-> "r", 0b0 <-> "" @@ -636,24 +603,9 @@ union clause ast = FENCE_TSO : (bits(4), bits(4)) mapping clause encdec = FENCE_TSO(pred, succ) <-> 0b1000 @ pred @ succ @ 0b00000 @ 0b000 @ 0b00000 @ 0b0001111 -$ifdef FEATURE_UNION_BARRIER - -function clause execute (FENCE_TSO(pred, succ)) = { - match (pred, succ) { - (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_tso()), - (_ : bits(2) @ 0b00, _ : bits(2) @ 0b00) => (), - - _ => { print("FIXME: unsupported fence"); - () } - }; - RETIRE_SUCCESS -} - -$else - function clause execute (FENCE_TSO(pred, succ)) = { match (pred, succ) { - (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_tso), + (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => sail_barrier(Barrier_RISCV_tso), (_ : bits(2) @ 0b00, _ : bits(2) @ 0b00) => (), _ => { print("FIXME: unsupported fence"); @@ -662,8 +614,6 @@ function clause execute (FENCE_TSO(pred, succ)) = { RETIRE_SUCCESS } -$endif - mapping clause assembly = FENCE_TSO(pred, succ) <-> "fence.tso" ^ spc() ^ fence_bits(pred) ^ sep() ^ fence_bits(succ) diff --git a/model/riscv_insts_mext.sail b/model/riscv_insts_mext.sail index 6bf94ee..cfac3bb 100644 --- a/model/riscv_insts_mext.sail +++ b/model/riscv_insts_mext.sail @@ -20,25 +20,20 @@ mapping encdec_mul_op : mul_op <-> bits(3) = { struct { high = true, signed_rs1 = false, signed_rs2 = false } <-> 0b011 } -mapping clause encdec = MUL(rs2, rs1, rd, mul_op) - <-> 0b0000001 @ rs2 @ rs1 @ encdec_mul_op(mul_op) @ rd @ 0b0110011 +mapping clause encdec = MUL(rs2, rs1, rd, mul_op) if haveMulDiv() | haveZmmul() + <-> 0b0000001 @ rs2 @ rs1 @ encdec_mul_op(mul_op) @ rd @ 0b0110011 if haveMulDiv() | haveZmmul() function clause execute (MUL(rs2, rs1, rd, mul_op)) = { - if haveMulDiv() | haveZmmul() then { - let rs1_val = X(rs1); - let rs2_val = X(rs2); - let rs1_int : int = if mul_op.signed_rs1 then signed(rs1_val) else unsigned(rs1_val); - let rs2_int : int = if mul_op.signed_rs2 then signed(rs2_val) else unsigned(rs2_val); - let result_wide = to_bits(2 * sizeof(xlen), rs1_int * rs2_int); - let result = if mul_op.high - then result_wide[(2 * sizeof(xlen) - 1) .. sizeof(xlen)] - else result_wide[(sizeof(xlen) - 1) .. 0]; - X(rd) = result; - RETIRE_SUCCESS - } else { - handle_illegal(); - RETIRE_FAIL - } + let rs1_val = X(rs1); + let rs2_val = X(rs2); + let rs1_int : int = if mul_op.signed_rs1 then signed(rs1_val) else unsigned(rs1_val); + let rs2_int : int = if mul_op.signed_rs2 then signed(rs2_val) else unsigned(rs2_val); + let result_wide = to_bits(2 * sizeof(xlen), rs1_int * rs2_int); + let result = if mul_op.high + then result_wide[(2 * sizeof(xlen) - 1) .. sizeof(xlen)] + else result_wide[(sizeof(xlen) - 1) .. 0]; + X(rd) = result; + RETIRE_SUCCESS } mapping mul_mnemonic : mul_op <-> string = { @@ -54,24 +49,19 @@ mapping clause assembly = MUL(rs2, rs1, rd, mul_op) /* ****************************************************************** */ union clause ast = DIV : (regidx, regidx, regidx, bool) -mapping clause encdec = DIV(rs2, rs1, rd, s) - <-> 0b0000001 @ rs2 @ rs1 @ 0b10 @ bool_not_bits(s) @ rd @ 0b0110011 +mapping clause encdec = DIV(rs2, rs1, rd, s) if haveMulDiv() + <-> 0b0000001 @ rs2 @ rs1 @ 0b10 @ bool_not_bits(s) @ rd @ 0b0110011 if haveMulDiv() function clause execute (DIV(rs2, rs1, rd, s)) = { - if haveMulDiv() then { - let rs1_val = X(rs1); - let rs2_val = X(rs2); - let rs1_int : int = if s then signed(rs1_val) else unsigned(rs1_val); - let rs2_int : int = if s then signed(rs2_val) else unsigned(rs2_val); - let q : int = if rs2_int == 0 then -1 else quot_round_zero(rs1_int, rs2_int); - /* check for signed overflow */ - let q': int = if s & q > xlen_max_signed then xlen_min_signed else q; - X(rd) = to_bits(sizeof(xlen), q'); - RETIRE_SUCCESS - } else { - handle_illegal(); - RETIRE_FAIL - } + let rs1_val = X(rs1); + let rs2_val = X(rs2); + let rs1_int : int = if s then signed(rs1_val) else unsigned(rs1_val); + let rs2_int : int = if s then signed(rs2_val) else unsigned(rs2_val); + let q : int = if rs2_int == 0 then -1 else quot_round_zero(rs1_int, rs2_int); + /* check for signed overflow */ + let q': int = if s & q > xlen_max_signed then xlen_min_signed else q; + X(rd) = to_bits(sizeof(xlen), q'); + RETIRE_SUCCESS } mapping maybe_not_u : bool <-> string = { @@ -85,23 +75,18 @@ mapping clause assembly = DIV(rs2, rs1, rd, s) /* ****************************************************************** */ union clause ast = REM : (regidx, regidx, regidx, bool) -mapping clause encdec = REM(rs2, rs1, rd, s) - <-> 0b0000001 @ rs2 @ rs1 @ 0b11 @ bool_not_bits(s) @ rd @ 0b0110011 +mapping clause encdec = REM(rs2, rs1, rd, s) if haveMulDiv() + <-> 0b0000001 @ rs2 @ rs1 @ 0b11 @ bool_not_bits(s) @ rd @ 0b0110011 if haveMulDiv() function clause execute (REM(rs2, rs1, rd, s)) = { - if haveMulDiv() then { - let rs1_val = X(rs1); - let rs2_val = X(rs2); - let rs1_int : int = if s then signed(rs1_val) else unsigned(rs1_val); - let rs2_int : int = if s then signed(rs2_val) else unsigned(rs2_val); - let r : int = if rs2_int == 0 then rs1_int else rem_round_zero(rs1_int, rs2_int); - /* signed overflow case returns zero naturally as required due to -1 divisor */ - X(rd) = to_bits(sizeof(xlen), r); - RETIRE_SUCCESS - } else { - handle_illegal(); - RETIRE_FAIL - } + let rs1_val = X(rs1); + let rs2_val = X(rs2); + let rs1_int : int = if s then signed(rs1_val) else unsigned(rs1_val); + let rs2_int : int = if s then signed(rs2_val) else unsigned(rs2_val); + let r : int = if rs2_int == 0 then rs1_int else rem_round_zero(rs1_int, rs2_int); + /* signed overflow case returns zero naturally as required due to -1 divisor */ + X(rd) = to_bits(sizeof(xlen), r); + RETIRE_SUCCESS } mapping clause assembly = REM(rs2, rs1, rd, s) @@ -111,25 +96,20 @@ mapping clause assembly = REM(rs2, rs1, rd, s) union clause ast = MULW : (regidx, regidx, regidx) mapping clause encdec = MULW(rs2, rs1, rd) - if sizeof(xlen) == 64 + if sizeof(xlen) == 64 & (haveMulDiv() | haveZmmul()) <-> 0b0000001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0111011 - if sizeof(xlen) == 64 + if sizeof(xlen) == 64 & (haveMulDiv() | haveZmmul()) function clause execute (MULW(rs2, rs1, rd)) = { - if haveMulDiv() | haveZmmul() then { - let rs1_val = X(rs1)[31..0]; - let rs2_val = X(rs2)[31..0]; - let rs1_int : int = signed(rs1_val); - let rs2_int : int = signed(rs2_val); - /* to_bits requires expansion to 64 bits followed by truncation */ - let result32 = to_bits(64, rs1_int * rs2_int)[31..0]; - let result : xlenbits = sign_extend(result32); - X(rd) = result; - RETIRE_SUCCESS - } else { - handle_illegal(); - RETIRE_FAIL - } + let rs1_val = X(rs1)[31..0]; + let rs2_val = X(rs2)[31..0]; + let rs1_int : int = signed(rs1_val); + let rs2_int : int = signed(rs2_val); + /* to_bits requires expansion to 64 bits followed by truncation */ + let result32 = to_bits(64, rs1_int * rs2_int)[31..0]; + let result : xlenbits = sign_extend(result32); + X(rd) = result; + RETIRE_SUCCESS } mapping clause assembly = MULW(rs2, rs1, rd) @@ -141,25 +121,20 @@ mapping clause assembly = MULW(rs2, rs1, rd) union clause ast = DIVW : (regidx, regidx, regidx, bool) mapping clause encdec = DIVW(rs2, rs1, rd, s) - if sizeof(xlen) == 64 + if sizeof(xlen) == 64 & haveMulDiv() <-> 0b0000001 @ rs2 @ rs1 @ 0b10 @ bool_not_bits(s) @ rd @ 0b0111011 - if sizeof(xlen) == 64 + if sizeof(xlen) == 64 & haveMulDiv() function clause execute (DIVW(rs2, rs1, rd, s)) = { - if haveMulDiv() then { - let rs1_val = X(rs1)[31..0]; - let rs2_val = X(rs2)[31..0]; - let rs1_int : int = if s then signed(rs1_val) else unsigned(rs1_val); - let rs2_int : int = if s then signed(rs2_val) else unsigned(rs2_val); - let q : int = if rs2_int == 0 then -1 else quot_round_zero(rs1_int, rs2_int); - /* check for signed overflow */ - let q': int = if s & q > (2 ^ 31 - 1) then (0 - 2^31) else q; - X(rd) = sign_extend(to_bits(32, q')); - RETIRE_SUCCESS - } else { - handle_illegal(); - RETIRE_FAIL - } + let rs1_val = X(rs1)[31..0]; + let rs2_val = X(rs2)[31..0]; + let rs1_int : int = if s then signed(rs1_val) else unsigned(rs1_val); + let rs2_int : int = if s then signed(rs2_val) else unsigned(rs2_val); + let q : int = if rs2_int == 0 then -1 else quot_round_zero(rs1_int, rs2_int); + /* check for signed overflow */ + let q': int = if s & q > (2 ^ 31 - 1) then (0 - 2^31) else q; + X(rd) = sign_extend(to_bits(32, q')); + RETIRE_SUCCESS } mapping clause assembly = DIVW(rs2, rs1, rd, s) @@ -171,24 +146,19 @@ mapping clause assembly = DIVW(rs2, rs1, rd, s) union clause ast = REMW : (regidx, regidx, regidx, bool) mapping clause encdec = REMW(rs2, rs1, rd, s) - if sizeof(xlen) == 64 + if sizeof(xlen) == 64 & haveMulDiv() <-> 0b0000001 @ rs2 @ rs1 @ 0b11 @ bool_not_bits(s) @ rd @ 0b0111011 - if sizeof(xlen) == 64 + if sizeof(xlen) == 64 & haveMulDiv() function clause execute (REMW(rs2, rs1, rd, s)) = { - if haveMulDiv() then { - let rs1_val = X(rs1)[31..0]; - let rs2_val = X(rs2)[31..0]; - let rs1_int : int = if s then signed(rs1_val) else unsigned(rs1_val); - let rs2_int : int = if s then signed(rs2_val) else unsigned(rs2_val); - let r : int = if rs2_int == 0 then rs1_int else rem_round_zero(rs1_int, rs2_int); - /* signed overflow case returns zero naturally as required due to -1 divisor */ - X(rd) = sign_extend(to_bits(32, r)); - RETIRE_SUCCESS - } else { - handle_illegal(); - RETIRE_FAIL - } + let rs1_val = X(rs1)[31..0]; + let rs2_val = X(rs2)[31..0]; + let rs1_int : int = if s then signed(rs1_val) else unsigned(rs1_val); + let rs2_int : int = if s then signed(rs2_val) else unsigned(rs2_val); + let r : int = if rs2_int == 0 then rs1_int else rem_round_zero(rs1_int, rs2_int); + /* signed overflow case returns zero naturally as required due to -1 divisor */ + X(rd) = sign_extend(to_bits(32, r)); + RETIRE_SUCCESS } mapping clause assembly = REMW(rs2, rs1, rd, s) diff --git a/model/riscv_insts_vext_vset.sail b/model/riscv_insts_vext_vset.sail index 000b2f3..40a7ea9 100644 --- a/model/riscv_insts_vext_vset.sail +++ b/model/riscv_insts_vext_vset.sail @@ -41,7 +41,7 @@ mapping maybe_ma_flag : string <-> bits(1) = { sep() ^ "mu" <-> 0b0 } -val handle_illegal_vtype : unit -> unit effect {rreg} +val handle_illegal_vtype : unit -> unit function handle_illegal_vtype() = { /* Note: Implementations can set vill or trap if the vtype setting is not supported. * TODO: configuration support for both solutions diff --git a/model/riscv_pc_access.sail b/model/riscv_pc_access.sail index d3e54e5..a17e86d 100644 --- a/model/riscv_pc_access.sail +++ b/model/riscv_pc_access.sail @@ -22,6 +22,7 @@ function get_next_pc() = nextPC val set_next_pc : xlenbits -> unit function set_next_pc(pc) = { + sail_branch_announce(sizeof(xlen), pc); nextPC = pc } diff --git a/model/riscv_step.sail b/model/riscv_step.sail index 012f63b..69d2b8c 100644 --- a/model/riscv_step.sail +++ b/model/riscv_step.sail @@ -47,6 +47,7 @@ function step(step_no : int) -> bool = { }, /* non-error cases: */ F_RVC(h) => { + sail_instr_announce(h); instbits = zero_extend(h); let ast = ext_decode_compressed(h); if get_config_print_instr() @@ -63,6 +64,7 @@ function step(step_no : int) -> bool = { } }, F_Base(w) => { + sail_instr_announce(w); instbits = zero_extend(w); let ast = ext_decode(w); if get_config_print_instr() @@ -96,7 +98,10 @@ function loop () : unit -> unit = { step_no : int = 0; while not(htif_done) do { let stepped = step(step_no); - if stepped then step_no = step_no + 1; + if stepped then { + step_no = step_no + 1; + sail_end_cycle() + }; /* check htif exit */ if htif_done then { diff --git a/model/riscv_vmem.sail b/model/riscv_vmem.sail index 2d1e5d1..6e29007 100644 --- a/model/riscv_vmem.sail +++ b/model/riscv_vmem.sail @@ -107,7 +107,7 @@ function pt_walk(sv_params, let mem_result = mem_read_priv(Read(Data), // AccessType Supervisor, // Privilege pte_phys_addr, - 8, // atom (8) + 2 ^ sv_params.log_pte_size_bytes, false, // aq false, // rl false); // res @@ -115,6 +115,9 @@ function pt_walk(sv_params, match mem_result { MemException(_) => PTW_Failure(PTW_Access(), ext_ptw), MemValue(pte) => { + // Extend to 64 bits even on RV32 for simplicity. + let pte : bits(64) = zero_extend(pte); + let pte_flags = Mk_PTE_Flags(pte[7 .. 0]); if pte_is_invalid(pte_flags) then PTW_Failure(PTW_Invalid_PTE(), ext_ptw) @@ -259,6 +262,16 @@ function translationMode(priv : Privilege) -> SATPMode = { // **************************************************************** // VA to PA translation +// Write a Page Table Entry. Currently PTEs are passed around as 64 bits, even +// for Sv32 where they are actually 32 bits. `pte_size` is used to indicate +// the actual size in bytes that we want to write. +function write_pte forall 'n, 'n in {4, 8} . ( + paddr : xlenbits, + pte_size : int('n), + pte : bits(64), +) -> MemoryOpResult(bool) = + mem_write_value_priv(paddr, pte_size, pte[pte_size * 8 - 1 .. 0], Supervisor, false, false, false) + // Result of address translation // PUBLIC @@ -304,14 +317,8 @@ function translate_TLB_hit(sv_params : SV_Params, let n_ent = {ent with pte=pte'}; write_TLB(tlb_index, n_ent); let pte_phys_addr = ent.pteAddr[(sizeof(xlen) - 1) .. 0]; - let mv = mem_write_value_priv(pte_phys_addr, - 8, - pte', - Supervisor, - false, - false, - false); - match mv { + + match write_pte(pte_phys_addr, 2 ^ sv_params.log_pte_size_bytes, pte') { MemValue(_) => (), MemException(e) => internal_error(__FILE__, __LINE__, "invalid physical address in TLB") @@ -356,14 +363,8 @@ function translate_TLB_miss(sv_params : SV_Params, else { // Writeback the PTE (which has new A/D bits) let pte_phys_addr = pteAddr[(sizeof(xlen) - 1) .. 0]; - let mv = mem_write_value_priv(pte_phys_addr, // pteAddr, - 8, - pte', - Supervisor, - false, - false, - false); - match mv { + + match write_pte(pte_phys_addr, 2 ^ sv_params.log_pte_size_bytes, pte') { MemValue(_) => { add_to_TLB(asid, vAddr, pAddr, pte', pteAddr, level, global, sv_params.vpn_size_bits, |