diff --git a/Makefile b/Makefile index 4f3b63af5..18c1326be 100644 --- a/Makefile +++ b/Makefile @@ -83,14 +83,13 @@ SAIL_SYS_SRCS += riscv_sys_control.sail # general exception handling # SAIL_RV32_VM_SRCS = riscv_vmem_sv32.sail riscv_vmem_rv32.sail # SAIL_RV64_VM_SRCS = riscv_vmem_sv39.sail riscv_vmem_sv48.sail riscv_vmem_rv64.sail -# SAIL_VM_SRCS = riscv_pte.sail riscv_ptw.sail riscv_vmem_common.sail riscv_vmem_tlb.sail +# SAIL_VM_SRCS = riscv_pte.sail riscv_ptw.sail riscv_vmem_tlb.sail # ifeq ($(ARCH),RV32) # SAIL_VM_SRCS += $(SAIL_RV32_VM_SRCS) # else # SAIL_VM_SRCS += $(SAIL_RV64_VM_SRCS) # endif -SAIL_VM_SRCS += riscv_vmem_common.sail SAIL_VM_SRCS += riscv_vmem_pte.sail SAIL_VM_SRCS += riscv_vmem_ptw.sail SAIL_VM_SRCS += riscv_vmem_tlb.sail diff --git a/doc/ReadingGuide.md b/doc/ReadingGuide.md index bf647932e..34819b620 100644 --- a/doc/ReadingGuide.md +++ b/doc/ReadingGuide.md @@ -77,8 +77,7 @@ such as the platform memory map. are used in the weak memory concurrency model. - The `riscv_vmem_*.sail` files describe the S-mode address - translation. `riscv_vmem_types` and `riscv_vmem_common.sail` - contain the definitions and processing of the page-table entries and + translation. `riscv_vmem_types` contains the definitions and processing of the page-table entries and their various permission and status bits. `riscv_types_ext`, `riscv_vmem_sv32.sail`, `riscv_vmem_sv39.sail`, and `riscv_vmem_sv48.sail` contain the specifications for the diff --git a/doc/notes_Virtual_Memory.adoc b/doc/notes_Virtual_Memory.adoc index fba39a1e9..d0a6353da 100644 --- a/doc/notes_Virtual_Memory.adoc +++ b/doc/notes_Virtual_Memory.adoc @@ -15,15 +15,11 @@ vmem specification code is in file: Additional files: - model/riscv_vmem_common.sail model/riscv_vmem_pte.sail model/riscv_vmem_ptw.sail model/riscv_vmem_tlb.sail model/riscv_vmem_types.sail -`riscv_vmem_common.sail` contains the parameterization for Sv32, Sv39, -Sv48 and Sv57. - `riscv_vmem_pte.sail` describes Page Table Entries, checks for permission bits, etc. diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail index 1510dd425..7871fd019 100644 --- a/model/riscv_insts_base.sail +++ b/model/riscv_insts_base.sail @@ -708,8 +708,11 @@ mapping clause encdec = SFENCE_VMA(rs1, rs2) <-> 0b0001001 @ rs2 @ rs1 @ 0b000 @ 0b00000 @ 0b1110011 function clause execute SFENCE_VMA(rs1, rs2) = { - let addr : option(xlenbits) = if rs1 == 0b00000 then None() else Some(X(rs1)); - let asid : option(xlenbits) = if rs2 == 0b00000 then None() else Some(X(rs2)); + let addr = if rs1 != zreg then Some(X(rs1)) else None(); + // Note, the Sail model does not currently support Sv32 & SXLEN=32 on RV64. + // In that case this asidlen would be incorrect because the maximum asidlen + // is 9 but we always set it to 16 for RV64. + let asid = if rs2 != zreg then Some(X(rs2)[asidlen - 1 .. 0]) else None(); match cur_privilege { User => { handle_illegal(); RETIRE_FAIL }, Supervisor => match (architecture(get_mstatus_SXL(mstatus)), mstatus[TVM]) { diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index b4fadd26b..4875b32b0 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -848,24 +848,31 @@ bitfield Satp64 : bits(64) = { PPN : 43 .. 0 } -function legalize_satp64(a : Architecture, o : bits(64), v : bits(64)) -> bits(64) = { - let s = Mk_Satp64(v); - match satp64Mode_of_bits(a, s[Mode]) { - None() => o, - Some(Sv32) => o, /* Sv32 is unsupported for now */ - Some(_) => s.bits - } -} - bitfield Satp32 : bits(32) = { Mode : 31, Asid : 30 .. 22, PPN : 21 .. 0 } -function legalize_satp32(a : Architecture, o : bits(32), v : bits(32)) -> bits(32) = { - /* all 32-bit satp modes are valid */ - v +// TODO: This currently assumes all ASID bits are implemented +// and does not legalize the asid field if asidlen is not the maximum. +function legalize_satp( + a : Architecture, + o : xlenbits, + v : xlenbits, +) -> xlenbits = { + if xlen == 32 then { + /* all 32-bit satp modes are valid */ + v + } else if xlen == 64 then { + let s = Mk_Satp64(v); + match satpMode_of_bits(a, s[Mode]) { + None() => o, + Some(_) => s.bits + } + } else { + internal_error(__FILE__, __LINE__, "Unsupported xlen" ^ dec_str(xlen)) + } } /* disabled trigger/debug module */ diff --git a/model/riscv_types.sail b/model/riscv_types.sail index 4a4de0772..618e8b307 100644 --- a/model/riscv_types.sail +++ b/model/riscv_types.sail @@ -31,6 +31,9 @@ let xlen_min_signed = 0 - 2 ^ (xlen - 1) type half = bits(16) type word = bits(32) +type pagesize_bits : Int = 12 +let pagesize_bits = sizeof(pagesize_bits) + /* register identifiers */ type regidx = bits(5) @@ -295,14 +298,15 @@ function extStatus_of_bits(e) = /* supervisor-level address translation modes */ type satp_mode = bits(4) -enum SATPMode = {Sbare, Sv32, Sv39, Sv48} +enum SATPMode = {Sbare, Sv32, Sv39, Sv48, Sv57} -function satp64Mode_of_bits(a : Architecture, m : satp_mode) -> option(SATPMode) = +function satpMode_of_bits(a : Architecture, m : satp_mode) -> option(SATPMode) = match (a, m) { (_, 0x0) => Some(Sbare), (RV32, 0x1) => Some(Sv32), (RV64, 0x8) => Some(Sv39), (RV64, 0x9) => Some(Sv48), + (RV64, 0xA) => Some(Sv57), (_, _) => None() } diff --git a/model/riscv_vmem.sail b/model/riscv_vmem.sail index 17a44c268..8ce1c1471 100644 --- a/model/riscv_vmem.sail +++ b/model/riscv_vmem.sail @@ -20,152 +20,135 @@ // However, we model a simple TLB so that // (1) we can meaningfully test SFENCE.VMA which is a no-op wihout TLBs; // (2) we can greatly speed up simulation speed -// (e.g., from 10s or minutes to few minutes for Linux boot) +// (e.g., from 10s of minutes to few minutes for Linux boot) // The TLB implementation is in a separate file: riscv_vmem_tlb.sail // The code in this file is structured and commented so you can easily // ignore TLB functionality at first reading. -// **************************************************************** -// Fields of virtual addresses - -// PRIVATE: Extract full VPN field from VA -function vpns_of_va(sv_params : SV_Params, - va : bits(64)) -> bits(64) = { - let mask : bits(64) = zero_extend(ones(sv_params.va_size_bits)); - (va & mask) >> pagesize_bits -} - -// PRIVATE: Extract VPN[level] from VA -function vpn_j_of_va(sv_params : SV_Params, - va : bits(64), - level : PTW_Level) -> bits(64) = { - let lsb : range(0,63) = pagesize_bits + level * sv_params.vpn_size_bits; - assert (lsb < xlen); - let mask : bits(64) = zero_extend(ones(sv_params.vpn_size_bits)); - ((va >> lsb) & mask) +struct PTW_Output('v : Int), is_sv_mode('v) = { + ppn : ppn_bits('v), + pte : pte_bits('v), + // Not technically correct on RV32 where physical addresses are 34 bits, + // but the model does not support this yet. + pteAddr : xlenbits, + level : level_range('v), + global : bool, } -// PRIVATE: Extract offset within page from VA -function offset_of_va(va : bits(64)) -> bits(PAGESIZE_BITS) = va[pagesize_bits - 1 .. 0] - -// Valid xlen-wide values containing virtual addrs must have upper -// bits equal to the MSB of the virtual address. -// Virtual address widths depend on the virtual memory mode. // PRIVATE -function is_valid_vAddr(struct { va_size_bits, _ } : SV_Params, - vAddr : bits(64)) -> bool = - vAddr == sign_extend(vAddr[va_size_bits - 1 .. 0]) - -// **************************************************************** -// Results of Page Table Walk (PTW) - -// PRIVATE -union PTW_Result = { - PTW_Success: (bits(64), bits(64), bits(64), nat, bool, ext_ptw), - PTW_Failure: (PTW_Error, ext_ptw) +union PTW_Result('v : Int), is_sv_mode('v) = { + PTW_Success : (PTW_Output('v), ext_ptw), + PTW_Failure : (PTW_Error, ext_ptw), } // **************************************************************** // Page Table Walk (PTW) -// Note: 'pt_walk()' is recursive => needs separate 'val' decls +// Write a Page Table Entry. +function write_pte forall 'n, 'n in {4, 8} . ( + paddr : xlenbits, + pte_size : int('n), + pte : bits('n * 8), +) -> MemoryOpResult(bool) = + mem_write_value_priv(paddr, pte_size, pte, Supervisor, false, false, false) + +// Read a Page Table Entry. +function read_pte forall 'n, 'n in {4, 8} . ( + paddr : xlenbits, + pte_size : int('n), +) -> MemoryOpResult(bits(8 * 'n)) = + mem_read_priv(Read(Data), Supervisor, paddr, pte_size, false, false, false) // PRIVATE -val pt_walk : (SV_Params, - bits(64), // virtual addr - AccessType(ext_access_type), // Read/Write/ReadWrite/Execute - Privilege, // User/Supervisor/Machine - bool, // mstatus.MXR - bool, // do_sum - bits(64), // PT base addr - PTW_Level, // tree level for this recursive call - bool, // global translation, - ext_ptw) // ext_ptw - -> PTW_Result - -function pt_walk(sv_params, - va, - ac, - priv, - mxr, - do_sum, - pt_base, - level, - global, - ext_ptw) = { - let vpn_j = vpn_j_of_va(sv_params, va, level); - let pte_offset = vpn_j << sv_params.log_pte_size_bytes; - let pte_addr = pt_base + pte_offset; - - // In Sv32, physical addrs are actually 34 bits, not XLEN(=32) bits. - // Below, 'pte_phys_addr' is XLEN bits because it's an arg to - // 'mem_read_priv()' [riscv_mem.sail] where it's declared as xlenbits. - // That def and this use need to be fixed together (TODO) - let pte_phys_addr : xlenbits = pte_addr[(xlen - 1) .. 0]; +// 'v is the virtual address size. +val pt_walk : forall 'v, is_sv_mode('v) . ( + int('v), // Sv32, Sv39, Sv48, Sv57 + bits('v - pagesize_bits), // Virtual Page Number + AccessType(ext_access_type), // Read/Write/ReadWrite/Execute + Privilege, // User/Supervisor/Machine + bool, // mstatus.MXR + bool, // do_sum + ppn_bits('v), // Base PPN (`a` in the spec). + level_range('v), // Tree level for this recursive call (`i` in the spec). + bool, // global translation, + ext_ptw // ext_ptw +) -> PTW_Result('v) + +function pt_walk( + sv_width, + vpn, + ac, + priv, + mxr, + do_sum, + pt_base, + level, + global, + ext_ptw, +) = { + // Extract the PPN component for this level; 10 bits on Sv32, otherwise 9. + let 'vpn_i_size = if 'v == 32 then 10 else 9; + let vpn_i = vpn[(level + 1) * vpn_i_size - 1 .. level * vpn_i_size]; + let 'log_pte_size_bytes = if 'v == 32 then 2 else 3; + // Address of PTE in page table. This is 34 bits for Sv32, otherwise 56 bits. + let pte_addr = pt_base @ vpn_i @ zeros('log_pte_size_bytes); + + // In Sv32, physical addrs are actually 34 bits, but the model + // currently uses XLEN physical addresses. So with Sv32 on RV32 we + // truncate 2 bits. + let pte_addr : xlenbits = if 'v == 32 & xlen == 32 then { + // Check that the above hack didn't have any effect (more or less; we + // might still run into issues close to 2^32). + assert(pte_addr[33 .. 32] == zeros()); + pte_addr[31 .. 0] + } else { + // Cannot use Sv39+ on RV32. + assert('v == 32 | xlen == 64); + zero_extend(pte_addr) + }; // Read this-level PTE from mem - let mem_result = mem_read_priv(Read(Data), // AccessType - Supervisor, // Privilege - pte_phys_addr, - 2 ^ sv_params.log_pte_size_bytes, - false, // aq - false, // rl - false); // res - - match mem_result { + match read_pte(pte_addr, 2 ^ log_pte_size_bytes) { 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 + let pte_ext = ext_bits_of_PTE(pte); + + if pte_is_invalid(pte_flags, pte_ext) then PTW_Failure(PTW_Invalid_PTE(), ext_ptw) else { - let ppns : bits(64) = PPNs_of_PTE(sv_params, pte); - let global' = global | (pte_flags[G] == 0b1); + let ppn = PPN_of_PTE(pte); // 22 or 44. + let global = global | (pte_flags[G] == 0b1); if pte_is_ptr(pte_flags) then { // Non-Leaf PTE - if level > 0 then { + if level > 0 then // follow the pointer to walk next level - let pt_base' : bits(64) = ppns << pagesize_bits; - let level' = level - 1; - pt_walk(sv_params, va, ac, priv, mxr, do_sum, - pt_base', level', global', ext_ptw) - } + pt_walk(sv_width, vpn, ac, priv, mxr, do_sum, ppn, level - 1, global, ext_ptw) else // level 0 PTE, but contains a pointer instead of a leaf PTW_Failure(PTW_Invalid_PTE(), ext_ptw) - } - else { + } else { // Leaf PTE - let ext_pte = msbs_of_PTE(sv_params, pte); let pte_check = check_PTE_permission(ac, priv, mxr, do_sum, pte_flags, - ext_pte, ext_ptw); + pte_ext, ext_ptw); match pte_check { PTE_Check_Failure(ext_ptw, ext_ptw_fail) => PTW_Failure(ext_get_ptw_error(ext_ptw_fail), ext_ptw), PTE_Check_Success(ext_ptw) => if level > 0 then { - // Superpage; construct mask for lower-level PPNs from the PTE - let mask_bits = level * sv_params.pte_PPN_j_size_bits; - // Clear the lowest `mask_bits` bits. - let ppns_masked = (ppns >> mask_bits) << mask_bits; - if not(ppns == ppns_masked) then - // misaligned superpage mapping + // Superpage. Check it is correctly aligned. + let ppn_size_bits = if 'v == 32 then 10 else 9; + let low_bits = ppn_size_bits * level; + if ppn[low_bits - 1 .. 0] != zeros() then PTW_Failure(PTW_Misaligned(), ext_ptw) else { // Compose final PA in superpage: - // Superpage PPN + lower VPNs + pagesize_bits page-offset - let mask : bits(64) = ~ (ones() << mask_bits); - let ppn = ppns | (vpns_of_va(sv_params, va) & mask); - let pa = (ppn << pagesize_bits) | zero_extend(offset_of_va(va)); - PTW_Success(pa, pte, pte_addr, level, global', ext_ptw) + // Superpage PPN @ lower VPNs @ page-offset + let ppn = ppn[length(ppn) - 1 .. low_bits] @ vpn[low_bits - 1 .. 0]; + PTW_Success(struct { ppn=ppn, pte=pte, pteAddr=pte_addr, level=level, global=global}, ext_ptw) } - } - else { - let pa = (ppns << pagesize_bits) | zero_extend(offset_of_va(va)); - PTW_Success(pa, pte, pte_addr, level, global', ext_ptw) + } else { + PTW_Success(struct { ppn=ppn, pte=pte, pteAddr=pte_addr, level=level, global=global}, ext_ptw) } } } @@ -177,32 +160,7 @@ function pt_walk(sv_params, // **************************************************************** // Architectural SATP CSR -// See riscv_sys_regs.sail for legalize_satp{32,64}(). -// WARNING: those functions legalize Mode but not ASID? -// PUBLIC: invoked from writeCSR() to fixup WARL fields -function legalize_satp(a : Architecture, - o : xlenbits, // previous value of satp - v : xlenbits) // proposed new value of satp - -> xlenbits = { // new legal value of satp - if xlen == 32 then { - // The slice and extend ops below are no-ops when xlen==32, - // but appease the type-checker when xlen==64 (when this code is not executed!) - let o32 : bits(32) = o[31 .. 0]; - let v32 : bits(32) = v[31 .. 0]; - let new_satp : bits(32) = legalize_satp32(a, o32, v32); - zero_extend(new_satp); - } else if xlen == 64 then { - // The extend and truncate ops below are no-ops when xlen==64, - // but appease the type-checker when xlen==32 (when this code is not executed!) - let o64 : bits(64) = zero_extend(o); - let v64 : bits(64) = zero_extend(v); - let new_satp : bits(64) = legalize_satp64(a, o64, v64); - truncate(new_satp, xlen) - } else - internal_error(__FILE__, __LINE__, "Unsupported xlen" ^ dec_str(xlen)) -} - -// PUBLIC +// PUBLIC: see also riscv_insts_zicsr.sail and other CSR-related files register satp : xlenbits mapping clause csr_name_map = 0x180 <-> "satp" function clause is_CSR_defined(0x180) = extensionEnabled(Ext_S) @@ -212,70 +170,49 @@ function clause write_CSR(0x180, value) = { satp = legalize_satp(cur_Architectur // ---------------- // Fields of SATP -// ASID is 9b in Sv32, 16b in Sv39/Sv48/Sv57: we use 16b for both +// ASID is 9b in Sv32, 16b in Sv39/Sv48/Sv57 // PRIVATE -function satp_to_asid(satp_val : xlenbits) -> asidbits = - if xlen == 32 then zero_extend(Mk_Satp32(satp_val)[Asid]) - else if xlen == 64 then Mk_Satp64(satp_val)[Asid] - else internal_error(__FILE__, __LINE__, - "Unsupported xlen" ^ dec_str(xlen)) +val satp_to_asid : forall 'n, 'n in {32, 64}. bits('n) -> bits(if 'n == 32 then 9 else 16) +function satp_to_asid(satp_val) = + if 'n == 32 then Mk_Satp32(satp_val)[Asid] else Mk_Satp64(satp_val)[Asid] -// Result is 64b to cover both RV32 and RV64 addrs // PRIVATE -function satp_to_PT_base(satp_val : xlenbits) -> bits(64) = { - let ppn = if xlen == 32 then zero_extend (64, Mk_Satp32(satp_val)[PPN]) - else if xlen == 64 then zero_extend (64, Mk_Satp64(satp_val)[PPN]) - else internal_error(__FILE__, __LINE__, - "Unsupported xlen" ^ dec_str(xlen)); - ppn << pagesize_bits -} +val satp_to_ppn : forall 'n, 'n in {32, 64}. bits('n) -> bits(if 'n == 32 then 22 else 44) +function satp_to_ppn(satp_val) = + if 'n == 32 then Mk_Satp32(satp_val)[PPN] else Mk_Satp64(satp_val)[PPN] // Compute address translation mode from SATP register // PRIVATE function translationMode(priv : Privilege) -> SATPMode = { - if priv == Machine then - Sbare - else if xlen == 32 then - match Mk_Satp32(satp)[Mode] { - 0b0 => Sbare, - 0b1 => Sv32 - } - else if xlen == 64 then { - // Translation mode is based on mstatus.SXL, which could be RV32 when xlen==64 + if priv == Machine then Sbare + else { let arch = architecture(get_mstatus_SXL(mstatus)); - match arch { - Some(RV64) => { let mbits : bits(4) = satp[63 .. 60]; - match satp64Mode_of_bits(RV64, mbits) { // see riscv_types.sail - Some(m) => m, - None() => internal_error(__FILE__, __LINE__, - "invalid RV64 translation mode in satp") - } - }, - Some(RV32) => match Mk_Satp32(satp[31 .. 0])[Mode] { // Note: satp is 64bits here - // When xlen is 64, mstatus.SXL (for S privilege) can be RV32 - 0b0 => Sbare, - 0b1 => Sv32 - }, - _ => internal_error(__FILE__, __LINE__, "unsupported address translation arch") + let arch : Architecture = match arch { + Some(RV32) => RV32, + Some(RV64) => RV64, + // The model does not support modifying SXL currently so this cannot happen. + _ => internal_error(__FILE__, __LINE__, "unsupported address translation arch"), + }; + let mbits : satp_mode = match arch { + RV64 => { + // Can't have an effective architecture of RV64 on RV32. + assert(xlen >= 64); + Mk_Satp64(satp)[Mode] + }, + RV32 => 0b000 @ Mk_Satp32(satp[31..0])[Mode], + _ => internal_error(__FILE__, __LINE__, "should be unreachable"), + }; + match satpMode_of_bits(arch, mbits) { + Some(m) => m, + // The model does not support modifying SXL currently so this cannot happen. + None() => internal_error(__FILE__, __LINE__, "invalid translation mode in satp") } } - else - internal_error(__FILE__, __LINE__, "unsupported xlen") } // **************************************************************** // 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 @@ -285,81 +222,83 @@ union TR_Result('paddr : Type, 'failure : Type) = { } // This function can be ignored on first reading since TLBs are not -// part of RISC-V architecture spec (see TLB_NOTE above). +// part of RISC-V architecture spec (see TLB NOTE above). // PRIVATE: translate on TLB hit, and maintenance of PTE in TLB -function translate_TLB_hit(sv_params : SV_Params, - asid : asidbits, - ptb : bits(64), - vAddr : bits(64), - ac : AccessType(ext_access_type), - priv : Privilege, - mxr : bool, - do_sum : bool, - ext_ptw : ext_ptw, - tlb_index : tlb_index_range, - ent : TLB_Entry) - -> TR_Result(bits(64), PTW_Error) = { - let pte = ent.pte; - let ext_pte = msbs_of_PTE(sv_params, pte); +function translate_TLB_hit forall 'v, is_sv_mode('v) . ( + sv_width : int('v), + asid : asidbits, + vpn : bits('v - pagesize_bits), + ac : AccessType(ext_access_type), + priv : Privilege, + mxr : bool, + do_sum : bool, + ext_ptw : ext_ptw, + tlb_index : tlb_index_range, + ent : TLB_Entry, +) -> TR_Result(ppn_bits('v), PTW_Error) = { + + let pte_width = if sv_width == 32 then 4 else 8; + let pte = tlb_get_pte(pte_width, ent); + let ext_pte = ext_bits_of_PTE(pte); let pte_flags = Mk_PTE_Flags(pte[7 .. 0]); let pte_check = check_PTE_permission(ac, priv, mxr, do_sum, pte_flags, ext_pte, ext_ptw); + match pte_check { PTE_Check_Failure(ext_ptw, ext_ptw_fail) => TR_Failure(ext_get_ptw_error(ext_ptw_fail), ext_ptw), PTE_Check_Success(ext_ptw) => - match update_PTE_Bits(sv_params, pte, ac) { - None() => TR_Address(ent.pAddr | (vAddr & ent.vAddrMask), ext_ptw), + match update_PTE_Bits(pte, ac) { + None() => TR_Address(tlb_get_ppn(sv_width, ent, vpn), ext_ptw), Some(pte') => - // See riscv_platform.sail if not(plat_enable_dirty_update()) then // pte needs dirty/accessed update but that is not enabled TR_Failure(PTW_PTE_Update(), ext_ptw) else { // Writeback the PTE (which has new A/D bits) - let n_ent = {ent with pte=pte'}; - write_TLB(tlb_index, n_ent); + write_TLB(tlb_index, tlb_set_pte(ent, pte')); let pte_phys_addr = ent.pteAddr[(xlen - 1) .. 0]; - - match write_pte(pte_phys_addr, 2 ^ sv_params.log_pte_size_bytes, pte') { + match write_pte(pte_phys_addr, pte_width, pte') { MemValue(_) => (), MemException(e) => internal_error(__FILE__, __LINE__, "invalid physical address in TLB") }; - TR_Address(ent.pAddr | (vAddr & ent.vAddrMask), ext_ptw) + TR_Address(tlb_get_ppn(sv_width, ent, vpn), ext_ptw) } } } } // PRIVATE: translate on TLB miss (do a page-table walk) -function translate_TLB_miss(sv_params : SV_Params, - asid : asidbits, - ptb : bits(64), - vAddr : bits(64), - ac : AccessType(ext_access_type), - priv : Privilege, - mxr : bool, - do_sum : bool, - ext_ptw : ext_ptw) -> TR_Result(bits(64), PTW_Error) = { - let initial_level = sv_params.levels - 1; - let ptw_result = pt_walk(sv_params, vAddr, ac, priv, mxr, do_sum, - ptb, initial_level, false, ext_ptw); +function translate_TLB_miss forall 'v, is_sv_mode('v) . ( + sv_width : int('v), + asid : asidbits, + base_ppn : ppn_bits('v), + vpn : bits('v - pagesize_bits), + ac : AccessType(ext_access_type), + priv : Privilege, + mxr : bool, + do_sum : bool, + ext_ptw : ext_ptw, +) -> TR_Result(ppn_bits('v), PTW_Error) = { + let initial_level = if 'v == 32 then 1 else (if 'v == 39 then 2 else (if 'v == 48 then 3 else 4)); + + let 'pte_width = if sv_width == 32 then 4 else 8; + let ptw_result = pt_walk(sv_width, vpn, ac, priv, mxr, do_sum, + base_ppn, initial_level, false, ext_ptw); match ptw_result { PTW_Failure(f, ext_ptw) => TR_Failure(f, ext_ptw), - PTW_Success(pAddr, pte, pteAddr, level, global, ext_ptw) => { - let ext_pte = msbs_of_PTE(sv_params, pte); + PTW_Success(struct {ppn, pte, pteAddr, level, global}, ext_ptw) => { + let ext_pte = ext_bits_of_PTE(pte); // Without TLBs, this 'match' expression can be replaced simply - // by: 'TR_Address(pAddr, ext_ptw)' (see TLB_NOTE above) - match update_PTE_Bits(sv_params, pte, ac) { + // by: 'TR_Address(ppn, ext_ptw)' (see TLB NOTE above) + match update_PTE_Bits(pte, ac) { None() => { - add_to_TLB(asid, vAddr, pAddr, pte, pteAddr, level, global, - sv_params.vpn_size_bits, - pagesize_bits); - TR_Address(pAddr, ext_ptw) + add_to_TLB(sv_width, asid, vpn, ppn, pte, pteAddr, level, global); + TR_Address(ppn, ext_ptw) }, - Some(pte') => + Some(pte) => // See riscv_platform.sail if not(plat_enable_dirty_update()) then // pte needs dirty/accessed update but that is not enabled @@ -367,13 +306,10 @@ function translate_TLB_miss(sv_params : SV_Params, else { // Writeback the PTE (which has new A/D bits) let pte_phys_addr = pteAddr[(xlen - 1) .. 0]; - - match write_pte(pte_phys_addr, 2 ^ sv_params.log_pte_size_bytes, pte') { + match write_pte(pte_phys_addr, pte_width, pte) { MemValue(_) => { - add_to_TLB(asid, vAddr, pAddr, pte', pteAddr, level, global, - sv_params.vpn_size_bits, - pagesize_bits); - TR_Address(pAddr, ext_ptw) + add_to_TLB(sv_width, asid, vpn, ppn, pte, pteAddr, level, global); + TR_Address(ppn, ext_ptw) }, MemException(e) => TR_Failure(PTW_Access(), ext_ptw) @@ -384,62 +320,98 @@ function translate_TLB_miss(sv_params : SV_Params, } } +// Mapping the SATPMode to the width integer. Note there is also SvBare +// and it's an error to call this with SvBare. +mapping satp_mode_width : SATPMode <-> {32, 39, 48, 57} = { + Sv32 <-> 32, + Sv39 <-> 39, + Sv48 <-> 48, + Sv57 <-> 57, +} + // PRIVATE -function translate(sv_params : SV_Params, - asid : asidbits, - ptb : bits(64), - vAddr : bits(64), - ac : AccessType(ext_access_type), - priv : Privilege, - mxr : bool, - do_sum : bool, - ext_ptw : ext_ptw) - -> TR_Result(bits(64), PTW_Error) = { +function translate forall 'v, is_sv_mode('v) . ( + sv_width : int('v), + asid : asidbits, + base_ppn : ppn_bits('v), + vAddr : bits('v), + ac : AccessType(ext_access_type), + priv : Privilege, + mxr : bool, + do_sum : bool, + ext_ptw : ext_ptw, +) -> TR_Result(ppn_bits('v), PTW_Error) = { // On first reading, assume lookup_TLB returns None(), since TLBs - // are not part of RISC-V archticture spec (see TLB_NOTE above) - match lookup_TLB(asid, vAddr) { - Some(index, ent) => translate_TLB_hit(sv_params, asid, ptb, vAddr, ac, priv, + // are not part of RISC-V archticture spec (see TLB NOTE above) + let vpn = vAddr['v - 1 .. pagesize_bits]; + match lookup_TLB(sv_width, asid, vAddr) { + Some(index, ent) => translate_TLB_hit(sv_width, asid, vpn, ac, priv, mxr, do_sum, ext_ptw, index, ent), - None() => translate_TLB_miss(sv_params, asid, ptb, vAddr, ac, priv, + None() => translate_TLB_miss(sv_width, asid, base_ppn, vpn, ac, priv, mxr, do_sum, ext_ptw) } } +// SATP is represented in the model as an XLEN register (xlenbits), but it's +// actually SXLEN. That means if we are using Sv39 (which is only available when +// SXLEN is 32), then it must be a 32 bit register. +function get_satp forall 'v, is_sv_mode('v). ( + sv_width : int('v) +) -> bits(if 'v == 32 then 32 else 64) = { + // Cannot use Sv39+ on RV32. + assert('v == 32 | xlen == 64); + if sv_width == 32 then satp[31 .. 0] else satp +} + // Top-level addr-translation function // PUBLIC: invoked from instr-fetch and load/store/amo function translateAddr(vAddr : xlenbits, ac : AccessType(ext_access_type)) -> TR_Result(xlenbits, ExceptionType) = { - // Internally the vmem code works with 64-bit values, whether xlen==32 or xlen==64 - // This 'extend' is a no-op when xlen==64 and extends when xlen==32 - let vAddr_64b : bits(64) = zero_extend(vAddr); // Effective privilege takes into account mstatus.PRV, mstatus.MPP // See riscv_sys_regs.sail for effectivePrivilege() and cur_privilege - let effPriv : Privilege = effectivePrivilege(ac, mstatus, cur_privilege); - let mode : SATPMode = translationMode(effPriv); - let (valid_va, sv_params) : (bool, SV_Params) = match mode { - Sbare => return TR_Address(vAddr, init_ext_ptw), - Sv32 => (true, sv32_params), - Sv39 => (is_valid_vAddr(sv39_params, vAddr_64b), sv39_params), - Sv48 => (is_valid_vAddr(sv48_params, vAddr_64b), sv48_params), - // Sv57 => (is_valid_vAddr(sv57_params, vAddr_64b), sv57_params), // TODO - }; - if not(valid_va) then + let effPriv = effectivePrivilege(ac, mstatus, cur_privilege); + + let mode = translationMode(effPriv); + + if mode == Sbare then return TR_Address(vAddr, init_ext_ptw); + + // Sv39 -> 39, etc. + let sv_width = satp_mode_width(mode); + + // For Sv32 on RV64, satp is 32 bits (SXLEN), not XLEN. + let satp_sxlen = get_satp(sv_width); + + // Cannot use Sv39+ on RV32. + assert(sv_width == 32 | xlen == 64); + + let svAddr = vAddr[sv_width - 1 .. 0]; + if vAddr != sign_extend(svAddr) then { TR_Failure(translationException(ac, PTW_Invalid_Addr()), init_ext_ptw) - else { - let mxr = mstatus[MXR] == 0b1; - let do_sum = mstatus[SUM] == 0b1; - let asid : asidbits = satp_to_asid(satp); - let ptb : bits(64) = satp_to_PT_base(satp); - let tr_result1 = translate(sv_params, - asid, - ptb, - vAddr_64b, - ac, effPriv, mxr, do_sum, - init_ext_ptw); + } else { + let mxr = mstatus[MXR] == 0b1; + let do_sum = mstatus[SUM] == 0b1; + let asid = satp_to_asid(satp_sxlen); + let base_ppn = satp_to_ppn(satp_sxlen); + let res = translate(sv_width, + zero_extend(asid), + base_ppn, + svAddr, + ac, effPriv, mxr, do_sum, + init_ext_ptw); // Fixup result PA or exception - match tr_result1 { - TR_Address(pa, ext_ptw) => TR_Address(truncate(pa, xlen), ext_ptw), + match res { + TR_Address(ppn, ext_ptw) => { + // Append the page offset. This is now a 34 or 56 bit address. + let paddr = ppn @ vAddr[pagesize_bits - 1 .. 0]; + + // On RV64 we can simply zero extend to 64 bits. + // On RV32 we have to truncate to 32 bits. + // TODO: In future we should have a physical address type in addition + // to xlenbits, and this should be 34 bits on RV32. + let paddr : xlenbits = truncate(zero_extend(64, paddr), xlen); + TR_Address(paddr, ext_ptw) + }, TR_Failure(f, ext_ptw) => TR_Failure(translationException(ac, f), ext_ptw) } } diff --git a/model/riscv_vmem_common.sail b/model/riscv_vmem_common.sail deleted file mode 100644 index a6b717b65..000000000 --- a/model/riscv_vmem_common.sail +++ /dev/null @@ -1,103 +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 */ -/*=======================================================================================*/ - -// **************************************************************** -// Parameters for VM modes sv32, sv39, sv48 and (TODO) Sv57 - -// All VM modes use the same page size (4KB, with 12-bit index) - -// This two-line idiom constrains the value (2nd line) to be a singleton, -// which helps in type-checking wherever it is used. -type PAGESIZE_BITS : Int = 12 -let pagesize_bits = sizeof(PAGESIZE_BITS) - -// PRIVATE -struct SV_Params = { - // VA - va_size_bits : {32, 39, 48}, // 32 39 48 - vpn_size_bits : {10, 9}, // 10 9 9 - - // PTE - levels : { 2, 3, 4}, // 2 3 4 - log_pte_size_bytes : { 2, 3}, // 2 3 3 - pte_msbs_lsb_index : {32, 54}, // 32 54 54 - pte_msbs_size_bits : { 0, 10}, // 0 10 10 - pte_PPNs_lsb_index : {10}, // 10 10 10 - pte_PPNs_size_bits : {22, 44}, // 22 44 44 - pte_PPN_j_size_bits : {10, 9} // 10 9 9 -} - -// Current level during a page-table walk (0 to SV_Params.levels - 1) -type PTW_Level = range(0,3) // range(0,4) when add Sv57 (TODO) - -// PRIVATE -let sv32_params : SV_Params = struct { - // VA - va_size_bits = 32, - vpn_size_bits = 10, - - // PTE - levels = 2, - log_pte_size_bytes = 2, // 4 Bytes - pte_msbs_lsb_index = 32, - pte_msbs_size_bits = 0, - pte_PPNs_lsb_index = 10, - pte_PPNs_size_bits = 22, - pte_PPN_j_size_bits = 10 -} - -// PRIVATE -let sv39_params : SV_Params = struct { - // VA - va_size_bits = 39, - vpn_size_bits = 9, - - // PTE - levels = 3, - log_pte_size_bytes = 3, // 8 Bytes - pte_msbs_lsb_index = 54, - pte_msbs_size_bits = 10, - pte_PPNs_lsb_index = 10, - pte_PPNs_size_bits = 44, - pte_PPN_j_size_bits = 9 -} - -// PRIVATE -let sv48_params : SV_Params = struct { - // VA - va_size_bits = 48, - vpn_size_bits = 9, - - // PTE - levels = 4, - log_pte_size_bytes = 3, // 8 Bytes - pte_msbs_lsb_index = 54, - pte_msbs_size_bits = 10, - pte_PPNs_lsb_index = 10, - pte_PPNs_size_bits = 44, - pte_PPN_j_size_bits = 9 -} - -// TODO; not currently used -// PRIVATE -/* -let sv57_params : SV_Params = struct { - // VA - va_size_bits = 57, - vpn_size_bits = 9, - - // PTE - levels = 5, - log_pte_size_bytes = 3, // 8 Bytes - pte_msbs_lsb_index = 54, - pte_msbs_size_bits = 10, - pte_PPNs_lsb_index = 10, - pte_PPNs_size_bits = 44, - pte_PPN_j_size_bits = 9 -} -*/ diff --git a/model/riscv_vmem_pte.sail b/model/riscv_vmem_pte.sail index 07a94a3ed..cb923f34f 100644 --- a/model/riscv_vmem_pte.sail +++ b/model/riscv_vmem_pte.sail @@ -9,30 +9,47 @@ // **************************************************************** // PTE (Page Table Entry) in PTN (Page Table Node) -// PTE MSBs PPNs RSW BITs -// Sv32 - 31..10 9..8 7..0 -// Sv39 63..54 53..10 9..8 7..0 -// Sv48 63..54 53..10 9..8 7..0 +// PTE EXT PPNs RSW FLAGS +// Sv32 - 31..10 9..8 7..0 +// Sv39/48/57 63..54 53..10 9..8 7..0 -// MSBs of PTE are reserved for RV64 extensions. -// There are not available bits on RV32, so these bits will be zeros on RV32. +// The EXT bits of PTE are only present on RV64. They are not available on RV32 +// however their default value on RV32 is not necessarily zero. type pte_flags_bits = bits(8) -// For PTW extensions (non-standard) -type extPte = bits(64) +// Reserved PTE bits could be used by extensions on RV64. There are +// no such available bits on RV32. +type pte_ext_bits = bits(10) -// PRIVATE: extract msbs of PTE above the PPN -function msbs_of_PTE(sv_params : SV_Params, pte : bits(64)) -> bits(64) = { - let mask : bits(64) = zero_extend(ones(sv_params.pte_msbs_size_bits)); - (pte >> sv_params.pte_msbs_lsb_index) & mask +bitfield PTE_Ext : pte_ext_bits = { + // NAPOT page table entry + N : 9, + // Page based memory types + PBMT : 8 .. 7, + reserved : 6 .. 0, } -// PRIVATE: extract PPNs of PTE -function PPNs_of_PTE(sv_params : SV_Params, pte : bits(64)) -> bits(64) = { - let mask : bits(64) = zero_extend(ones(sv_params.pte_PPNs_size_bits)); - (pte >> sv_params.pte_PPNs_lsb_index) & mask -} +/* + * On SV32, there are no reserved bits available to extensions. Therefore, by + * default, we initialize the PTE extension field with all zeros. However, + * extensions may wish, on SV39/48/56, to put flags in the reserved region of + * those PTEs. To avoid the need for "inhibit" bits in extensions (i.e., so + * that extensions can use the more common and more RISC-V flavored "enable" + * disposition), we allow extensions to use any constant value by overriding + * this default_sv32_ext_pte value. + */ +let default_sv32_ext_pte : pte_ext_bits = zeros() + +// PRIVATE: extract ext bits of PTE above the PPN. +val ext_bits_of_PTE : forall 'pte_size, 'pte_size in {32, 64}. bits('pte_size) -> PTE_Ext +function ext_bits_of_PTE(pte) = + Mk_PTE_Ext(if 'pte_size == 64 then pte[63 .. 54] else default_sv32_ext_pte) + +// PRIVATE: extract full PPN from a PTE +val PPN_of_PTE : forall 'pte_size, 'pte_size in {32, 64}. + bits('pte_size) -> bits(if 'pte_size == 32 then 22 else 44) +function PPN_of_PTE(pte) = if 'pte_size == 32 then pte[31 .. 10] else pte[53 .. 10] // PRIVATE: 8 LSBs of PTEs in Sv32, Sv39, Sv48 and Sv57 bitfield PTE_Flags : pte_flags_bits = { @@ -47,14 +64,25 @@ bitfield PTE_Flags : pte_flags_bits = { } // PRIVATE: check if a PTE is a pointer to next level (non-leaf) -function pte_is_ptr(pte_flags : PTE_Flags) -> bool = (pte_flags[X] == 0b0) - & (pte_flags[W] == 0b0) - & (pte_flags[R] == 0b0) +function pte_is_ptr(pte_flags : PTE_Flags) -> bool = + pte_flags[X] == 0b0 + & pte_flags[W] == 0b0 + & pte_flags[R] == 0b0 + +// These extensions are not implemented in the model yet. +function haveSvnapot() -> bool = false +function haveSvpmbt() -> bool = false // PRIVATE: check if a PTE is valid -function pte_is_invalid(pte_flags : PTE_Flags) -> bool = (pte_flags[V] == 0b0) - | ((pte_flags[W] == 0b1) - & (pte_flags[R] == 0b0)) +function pte_is_invalid(pte_flags : PTE_Flags, pte_ext : PTE_Ext) -> bool = + pte_flags[V] == 0b0 + | (pte_flags[W] == 0b1 & pte_flags[R] == 0b0) + // Note, the following requirements depend on the privileged spec version. + // Early versions do not require this check. This will need to be behind + // a flag when the Sail model allows specifying the spec version. + | (pte_ext[N] != 0b0 & not(haveSvnapot())) + | (pte_ext[PBMT] != zeros() & not(haveSvpmbt())) + | pte_ext[reserved] != zeros() // ---------------- // Check access permissions in PTE @@ -74,7 +102,7 @@ function check_PTE_permission(ac : AccessType(ext_access_type), mxr : bool, do_sum : bool, pte_flags : PTE_Flags, - ext : extPte, + ext : PTE_Ext, ext_ptw : ext_ptw) -> PTE_Check = { let pte_U = pte_flags[U]; let pte_R = pte_flags[R]; @@ -107,11 +135,11 @@ function check_PTE_permission(ac : AccessType(ext_access_type), // Update PTE bits if needed; return new PTE if updated // PRIVATE -function update_PTE_Bits(sv_params : SV_Params, - pte : bits(64), - a : AccessType(ext_access_type)) - -> option(bits(64)) = { - let pte_flags = Mk_PTE_Flags(pte [7 .. 0]); +function update_PTE_Bits forall 'pte_size, 'pte_size in {32, 64} . ( + pte : bits('pte_size), + a : AccessType(ext_access_type), +) -> option(bits('pte_size)) = { + let pte_flags = Mk_PTE_Flags(pte[7 .. 0]); // Update 'dirty' bit? let update_d : bool = (pte_flags[D] == 0b0) @@ -128,8 +156,8 @@ function update_PTE_Bits(sv_params : SV_Params, let pte_flags = [pte_flags with A = 0b1, D = (if update_d then 0b1 else pte_flags[D])]; - Some(pte[63 .. 8] @ pte_flags.bits) - } - else + Some([pte with 7 .. 0 = pte_flags.bits]) + } else { None() + } } diff --git a/model/riscv_vmem_tlb.sail b/model/riscv_vmem_tlb.sail index d066f1356..f91c06857 100644 --- a/model/riscv_vmem_tlb.sail +++ b/model/riscv_vmem_tlb.sail @@ -12,19 +12,51 @@ // (2) we can greatly speed up simulation speed (for Linux boot, can // reduce elapsed time from 10s of minutes to few minutes). -type asidbits = bits(16) +// Maximum number of Virtual/Physical Page Number bits. The same TLB +// is used for all VM modes so these are the values for Sv57. +type tlb_vpn_bits : Int = 57 - pagesize_bits +let tlb_vpn_bits = sizeof(tlb_vpn_bits) +type tlb_ppn_bits : Int = 44 +let tlb_ppn_bits = sizeof(tlb_ppn_bits) // PRIVATE +// We use a single TLB for all virtual memory modes, so it can store up to +// Sv57-sized entries. struct TLB_Entry = { - asid : asidbits, // address-space id - global : bool, // global translation - vAddr : bits(64), // VPN - pAddr : bits(64), // ppn - vMatchMask : bits(64), // matching mask for superpages - vAddrMask : bits(64), // selection mask for superpages - pte : bits(64), // PTE - pteAddr : bits(64), // for dirty writeback - age : bits(64) // for replacement policy? + asid : asidbits, // address-space id + global : bool, // global translation + vpn : bits(tlb_vpn_bits), // Virtual Page Number. SvXX - 12 bits. + vpnMask : bits(tlb_vpn_bits), // VPN selection mask for superpages. Upper bits are 1, lower bits 0. + ppn : bits(tlb_ppn_bits), // Physical Page Number, 22 (Sv32), or 44 (Sv39+) bits. + pte : bits(64), // PTE. This is only 32 bits for Sv32 so we zero extend. + pteAddr : bits(64), // Physical address of PTE, for writing dirty/accessed bits. +} + +// PTE access functions, for reading flags, and for modifying the dirty and +// accessed bits. +function tlb_get_pte forall 'n, 'n in {4, 8}. ( + pte_width : int('n), + ent : TLB_Entry, +) -> bits('n * 8) = ent.pte['n * 8 - 1 .. 0] + +function tlb_set_pte forall 'n, 'n in {4, 8}. ( + ent : TLB_Entry, + pte : bits('n * 8), +) -> TLB_Entry = { ent with pte=zero_extend(pte) } + +function tlb_get_ppn forall 'v, is_sv_mode('v) . ( + sv_width : int('v), + ent : TLB_Entry, + vpn : bits('v - pagesize_bits), +) -> ppn_bits('v) = { + // Sometimes the VPN is longer than the PPN (Sv39) and sometimes it is + // shorter. This is ok because the most significant component can never be + // included in the vpnMask. To avoid complicated truncation and zero + // extension we just extend to 64 bits and truncate at the end. + let vpn : bits(64) = zero_extend(vpn); + let vpnMask : bits(64) = zero_extend(ent.vpnMask); + let ppn : bits(64) = zero_extend(ent.ppn); + truncate(ppn | (vpn & vpnMask), if 'v == 32 then 22 else 44) } // 64 entries is based on benchmarks of Linux boots and is where you stop @@ -45,100 +77,103 @@ register tlb : vector(num_tlb_entries, option(TLB_Entry)) = [ ] // Indexed by the lowest bits of the VPN. -function tlb_hash(vaddr : bits(64)) -> tlb_index_range = - unsigned(vaddr[17 .. 12]) +function tlb_hash forall 'v, is_sv_mode('v) . ( + sv_mode : int('v), + vpn : bits('v - pagesize_bits), +) -> tlb_index_range = + unsigned(vpn[5 .. 0]) -// PUBLIC: invoked in init_vmem() [riscv_vmem.sail] +// PUBLIC: invoked in init_vmem() function init_TLB() -> unit = { foreach (i from 0 to (length(tlb) - 1)) { tlb[i] = None(); } } -// PUBLIC: invoked in translate_TLB_hit() [riscv_vmem.sail] +// PUBLIC: invoked in translate_TLB_hit() function write_TLB(index : tlb_index_range, ent : TLB_Entry) -> unit = tlb[index] = Some(ent) // PRIVATE -function match_TLB_Entry(ent : TLB_Entry, - asid : asidbits, - vaddr : bits(64)) -> bool = - (ent.global | (ent.asid == asid)) - & (ent.vAddr == (ent.vMatchMask & vaddr)) +function match_TLB_Entry( + ent : TLB_Entry, + asid : asidbits, + vpn : bits(tlb_vpn_bits), +) -> bool = + (ent.global | (ent.asid == asid)) & + (ent.vpn == (ent.vpnMask & vpn)) // PRIVATE -function flush_TLB_Entry(e : TLB_Entry, - asid : option(asidbits), - addr : option(bits(64))) -> bool = { - match (asid, addr) { - ( None(), None()) => true, - ( None(), Some(a)) => e.vAddr == (e.vMatchMask & a), - (Some(i), None()) => (e.asid == i) & not(e.global), - (Some(i), Some(a)) => ( (e.asid == i) & (e.vAddr == (a & e.vMatchMask)) - & not(e.global)) - } +function flush_TLB_Entry(ent : TLB_Entry, + asid : option(asidbits), + vaddr : option(xlenbits)) -> bool = { + let asid_matches : bool = match asid { + Some(asid) => ent.asid == asid & not(ent.global), + None() => true, + }; + let addr_matches : bool = match vaddr { + Some(vaddr) => { + let vaddr : bits(64) = zero_extend(vaddr); + ent.vpn == (ent.vpnMask & vaddr[56 .. pagesize_bits]) + }, + None() => true, + }; + asid_matches & addr_matches } -// PUBLIC: invoked in translate() [riscv_vmem.sail] -function lookup_TLB (asid : asidbits, vaddr : bits(64)) -> option((tlb_index_range, TLB_Entry)) = { - let index = tlb_hash(vaddr); +// PUBLIC: invoked in translate() +function lookup_TLB forall 'v, is_sv_mode('v) . ( + sv_width : int('v), + asid : asidbits, + vaddr : bits('v), +) -> option((tlb_index_range, TLB_Entry)) = { + let vpn = vaddr['v - 1 .. pagesize_bits]; + let index = tlb_hash('v, vpn); match tlb[index] { None() => None(), - Some(entry) => if match_TLB_Entry(entry, asid, vaddr) then Some((index, entry)) else None(), + Some(entry) => { + if match_TLB_Entry(entry, asid, zero_extend(vpn)) then Some((index, entry)) else None() + }, } } // PRIVATE -function add_to_TLB(asid : asidbits, - vAddr : bits(64), - pAddr : bits(64), - pte : bits(64), - pteAddr : bits(64), - level : nat, - global : bool, - levelBitSize : nat, - pagesize_bits : nat) -> unit = { - let shift = pagesize_bits + (level * levelBitSize); - assert(shift <= 64); - let vAddrMask : bits(64) = zero_extend(ones(shift)); - let vMatchMask : bits(64) = ~ (vAddrMask); - - let entry : TLB_Entry = struct{asid = asid, - global = global, - pte = pte, - pteAddr = pteAddr, - vAddrMask = vAddrMask, - vMatchMask = vMatchMask, - vAddr = vAddr & vMatchMask, - pAddr = pAddr & vMatchMask, - age = mcycle}; +function add_to_TLB forall 'v, is_sv_mode('v) . ( + sv_width : int('v), + asid : asidbits, + vpn : bits('v - pagesize_bits), + ppn : bits(if 'v == 32 then 22 else 44), + pte : bits(if 'v == 32 then 32 else 64), + pteAddr : xlenbits, + level : level_range('v), + global : bool, +) -> unit = { + let shift = level * (if 'v == 32 then 10 else 9); + let vpnMask : bits(tlb_vpn_bits) = ~(zero_extend(ones(shift))); + let entry : TLB_Entry = struct{asid = asid, + global = global, + pte = zero_extend(pte), + pteAddr = zero_extend(pteAddr), + vpnMask = vpnMask, + vpn = zero_extend(vpn) & vpnMask, + ppn = zero_extend(ppn)}; // Add the TLB entry. Note that this may be a super-page, but we still want // to add it to the index corresponding to the page because that is how // lookup_TLB looks it up. For superpages will just end up with the same // TLB entry in multiple slots. - let index = tlb_hash(vAddr); + let index = tlb_hash('v, vpn); tlb[index] = Some(entry); } // Top-level TLB flush function // PUBLIC: invoked from exec SFENCE_VMA -function flush_TLB(asid_xlen : option(xlenbits), - addr_xlen : option(xlenbits)) -> unit = { - let asid : option(asidbits) = - match asid_xlen { - None() => None(), - Some(a) => Some(a[15 .. 0]) - }; - let addr_64b : option(bits(64)) = - match addr_xlen { - None() => None(), - Some(a) => Some(zero_extend(a)) - }; +function flush_TLB(asid : option(asidbits), + addr : option(xlenbits)) -> unit = { foreach (i from 0 to (length(tlb) - 1)) { match tlb[i] { - Some(e) => if flush_TLB_Entry(e, asid, addr_64b) then { tlb[i] = None(); }, None() => (), + Some(e) => if flush_TLB_Entry(e, asid, addr) then { tlb[i] = None(); }, } } } diff --git a/model/riscv_vmem_types.sail b/model/riscv_vmem_types.sail index da1e053d6..9d8d1e28d 100644 --- a/model/riscv_vmem_types.sail +++ b/model/riscv_vmem_types.sail @@ -6,6 +6,25 @@ /* SPDX-License-Identifier: BSD-2-Clause */ /*=======================================================================================*/ +// Type constraint that checks if 'v is a valid virtual memory mode size. +type is_sv_mode('v) -> Bool = 'v in {32, 39, 48, 57} + +// Range of possible page levels depending on the virtual memory mode: +// +// Sv32 = range(0, 1) +// Sv39 = range(0, 2) +// Sv48 = range(0, 3) +// Sv57 = range(0, 4) +// +type level_range('v), is_sv_mode('v) = + range(0, (if 'v == 32 then 1 else (if 'v == 39 then 2 else (if 'v == 48 then 3 else 4)))) + +// Size of a Page Table Entry, depending on the virtual memory mode. +type pte_bits('v), is_sv_mode('v) = bits(if 'v == 32 then 32 else 64) + +// Number of Physical Page Number bits, depending on the virtual memory mode. +type ppn_bits('v), is_sv_mode('v) = bits(if 'v == 32 then 22 else 44) + // Extensions for memory Accesstype. type ext_access_type = unit diff --git a/model/riscv_xlen.sail b/model/riscv_xlen.sail index 8b0544352..94fb6dd37 100644 --- a/model/riscv_xlen.sail +++ b/model/riscv_xlen.sail @@ -15,3 +15,6 @@ type xlenbits = bits(xlen) // This saves typing `sizeof()` everywhere. let xlen_bytes = sizeof(xlen_bytes) let xlen = sizeof(xlen) + +let asidlen = sizeof(asidlen) +type asidbits = bits(asidlen) diff --git a/model/riscv_xlen32.sail b/model/riscv_xlen32.sail index 926f20f74..61d3ff178 100644 --- a/model/riscv_xlen32.sail +++ b/model/riscv_xlen32.sail @@ -10,3 +10,6 @@ // This is done using the smallest/most logarithmic possible value since Sail's // type system works well for multiply and 2^ but not divide and log2. type log2_xlen_bytes : Int = 2 + +// This is the maximum; designs can implement shorter ASIDLENs. +type asidlen : Int = 9 diff --git a/model/riscv_xlen64.sail b/model/riscv_xlen64.sail index 9878c7ffa..1ecc0d6e1 100644 --- a/model/riscv_xlen64.sail +++ b/model/riscv_xlen64.sail @@ -10,3 +10,6 @@ // This is done using the smallest/most logarithmic possible value since Sail's // type system works well for multiply and 2^ but not divide and log2. type log2_xlen_bytes : Int = 3 + +// This is the maximum; designs can implement shorter ASIDLENs. +type asidlen : Int = 16 diff --git a/sail-riscv.install b/sail-riscv.install index 7a539dfb5..b253d859e 100644 --- a/sail-riscv.install +++ b/sail-riscv.install @@ -1,2 +1,2 @@ bin: ["c_emulator/riscv_sim_RV64" "c_emulator/riscv_sim_RV32"] -share: [ "model/main.sail" {"model/main.sail"} "model/prelude.sail" {"model/prelude.sail"} "model/prelude_mem.sail" {"model/prelude_mem.sail"} "model/prelude_mem_metadata.sail" {"model/prelude_mem_metadata.sail"} "model/riscv_addr_checks.sail" {"model/riscv_addr_checks.sail"} "model/riscv_addr_checks_common.sail" {"model/riscv_addr_checks_common.sail"} "model/riscv_analysis.sail" {"model/riscv_analysis.sail"} "model/riscv_csr_ext.sail" {"model/riscv_csr_ext.sail"} "model/riscv_csr_map.sail" {"model/riscv_csr_map.sail"} "model/riscv_decode_ext.sail" {"model/riscv_decode_ext.sail"} "model/riscv_ext_regs.sail" {"model/riscv_ext_regs.sail"} "model/riscv_fdext_control.sail" {"model/riscv_fdext_control.sail"} "model/riscv_fdext_regs.sail" {"model/riscv_fdext_regs.sail"} "model/riscv_fetch.sail" {"model/riscv_fetch.sail"} "model/riscv_fetch_rvfi.sail" {"model/riscv_fetch_rvfi.sail"} "model/riscv_flen_D.sail" {"model/riscv_flen_D.sail"} "model/riscv_flen_F.sail" {"model/riscv_flen_F.sail"} "model/riscv_freg_type.sail" {"model/riscv_freg_type.sail"} "model/riscv_insts_aext.sail" {"model/riscv_insts_aext.sail"} "model/riscv_insts_base.sail" {"model/riscv_insts_base.sail"} "model/riscv_insts_begin.sail" {"model/riscv_insts_begin.sail"} "model/riscv_insts_cdext.sail" {"model/riscv_insts_cdext.sail"} "model/riscv_insts_cext.sail" {"model/riscv_insts_cext.sail"} "model/riscv_insts_cfext.sail" {"model/riscv_insts_cfext.sail"} "model/riscv_insts_dext.sail" {"model/riscv_insts_dext.sail"} "model/riscv_insts_end.sail" {"model/riscv_insts_end.sail"} "model/riscv_insts_fext.sail" {"model/riscv_insts_fext.sail"} "model/riscv_insts_hints.sail" {"model/riscv_insts_hints.sail"} "model/riscv_insts_mext.sail" {"model/riscv_insts_mext.sail"} "model/riscv_insts_next.sail" {"model/riscv_insts_next.sail"} "model/riscv_insts_rmem.sail" {"model/riscv_insts_rmem.sail"} "model/riscv_insts_zba.sail" {"model/riscv_insts_zba.sail"} "model/riscv_insts_zbb.sail" {"model/riscv_insts_zbb.sail"} "model/riscv_insts_zbc.sail" {"model/riscv_insts_zbc.sail"} "model/riscv_insts_zbkb.sail" {"model/riscv_insts_zbkb.sail"} "model/riscv_insts_zbkx.sail" {"model/riscv_insts_zbkx.sail"} "model/riscv_insts_zbs.sail" {"model/riscv_insts_zbs.sail"} "model/riscv_insts_zfh.sail" {"model/riscv_insts_zfh.sail"} "model/riscv_insts_zicsr.sail" {"model/riscv_insts_zicsr.sail"} "model/riscv_insts_zkn.sail" {"model/riscv_insts_zkn.sail"} "model/riscv_insts_zks.sail" {"model/riscv_insts_zks.sail"} "model/riscv_jalr_rmem.sail" {"model/riscv_jalr_rmem.sail"} "model/riscv_jalr_seq.sail" {"model/riscv_jalr_seq.sail"} "model/riscv_mem.sail" {"model/riscv_mem.sail"} "model/riscv_misa_ext.sail" {"model/riscv_misa_ext.sail"} "model/riscv_next_control.sail" {"model/riscv_next_control.sail"} "model/riscv_next_regs.sail" {"model/riscv_next_regs.sail"} "model/riscv_pc_access.sail" {"model/riscv_pc_access.sail"} "model/riscv_platform.sail" {"model/riscv_platform.sail"} "model/riscv_pmp_control.sail" {"model/riscv_pmp_control.sail"} "model/riscv_pmp_regs.sail" {"model/riscv_pmp_regs.sail"} "model/riscv_pte.sail" {"model/riscv_pte.sail"} "model/riscv_ptw.sail" {"model/riscv_ptw.sail"} "model/riscv_reg_type.sail" {"model/riscv_reg_type.sail"} "model/riscv_regs.sail" {"model/riscv_regs.sail"} "model/riscv_softfloat_interface.sail" {"model/riscv_softfloat_interface.sail"} "model/riscv_step.sail" {"model/riscv_step.sail"} "model/riscv_step_common.sail" {"model/riscv_step_common.sail"} "model/riscv_step_ext.sail" {"model/riscv_step_ext.sail"} "model/riscv_step_rvfi.sail" {"model/riscv_step_rvfi.sail"} "model/riscv_sync_exception.sail" {"model/riscv_sync_exception.sail"} "model/riscv_sys_control.sail" {"model/riscv_sys_control.sail"} "model/riscv_sys_exceptions.sail" {"model/riscv_sys_exceptions.sail"} "model/riscv_sys_regs.sail" {"model/riscv_sys_regs.sail"} "model/riscv_termination_common.sail" {"model/riscv_termination_common.sail"} "model/riscv_termination_rv32.sail" {"model/riscv_termination_rv32.sail"} "model/riscv_termination_rv64.sail" {"model/riscv_termination_rv64.sail"} "model/riscv_types.sail" {"model/riscv_types.sail"} "model/riscv_types_common.sail" {"model/riscv_types_common.sail"} "model/riscv_types_ext.sail" {"model/riscv_types_ext.sail"} "model/riscv_types_kext.sail" {"model/riscv_types_kext.sail"} "model/riscv_vmem_common.sail" {"model/riscv_vmem_common.sail"} "model/riscv_vmem_rv32.sail" {"model/riscv_vmem_rv32.sail"} "model/riscv_vmem_rv64.sail" {"model/riscv_vmem_rv64.sail"} "model/riscv_vmem_sv32.sail" {"model/riscv_vmem_sv32.sail"} "model/riscv_vmem_sv39.sail" {"model/riscv_vmem_sv39.sail"} "model/riscv_vmem_sv48.sail" {"model/riscv_vmem_sv48.sail"} "model/riscv_vmem_tlb.sail" {"model/riscv_vmem_tlb.sail"} "model/riscv_vmem_types.sail" {"model/riscv_vmem_types.sail"} "model/riscv_xlen32.sail" {"model/riscv_xlen32.sail"} "model/riscv_xlen64.sail" {"model/riscv_xlen64.sail"} "model/rvfi_dii.sail" {"model/rvfi_dii.sail"} "c_emulator/riscv_platform.c" {"c_emulator/riscv_platform.c"} "c_emulator/riscv_platform_impl.c" {"c_emulator/riscv_platform_impl.c"} "c_emulator/riscv_prelude.c" {"c_emulator/riscv_prelude.c"} "c_emulator/riscv_sim.c" {"c_emulator/riscv_sim.c"} "c_emulator/riscv_softfloat.c" {"c_emulator/riscv_softfloat.c"} "c_emulator/riscv_config.h" {"c_emulator/riscv_config.h"} "c_emulator/riscv_platform.h" {"c_emulator/riscv_platform.h"} "c_emulator/riscv_platform_impl.h" {"c_emulator/riscv_platform_impl.h"} "c_emulator/riscv_prelude.h" {"c_emulator/riscv_prelude.h"} "c_emulator/riscv_sail.h" {"c_emulator/riscv_sail.h"} "c_emulator/riscv_softfloat.h" {"c_emulator/riscv_softfloat.h"} "handwritten_support/mem_metadata.lem" {"handwritten_support/mem_metadata.lem"} "handwritten_support/riscv_extras.lem" {"handwritten_support/riscv_extras.lem"} "handwritten_support/riscv_extras_fdext.lem" {"handwritten_support/riscv_extras_fdext.lem"} "handwritten_support/riscv_extras_sequential.lem" {"handwritten_support/riscv_extras_sequential.lem"} "handwritten_support/hgen/ast.hgen" {"handwritten_support/hgen/ast.hgen"} "handwritten_support/hgen/fold.hgen" {"handwritten_support/hgen/fold.hgen"} "handwritten_support/hgen/herdtools_ast_to_shallow_ast.hgen" {"handwritten_support/hgen/herdtools_ast_to_shallow_ast.hgen"} "handwritten_support/hgen/herdtools_types_to_shallow_types.hgen" {"handwritten_support/hgen/herdtools_types_to_shallow_types.hgen"} "handwritten_support/hgen/lexer.hgen" {"handwritten_support/hgen/lexer.hgen"} "handwritten_support/hgen/lexer_regexps.hgen" {"handwritten_support/hgen/lexer_regexps.hgen"} "handwritten_support/hgen/map.hgen" {"handwritten_support/hgen/map.hgen"} "handwritten_support/hgen/parser.hgen" {"handwritten_support/hgen/parser.hgen"} "handwritten_support/hgen/pretty.hgen" {"handwritten_support/hgen/pretty.hgen"} "handwritten_support/hgen/pretty_xml.hgen" {"handwritten_support/hgen/pretty_xml.hgen"} "handwritten_support/hgen/sail_trans_out.hgen" {"handwritten_support/hgen/sail_trans_out.hgen"} "handwritten_support/hgen/shallow_ast_to_herdtools_ast.hgen" {"handwritten_support/hgen/shallow_ast_to_herdtools_ast.hgen"} "handwritten_support/hgen/shallow_types_to_herdtools_types.hgen" {"handwritten_support/hgen/shallow_types_to_herdtools_types.hgen"} "handwritten_support/hgen/token_types.hgen" {"handwritten_support/hgen/token_types.hgen"} "handwritten_support/hgen/tokens.hgen" {"handwritten_support/hgen/tokens.hgen"} "handwritten_support/hgen/trans_sail.hgen" {"handwritten_support/hgen/trans_sail.hgen"} "handwritten_support/hgen/types.hgen" {"handwritten_support/hgen/types.hgen"} "handwritten_support/hgen/types_sail_trans_out.hgen" {"handwritten_support/hgen/types_sail_trans_out.hgen"} "handwritten_support/hgen/types_trans_sail.hgen" {"handwritten_support/hgen/types_trans_sail.hgen"} "handwritten_support/0.11/mem_metadata.lem" {"handwritten_support/0.11/mem_metadata.lem"} "handwritten_support/0.11/riscv_extras.lem" {"handwritten_support/0.11/riscv_extras.lem"} "handwritten_support/0.11/riscv_extras_fdext.lem" {"handwritten_support/0.11/riscv_extras_fdext.lem"} "handwritten_support/0.11/riscv_extras_sequential.lem" {"handwritten_support/0.11/riscv_extras_sequential.lem"} "generated_definitions/for-rmem/riscv.lem" {"generated_definitions/for-rmem/riscv.lem"} "generated_definitions/for-rmem/riscv_types.lem" {"generated_definitions/for-rmem/riscv_types.lem"} "generated_definitions/for-rmem/riscv_toFromInterp2.ml" {"generated_definitions/for-rmem/riscv_toFromInterp2.ml"} "generated_definitions/for-rmem/riscv.defs" {"generated_definitions/for-rmem/riscv.defs"} ] +share: [ "model/main.sail" {"model/main.sail"} "model/prelude.sail" {"model/prelude.sail"} "model/prelude_mem.sail" {"model/prelude_mem.sail"} "model/prelude_mem_metadata.sail" {"model/prelude_mem_metadata.sail"} "model/riscv_addr_checks.sail" {"model/riscv_addr_checks.sail"} "model/riscv_addr_checks_common.sail" {"model/riscv_addr_checks_common.sail"} "model/riscv_analysis.sail" {"model/riscv_analysis.sail"} "model/riscv_csr_ext.sail" {"model/riscv_csr_ext.sail"} "model/riscv_csr_map.sail" {"model/riscv_csr_map.sail"} "model/riscv_decode_ext.sail" {"model/riscv_decode_ext.sail"} "model/riscv_ext_regs.sail" {"model/riscv_ext_regs.sail"} "model/riscv_fdext_control.sail" {"model/riscv_fdext_control.sail"} "model/riscv_fdext_regs.sail" {"model/riscv_fdext_regs.sail"} "model/riscv_fetch.sail" {"model/riscv_fetch.sail"} "model/riscv_fetch_rvfi.sail" {"model/riscv_fetch_rvfi.sail"} "model/riscv_flen_D.sail" {"model/riscv_flen_D.sail"} "model/riscv_flen_F.sail" {"model/riscv_flen_F.sail"} "model/riscv_freg_type.sail" {"model/riscv_freg_type.sail"} "model/riscv_insts_aext.sail" {"model/riscv_insts_aext.sail"} "model/riscv_insts_base.sail" {"model/riscv_insts_base.sail"} "model/riscv_insts_begin.sail" {"model/riscv_insts_begin.sail"} "model/riscv_insts_cdext.sail" {"model/riscv_insts_cdext.sail"} "model/riscv_insts_cext.sail" {"model/riscv_insts_cext.sail"} "model/riscv_insts_cfext.sail" {"model/riscv_insts_cfext.sail"} "model/riscv_insts_dext.sail" {"model/riscv_insts_dext.sail"} "model/riscv_insts_end.sail" {"model/riscv_insts_end.sail"} "model/riscv_insts_fext.sail" {"model/riscv_insts_fext.sail"} "model/riscv_insts_hints.sail" {"model/riscv_insts_hints.sail"} "model/riscv_insts_mext.sail" {"model/riscv_insts_mext.sail"} "model/riscv_insts_next.sail" {"model/riscv_insts_next.sail"} "model/riscv_insts_rmem.sail" {"model/riscv_insts_rmem.sail"} "model/riscv_insts_zba.sail" {"model/riscv_insts_zba.sail"} "model/riscv_insts_zbb.sail" {"model/riscv_insts_zbb.sail"} "model/riscv_insts_zbc.sail" {"model/riscv_insts_zbc.sail"} "model/riscv_insts_zbkb.sail" {"model/riscv_insts_zbkb.sail"} "model/riscv_insts_zbkx.sail" {"model/riscv_insts_zbkx.sail"} "model/riscv_insts_zbs.sail" {"model/riscv_insts_zbs.sail"} "model/riscv_insts_zfh.sail" {"model/riscv_insts_zfh.sail"} "model/riscv_insts_zicsr.sail" {"model/riscv_insts_zicsr.sail"} "model/riscv_insts_zkn.sail" {"model/riscv_insts_zkn.sail"} "model/riscv_insts_zks.sail" {"model/riscv_insts_zks.sail"} "model/riscv_jalr_rmem.sail" {"model/riscv_jalr_rmem.sail"} "model/riscv_jalr_seq.sail" {"model/riscv_jalr_seq.sail"} "model/riscv_mem.sail" {"model/riscv_mem.sail"} "model/riscv_misa_ext.sail" {"model/riscv_misa_ext.sail"} "model/riscv_next_control.sail" {"model/riscv_next_control.sail"} "model/riscv_next_regs.sail" {"model/riscv_next_regs.sail"} "model/riscv_pc_access.sail" {"model/riscv_pc_access.sail"} "model/riscv_platform.sail" {"model/riscv_platform.sail"} "model/riscv_pmp_control.sail" {"model/riscv_pmp_control.sail"} "model/riscv_pmp_regs.sail" {"model/riscv_pmp_regs.sail"} "model/riscv_pte.sail" {"model/riscv_pte.sail"} "model/riscv_ptw.sail" {"model/riscv_ptw.sail"} "model/riscv_reg_type.sail" {"model/riscv_reg_type.sail"} "model/riscv_regs.sail" {"model/riscv_regs.sail"} "model/riscv_softfloat_interface.sail" {"model/riscv_softfloat_interface.sail"} "model/riscv_step.sail" {"model/riscv_step.sail"} "model/riscv_step_common.sail" {"model/riscv_step_common.sail"} "model/riscv_step_ext.sail" {"model/riscv_step_ext.sail"} "model/riscv_step_rvfi.sail" {"model/riscv_step_rvfi.sail"} "model/riscv_sync_exception.sail" {"model/riscv_sync_exception.sail"} "model/riscv_sys_control.sail" {"model/riscv_sys_control.sail"} "model/riscv_sys_exceptions.sail" {"model/riscv_sys_exceptions.sail"} "model/riscv_sys_regs.sail" {"model/riscv_sys_regs.sail"} "model/riscv_termination_common.sail" {"model/riscv_termination_common.sail"} "model/riscv_termination_rv32.sail" {"model/riscv_termination_rv32.sail"} "model/riscv_termination_rv64.sail" {"model/riscv_termination_rv64.sail"} "model/riscv_types.sail" {"model/riscv_types.sail"} "model/riscv_types_common.sail" {"model/riscv_types_common.sail"} "model/riscv_types_ext.sail" {"model/riscv_types_ext.sail"} "model/riscv_types_kext.sail" {"model/riscv_types_kext.sail"} "model/riscv_vmem_rv32.sail" {"model/riscv_vmem_rv32.sail"} "model/riscv_vmem_rv64.sail" {"model/riscv_vmem_rv64.sail"} "model/riscv_vmem_sv32.sail" {"model/riscv_vmem_sv32.sail"} "model/riscv_vmem_sv39.sail" {"model/riscv_vmem_sv39.sail"} "model/riscv_vmem_sv48.sail" {"model/riscv_vmem_sv48.sail"} "model/riscv_vmem_tlb.sail" {"model/riscv_vmem_tlb.sail"} "model/riscv_vmem_types.sail" {"model/riscv_vmem_types.sail"} "model/riscv_xlen32.sail" {"model/riscv_xlen32.sail"} "model/riscv_xlen64.sail" {"model/riscv_xlen64.sail"} "model/rvfi_dii.sail" {"model/rvfi_dii.sail"} "c_emulator/riscv_platform.c" {"c_emulator/riscv_platform.c"} "c_emulator/riscv_platform_impl.c" {"c_emulator/riscv_platform_impl.c"} "c_emulator/riscv_prelude.c" {"c_emulator/riscv_prelude.c"} "c_emulator/riscv_sim.c" {"c_emulator/riscv_sim.c"} "c_emulator/riscv_softfloat.c" {"c_emulator/riscv_softfloat.c"} "c_emulator/riscv_config.h" {"c_emulator/riscv_config.h"} "c_emulator/riscv_platform.h" {"c_emulator/riscv_platform.h"} "c_emulator/riscv_platform_impl.h" {"c_emulator/riscv_platform_impl.h"} "c_emulator/riscv_prelude.h" {"c_emulator/riscv_prelude.h"} "c_emulator/riscv_sail.h" {"c_emulator/riscv_sail.h"} "c_emulator/riscv_softfloat.h" {"c_emulator/riscv_softfloat.h"} "handwritten_support/mem_metadata.lem" {"handwritten_support/mem_metadata.lem"} "handwritten_support/riscv_extras.lem" {"handwritten_support/riscv_extras.lem"} "handwritten_support/riscv_extras_fdext.lem" {"handwritten_support/riscv_extras_fdext.lem"} "handwritten_support/riscv_extras_sequential.lem" {"handwritten_support/riscv_extras_sequential.lem"} "handwritten_support/hgen/ast.hgen" {"handwritten_support/hgen/ast.hgen"} "handwritten_support/hgen/fold.hgen" {"handwritten_support/hgen/fold.hgen"} "handwritten_support/hgen/herdtools_ast_to_shallow_ast.hgen" {"handwritten_support/hgen/herdtools_ast_to_shallow_ast.hgen"} "handwritten_support/hgen/herdtools_types_to_shallow_types.hgen" {"handwritten_support/hgen/herdtools_types_to_shallow_types.hgen"} "handwritten_support/hgen/lexer.hgen" {"handwritten_support/hgen/lexer.hgen"} "handwritten_support/hgen/lexer_regexps.hgen" {"handwritten_support/hgen/lexer_regexps.hgen"} "handwritten_support/hgen/map.hgen" {"handwritten_support/hgen/map.hgen"} "handwritten_support/hgen/parser.hgen" {"handwritten_support/hgen/parser.hgen"} "handwritten_support/hgen/pretty.hgen" {"handwritten_support/hgen/pretty.hgen"} "handwritten_support/hgen/pretty_xml.hgen" {"handwritten_support/hgen/pretty_xml.hgen"} "handwritten_support/hgen/sail_trans_out.hgen" {"handwritten_support/hgen/sail_trans_out.hgen"} "handwritten_support/hgen/shallow_ast_to_herdtools_ast.hgen" {"handwritten_support/hgen/shallow_ast_to_herdtools_ast.hgen"} "handwritten_support/hgen/shallow_types_to_herdtools_types.hgen" {"handwritten_support/hgen/shallow_types_to_herdtools_types.hgen"} "handwritten_support/hgen/token_types.hgen" {"handwritten_support/hgen/token_types.hgen"} "handwritten_support/hgen/tokens.hgen" {"handwritten_support/hgen/tokens.hgen"} "handwritten_support/hgen/trans_sail.hgen" {"handwritten_support/hgen/trans_sail.hgen"} "handwritten_support/hgen/types.hgen" {"handwritten_support/hgen/types.hgen"} "handwritten_support/hgen/types_sail_trans_out.hgen" {"handwritten_support/hgen/types_sail_trans_out.hgen"} "handwritten_support/hgen/types_trans_sail.hgen" {"handwritten_support/hgen/types_trans_sail.hgen"} "handwritten_support/0.11/mem_metadata.lem" {"handwritten_support/0.11/mem_metadata.lem"} "handwritten_support/0.11/riscv_extras.lem" {"handwritten_support/0.11/riscv_extras.lem"} "handwritten_support/0.11/riscv_extras_fdext.lem" {"handwritten_support/0.11/riscv_extras_fdext.lem"} "handwritten_support/0.11/riscv_extras_sequential.lem" {"handwritten_support/0.11/riscv_extras_sequential.lem"} "generated_definitions/for-rmem/riscv.lem" {"generated_definitions/for-rmem/riscv.lem"} "generated_definitions/for-rmem/riscv_types.lem" {"generated_definitions/for-rmem/riscv_types.lem"} "generated_definitions/for-rmem/riscv_toFromInterp2.ml" {"generated_definitions/for-rmem/riscv_toFromInterp2.ml"} "generated_definitions/for-rmem/riscv.defs" {"generated_definitions/for-rmem/riscv.defs"} ]