From 1d8731ee5b33adb6840fa8532465bf6ff39a7c8b Mon Sep 17 00:00:00 2001 From: Tim Hutt Date: Tue, 28 Nov 2023 13:22:45 +0000 Subject: [PATCH] Constrain TLB struct bit sizes Constraining them to <= 64 bits generates code that doesn't use GMP and is therefore much faster. This massively increases C emulation performance. --- model/riscv_vmem_tlb.sail | 17 ++++++++++++----- 1 file changed, 12 insertions(+), 5 deletions(-) diff --git a/model/riscv_vmem_tlb.sail b/model/riscv_vmem_tlb.sail index 27b63ba37..6a970b566 100644 --- a/model/riscv_vmem_tlb.sail +++ b/model/riscv_vmem_tlb.sail @@ -68,9 +68,13 @@ /* SUCH DAMAGE. */ /*=======================================================================================*/ -/* idealized generic TLB entry to model fence.vm and also speed up simulation. */ +/* Idealized generic TLB entry to model fence.vm and also speed up simulation. + * The type size constraints allow Sail to use uint64 which is much faster than + * bigints. + */ -struct TLB_Entry('asidlen: Int, 'valen: Int, 'palen: Int, 'ptelen: Int) = { +struct TLB_Entry('asidlen: Int, 'valen: Int, 'palen: Int, 'ptelen: Int), + 'asidlen <= 64 & 'valen <= 64 & 'palen <= 64 & 'ptelen <= 64 = { asid : bits('asidlen), global : bool, vAddr : bits('valen), /* VPN */ @@ -83,7 +87,8 @@ struct TLB_Entry('asidlen: Int, 'valen: Int, 'palen: Int, 'ptelen: Int) = { } -val make_TLB_Entry : forall 'asidlen 'valen 'palen 'ptelen, 'valen > 0. +val make_TLB_Entry : forall 'asidlen 'valen 'palen 'ptelen, + 'asidlen <= 64 & 'valen <= 64 & 'palen <= 64 & 'ptelen <= 64 & 'valen > 0. (bits('asidlen), bool, bits('valen), bits('palen), bits('ptelen), nat, bits('palen), nat) -> TLB_Entry('asidlen, 'valen, 'palen, 'ptelen) function make_TLB_Entry(asid, global, vAddr, pAddr, pte, level, pteAddr, levelBitSize) = { @@ -104,13 +109,15 @@ function make_TLB_Entry(asid, global, vAddr, pAddr, pte, level, pteAddr, levelBi } } -val match_TLB_Entry : forall 'asidlen 'valen 'palen 'ptelen. +val match_TLB_Entry : forall 'asidlen 'valen 'palen 'ptelen, + 'asidlen <= 64 & 'valen <= 64 & 'palen <= 64 & 'ptelen <= 64. (TLB_Entry('asidlen, 'valen, 'palen, 'ptelen), bits('asidlen), bits('valen)) -> bool function match_TLB_Entry(ent, asid, vaddr) = (ent.global | (ent.asid == asid)) & (ent.vAddr == (ent.vMatchMask & vaddr)) -val flush_TLB_Entry : forall 'asidlen 'valen 'palen 'ptelen. +val flush_TLB_Entry : forall 'asidlen 'valen 'palen 'ptelen, + 'asidlen <= 64 & 'valen <= 64 & 'palen <= 64 & 'ptelen <= 64. (TLB_Entry('asidlen, 'valen, 'palen, 'ptelen), option(bits('asidlen)), option(bits('valen))) -> bool function flush_TLB_Entry(e, asid, addr) = {