@@ -27,17 +27,37 @@ struct TLB_Entry = {
2727 age : bits (64 ) // for replacement policy?
2828}
2929
30- // Single-entry TLB (could enlarge this in future for better simulation speed)
30+ // 64 entries is based on benchmarks of Linux boots and is where you stop
31+ // seeing performance improvements.
32+ type num_tlb_entries : Int = 64
33+ type tlb_index_range = range (0 , num_tlb_entries - 1 )
34+
3135// PRIVATE
32- register tlb : option (TLB_Entry ) = None ()
36+ register tlb : vector (num_tlb_entries , option (TLB_Entry )) = [
37+ None (), None (), None (), None (), None (), None (), None (), None (),
38+ None (), None (), None (), None (), None (), None (), None (), None (),
39+ None (), None (), None (), None (), None (), None (), None (), None (),
40+ None (), None (), None (), None (), None (), None (), None (), None (),
41+ None (), None (), None (), None (), None (), None (), None (), None (),
42+ None (), None (), None (), None (), None (), None (), None (), None (),
43+ None (), None (), None (), None (), None (), None (), None (), None (),
44+ None (), None (), None (), None (), None (), None (), None (), None (),
45+ ]
46+
47+ // Indexed by the lowest bits of the VPN.
48+ function tlb_hash (vaddr : bits (64 )) -> tlb_index_range =
49+ unsigned (vaddr [17 .. 12 ])
3350
3451// PUBLIC: invoked in init_vmem() [riscv_vmem.sail]
35- function init_TLB () -> unit =
36- tlb = None ()
52+ function init_TLB () -> unit = {
53+ foreach (i from 0 to (length (tlb ) - 1 )) {
54+ tlb [i ] = None ();
55+ }
56+ }
3757
3858// PUBLIC: invoked in translate_TLB_hit() [riscv_vmem.sail]
39- function write_TLB (idx : nat , ent : TLB_Entry ) -> unit =
40- tlb = Some (ent )
59+ function write_TLB (index : tlb_index_range , ent : TLB_Entry ) -> unit =
60+ tlb [ index ] = Some (ent )
4161
4262// PRIVATE
4363function match_TLB_Entry (ent : TLB_Entry ,
@@ -60,11 +80,13 @@ function flush_TLB_Entry(e : TLB_Entry,
6080}
6181
6282// PUBLIC: invoked in translate() [riscv_vmem.sail]
63- function lookup_TLB (asid : asidbits , vaddr : bits (64 )) -> option ((nat , TLB_Entry )) =
64- match tlb {
65- None () => None (),
66- Some (e ) => if match_TLB_Entry (e , asid , vaddr ) then Some ((0 , e )) else None ()
83+ function lookup_TLB (asid : asidbits , vaddr : bits (64 )) -> option ((tlb_index_range , TLB_Entry )) = {
84+ let index = tlb_hash (vaddr );
85+ match tlb [index ] {
86+ None () => None (),
87+ Some (entry ) => if match_TLB_Entry (entry , asid , vaddr ) then Some ((index , entry )) else None (),
6788 }
89+ }
6890
6991// PRIVATE
7092function add_to_TLB (asid : asidbits ,
@@ -75,21 +97,28 @@ function add_to_TLB(asid : asidbits,
7597 level : nat ,
7698 global : bool ,
7799 levelBitSize : nat ,
78- PAGESIZE_BITS : nat ) -> unit = {
79- let shift = PAGESIZE_BITS + (level * levelBitSize );
100+ pagesize_bits : nat ) -> unit = {
101+ let shift = pagesize_bits + (level * levelBitSize );
80102 assert (shift <= 64 );
81103 let vAddrMask : bits (64 ) = zero_extend (ones (shift ));
82104 let vMatchMask : bits (64 ) = ~ (vAddrMask );
83- let entry : TLB_Entry = struct {asid = asid ,
84- global = global ,
85- pte = pte ,
86- pteAddr = pteAddr ,
87- vAddrMask = vAddrMask ,
88- vMatchMask = vMatchMask ,
89- vAddr = vAddr & vMatchMask ,
90- pAddr = shiftl (shiftr (pAddr , shift ), shift ),
91- age = mcycle };
92- tlb = Some (entry )
105+
106+ let entry : TLB_Entry = struct {asid = asid ,
107+ global = global ,
108+ pte = pte ,
109+ pteAddr = pteAddr ,
110+ vAddrMask = vAddrMask ,
111+ vMatchMask = vMatchMask ,
112+ vAddr = vAddr & vMatchMask ,
113+ pAddr = pAddr & vMatchMask ,
114+ age = mcycle };
115+
116+ // Add the TLB entry. Note that this may be a super-page, but we still want
117+ // to add it to the index corresponding to the page because that is how
118+ // lookup_TLB looks it up. For superpages will just end up with the same
119+ // TLB entry in multiple slots.
120+ let index = tlb_hash (vAddr );
121+ tlb [index ] = Some (entry );
93122}
94123
95124// Top-level TLB flush function
@@ -106,10 +135,10 @@ function flush_TLB(asid_xlen : option(xlenbits),
106135 None () => None (),
107136 Some (a ) => Some (zero_extend (a ))
108137 };
109- match tlb {
110- None () => () ,
111- Some (e ) => if flush_TLB_Entry (e , asid , addr_64b )
112- then tlb = None ()
113- else ()
138+ foreach ( i from 0 to ( length ( tlb ) - 1 )) {
139+ match tlb [ i ] {
140+ Some (e ) => if flush_TLB_Entry (e , asid , addr_64b ) then { tlb [ i ] = None (); } ,
141+ None () => () ,
142+ }
114143 }
115144}
0 commit comments