riscv/model/riscv.sml

112     pte: SV_PTE, pteAddr: BitsN.nbit, vAddr: BitsN.nbit,
1426 fun TLBEntry_age_rupd ({age, asid, global, pAddr, pte, pteAddr, vAddr,
1428   {age = x', asid = asid, global = global, pAddr = pAddr, pte = pte,
1432 fun TLBEntry_asid_rupd ({age, asid, global, pAddr, pte, pteAddr, vAddr,
1434   {age = age, asid = x', global = global, pAddr = pAddr, pte = pte,
1438 fun TLBEntry_global_rupd ({age, asid, global, pAddr, pte, pteAddr, vAddr,
1440   {age = age, asid = asid, global = x', pAddr = pAddr, pte = pte,
1444 fun TLBEntry_pAddr_rupd ({age, asid, global, pAddr, pte, pteAddr, vAddr,
1446   {age = age, asid = asid, global = global, pAddr = x', pte = pte,
1450 fun TLBEntry_pte_rupd ({age, asid, global, pAddr, pte, pteAddr, vAddr,
1452   {age = age, asid = asid, global = global, pAddr = pAddr, pte = x',
1456 fun TLBEntry_pteAddr_rupd ({age, asid, global, pAddr, pte, pteAddr, vAddr,
1458   {age = age, asid = asid, global = global, pAddr = pAddr, pte = pte,
1462 fun TLBEntry_vAddr_rupd ({age, asid, global, pAddr, pte, pteAddr, vAddr,
1464   {age = age, asid = asid, global = global, pAddr = pAddr, pte = pte,
1468 fun TLBEntry_vAddrMask_rupd ({age, asid, global, pAddr, pte, pteAddr,
1470   {age = age, asid = asid, global = global, pAddr = pAddr, pte = pte,
1474 fun TLBEntry_vMatchMask_rupd ({age, asid, global, pAddr, pte, pteAddr,
1476   {age = age, asid = asid, global = global, pAddr = pAddr, pte = pte,
4050     val pte = rec'SV_PTE(rawReadData pte_addr)
4061            " pte=0x",
4062            L3.padLeftString(#"0",(16,BitsN.toHexString(reg'SV_PTE pte)))])
4065     ; if not(#PTE_V(pte : SV_PTE))
4069       else if ((#PTE_T(pte : SV_PTE)) = (BitsN.B(0x0,4))) orelse
4070          ((#PTE_T(pte : SV_PTE)) = (BitsN.B(0x1,4)))
4085                               (#PTE_PPNi(pte : SV_PTE),PAGESIZE_BITS)),
4087       else if not(checkMemPermission(ft,(ac,(priv,#PTE_T(pte : SV_PTE)))))
4092              val pte_w = ref pte
4095                val old_r = #PTE_R(pte : SV_PTE)
4096                val old_d = #PTE_D(pte : SV_PTE)
4113                                        (#PTE_PPNi(pte : SV_PTE),
4124                      else #PTE_PPNi(pte : SV_PTE)
4130                        (level,(isGlobal(#PTE_T(pte : SV_PTE)),pte_addr))))
4141 fun mkTLBEntry (asid,(global,(vAddr,(pAddr,(pte,(i,pteAddr)))))) =
4145      pte =
4154     ; ent := (TLBEntry_pte_rupd((!ent),pte))
4208 fun addToTLB (asid,(vAddr,(pAddr,(pte,(pteAddr,(i,(global,curTLB))))))) =
4211        (asid,(global,(vAddr,(pAddr,(pte,(i,pteAddr)))))))
4312                (ft,(ac,(priv,#PTE_T((#pte(e : TLBEntry)) : SV_PTE))))
4315                       (not(#PTE_D((#pte(e : TLBEntry)) : SV_PTE)))
4320                                 val x0 = #pte((!ent) : TLBEntry)
4328                                  (reg'SV_PTE(#pte((!ent) : TLBEntry)),8))
4359             Option.SOME(pAddr,(pte,(i,(global,pteAddr)))) =>
4363                       (vAddr,(pAddr,(pte,(pteAddr,(i,(global,TLB ()))))))))