diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail index 8953ad4b3..dfb024746 100644 --- a/model/riscv_insts_zicsr.sail +++ b/model/riscv_insts_zicsr.sail @@ -198,10 +198,10 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = { (0x304, _) => { mie = legalize_mie(mie, value); Some(mie.bits()) }, (0x305, _) => { Some(set_mtvec(value)) }, (0x306, _) => { mcounteren = legalize_mcounteren(mcounteren, value); Some(zero_extend(mcounteren.bits())) }, - (0x30A, 32) => { menvcfg = legalize_envcfg(menvcfg, menvcfg.bits()[63 .. 32] @ value); Some(menvcfg.bits()[31 .. 0]) }, - (0x30A, 64) => { menvcfg = legalize_envcfg(menvcfg, value); Some(menvcfg.bits()) }, + (0x30A, 32) => { menvcfg = legalize_menvcfg(menvcfg, menvcfg.bits()[63 .. 32] @ value); Some(menvcfg.bits()[31 .. 0]) }, + (0x30A, 64) => { menvcfg = legalize_menvcfg(menvcfg, value); Some(menvcfg.bits()) }, (0x310, 32) => { Some(mstatush.bits()) }, // ignore writes for now - (0x31A, 32) => { menvcfg = legalize_envcfg(menvcfg, value @ menvcfg.bits()[31 .. 0]); Some(menvcfg.bits()[63 .. 32]) }, + (0x31A, 32) => { menvcfg = legalize_menvcfg(menvcfg, value @ menvcfg.bits()[31 .. 0]); Some(menvcfg.bits()[63 .. 32]) }, (0x320, _) => { mcountinhibit = legalize_mcountinhibit(mcountinhibit, value); Some(zero_extend(mcountinhibit.bits())) }, (0x340, _) => { mscratch = value; Some(mscratch) }, (0x341, _) => { Some(set_xret_target(Machine, value)) }, @@ -248,7 +248,7 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = { (0x104, _) => { mie = legalize_sie(mie, mideleg, value); Some(mie.bits()) }, (0x105, _) => { Some(set_stvec(value)) }, (0x106, _) => { scounteren = legalize_scounteren(scounteren, value); Some(zero_extend(scounteren.bits())) }, - (0x10A, _) => { senvcfg = legalize_envcfg(senvcfg, zero_extend(value)); Some(senvcfg.bits()[sizeof(xlen) - 1 .. 0]) }, + (0x10A, _) => { senvcfg = legalize_senvcfg(senvcfg, zero_extend(value)); Some(senvcfg.bits()[sizeof(xlen) - 1 .. 0]) }, (0x140, _) => { sscratch = value; Some(sscratch) }, (0x141, _) => { Some(set_xret_target(Supervisor, value)) }, (0x142, _) => { scause->bits() = value; Some(scause.bits()) }, diff --git a/model/riscv_pte.sail b/model/riscv_pte.sail index 90345cc93..7e2633742 100644 --- a/model/riscv_pte.sail +++ b/model/riscv_pte.sail @@ -77,6 +77,12 @@ type pteAttribs = bits(8) */ type extPte = bits(10) +bitfield EXT_PTE_Bits : extPte = { + N : 9, + PBMT : 8 .. 7, + RSVD : 6 .. 0 +} + /* * On SV32, there are no reserved bits available to extensions. Therefore, by * default, we initialize the PTE extension field with all zeros. However, @@ -106,7 +112,13 @@ function isPTEPtr(p : pteAttribs, ext : extPte) -> bool = { function isInvalidPTE(p : pteAttribs, ext : extPte) -> bool = { let a = Mk_PTE_Bits(p); - a.V() == 0b0 | (a.W() == 0b1 & a.R() == 0b0) + let e = Mk_EXT_PTE_Bits(ext); + a.V() == 0b0 | + (a.W() == 0b1 & a.R() == 0b0) | + (e.RSVD() != 0b0000000 | e.PBMT() == 0b11) | + (not(isPTEPtr(p, ext)) & (e.N() != 0b0 ) & (not(haveSvnapot()))) | + (not(isPTEPtr(p, ext)) & (e.PBMT() != 0b00) & (not(haveSvpbmt()) | menvcfg.PBMTE() == 0b0)) | + (isPTEPtr(p, ext) & (a.D() == 0b1 | a.A() == 0b1 | a.U() == 0b1 | e.N() != 0b0 | e.PBMT() != 0b00)) } union PTE_Check = { diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index 84f708e2f..75c9f038a 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -215,6 +215,12 @@ function haveZmmul() -> bool = true /* Zicond extension support */ function haveZicond() -> bool = true +/* Svpbmt extension support */ +function haveSvpbmt() -> bool = true + +/* Svnapot extension support */ +function haveSvnapot() -> bool = true + bitfield Mstatush : bits(32) = { MBE : 5, SBE : 4 @@ -865,7 +871,16 @@ bitfield Envcfg : bits(64) = { register menvcfg : Envcfg register senvcfg : Envcfg -function legalize_envcfg(o : Envcfg, v : bits(64)) -> Envcfg = { +function legalize_menvcfg(o : Envcfg, v : bits(64)) -> Envcfg = { + let v = Mk_Envcfg(v); + let o = update_FIOM(o, if sys_enable_writable_fiom() then v.FIOM() else 0b0); + // Svpbmt - PBMTE : PBMT enable + let o = update_PBMTE(o, if haveSvpbmt() then v.PBMTE() else 0b0); + // Other extensions are not implemented yet so all other fields are read only zero. + o +} + +function legalize_senvcfg(o : Envcfg, v : bits(64)) -> Envcfg = { let v = Mk_Envcfg(v); let o = update_FIOM(o, if sys_enable_writable_fiom() then v.FIOM() else 0b0); // Other extensions are not implemented yet so all other fields are read only zero. diff --git a/model/riscv_vmem_sv39.sail b/model/riscv_vmem_sv39.sail index 25378a8dc..eedbe08cc 100644 --- a/model/riscv_vmem_sv39.sail +++ b/model/riscv_vmem_sv39.sail @@ -90,6 +90,7 @@ function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { let pbits = pte.BITS(); let ext_pte = pte.Ext(); let pattr = Mk_PTE_Bits(pbits); + let eattr = Mk_EXT_PTE_Bits(ext_pte); let is_global = global | (pattr.G() == 0b1); /* print("walk39(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level) ^ " pt_base=" ^ BitStr(ptb) @@ -119,7 +120,9 @@ function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { if level > 0 then { /* superpage */ /* fixme hack: to get a mask of appropriate size */ let mask = shiftl(pte.PPNi() ^ pte.PPNi() ^ zero_extend(0b1), level * SV39_LEVEL_BITS) - 1; - if (pte.PPNi() & mask) != zero_extend(0b0) then { + if eattr.N() == 0b1 then { + PTW_Failure(PTW_Invalid_PTE(), ext_ptw) + } else if (pte.PPNi() & mask) != zero_extend(0b0) then { /* misaligned superpage mapping */ /* print("walk39: misaligned superpage mapping"); */ PTW_Failure(PTW_Misaligned(), ext_ptw) @@ -133,9 +136,17 @@ function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { } } else { /* normal leaf PTE */ -/* let res = append(pte.PPNi(), va.PgOfs()); - print("walk39: pte.ppn=" ^ BitStr(pte.PPNi()) ^ " ppn=" ^ BitStr(pte.PPNi()) ^ " res=" ^ BitStr(res)); */ - PTW_Success(append(pte.PPNi(), va.PgOfs()), pte, pte_addr, level, is_global, ext_ptw) + if ( eattr.N() == 0b1 & pte.PPNi()[3 .. 0] != 0b1000 ) then { + PTW_Failure(PTW_Invalid_PTE(), ext_ptw) + } else { + let ppn : bits(44) = match eattr.N() { + 0b0 => pte.PPNi(), + 0b1 => append(pte.PPNi()[43 .. 4], va.VPNi()[3 .. 0]) + }; +/* let res = append(ppn, va.PgOfs()); + print("walk39: pte.ppn=" ^ BitStr(pte.PPNi()) ^ " ppn=" ^ BitStr(ppn) ^ " res=" ^ BitStr(res)); */ + PTW_Success(append(ppn, va.PgOfs()), pte, pte_addr, level, is_global, ext_ptw) + } } } } diff --git a/model/riscv_vmem_sv48.sail b/model/riscv_vmem_sv48.sail index 64c7a542a..d0fd0992c 100644 --- a/model/riscv_vmem_sv48.sail +++ b/model/riscv_vmem_sv48.sail @@ -90,6 +90,7 @@ function walk48(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { let pbits = pte.BITS(); let ext_pte = pte.Ext(); let pattr = Mk_PTE_Bits(pbits); + let eattr = Mk_EXT_PTE_Bits(ext_pte); let is_global = global | (pattr.G() == 0b1); /* print("walk48(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level) ^ " pt_base=" ^ BitStr(ptb) @@ -119,7 +120,9 @@ function walk48(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { if level > 0 then { /* superpage */ /* fixme hack: to get a mask of appropriate size */ let mask = shiftl(pte.PPNi() ^ pte.PPNi() ^ zero_extend(0b1), level * SV48_LEVEL_BITS) - 1; - if (pte.PPNi() & mask) != zero_extend(0b0) then { + if eattr.N() == 0b1 then { + PTW_Failure(PTW_Invalid_PTE(), ext_ptw) + } else if (pte.PPNi() & mask) != zero_extend(0b0) then { /* misaligned superpage mapping */ /* print("walk48: misaligned superpage mapping"); */ PTW_Failure(PTW_Misaligned(), ext_ptw) @@ -133,9 +136,17 @@ function walk48(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { } } else { /* normal leaf PTE */ -/* let res = append(pte.PPNi(), va.PgOfs()); - print("walk48: pte.ppn=" ^ BitStr(pte.PPNi()) ^ " ppn=" ^ BitStr(pte.PPNi()) ^ " res=" ^ BitStr(res)); */ - PTW_Success(append(pte.PPNi(), va.PgOfs()), pte, pte_addr, level, is_global, ext_ptw) + if ( eattr.N() == 0b1 & pte.PPNi()[3 .. 0] != 0b1000 ) then { + PTW_Failure(PTW_Invalid_PTE(), ext_ptw) + } else { + let ppn : bits(44) = match eattr.N() { + 0b0 => pte.PPNi(), + 0b1 => append(pte.PPNi()[43 .. 4], va.VPNi()[3 .. 0]) + }; +/* let res = append(ppn, va.PgOfs()); + print("walk48: pte.ppn=" ^ BitStr(pte.PPNi()) ^ " ppn=" ^ BitStr(ppn) ^ " res=" ^ BitStr(res)); */ + PTW_Success(append(ppn, va.PgOfs()), pte, pte_addr, level, is_global, ext_ptw) + } } } }