because PLRU messed up the input (should have been log2 of way count), copy plru.py to plru2.py, fix in plru2.py, write formal proof (this bug), then later (as a different bug) migrate all uses to plru2.py, then rename plru2.py back to plru.py and change all imports back. 2**BITS mistranslated to nmigen as 2*BITS https://github.com/antonblanchard/microwatt/blob/050185e2caabfb7a0ec11a433955fca18781d83a/plru.vhdl#L22 https://git.libre-soc.org/?p=nmutil.git;a=blob;f=src/nmutil/plru.py;h=80c67571d42adcc48925181116acf23e445c1548;hb=6e8678a9beabcc1577a1d789a211c0272fda10f6#l34 DONE: PLRU formal proof: https://git.libre-soc.org/?p=nmutil.git;a=blob;f=src/nmutil/formal/test_plru.py;hb=HEAD
I retranslated microwatt's plru.vhdl and added a formal proof, then added a simulation too... The translation has 2 differences from microwatt: 1. microwatt has the `tree` array have 2**BITS entries, even though it doesn't use the last entry. I shortened that in my translation, though it isn't really an issue. 2. microwatt seems to access `tree` with the wrong `node` (multiplied by 2 even though it shouldn't yet be), assuming vhdl's semantics behave like I expect. I fixed that in my translation by introducing a `val` temporary that is assigned before `node` is modified. https://github.com/antonblanchard/microwatt/blob/f67b1431655c291fc1c99857a5c1ef624d5b264c/plru.vhdl#L41 https://git.libre-soc.org/?p=nmutil.git;a=blob;f=src/nmutil/plru2.py;h=d766f6c16b44ea7e5b4c2952a09c9f6004b1431e;hb=0759ba7a4a56812e195ee324bf87855084797ec0#l84 This is a bug in microwatt afaict, I'll be submitting an issue shortly.
(In reply to Jacob Lifshay from comment #1) > This is a bug in microwatt afaict, I'll be submitting an issue shortly. microwatt issue: https://github.com/antonblanchard/microwatt/issues/398
(In reply to Jacob Lifshay from comment #1) > I retranslated microwatt's plru.vhdl and added a formal proof, then added a > simulation too... nicely done > This is a bug in microwatt afaict, I'll be submitting an issue shortly. i think they'll really appreciate that. the TLBs get 64 plrus allocated so it is not a small resource allocation.
PLRUs is just an array of PLRU, not going to worry about it. closing, good job
actually, i want to modify PLRU's API somewhat so you can have a sram of PLRU states and just one PLRU circuit rather than a bunch of dffs and PLRUs. the sram would need 1 clocked write port and one combinatorial read port (unless you want to wait an extra cycle), it would be external to PLRU. so please don't close this one just yet
that doesn't affect the fact that the proof is written and passes so as far as the purpose of this bugreport is concerned it is 100% completed. if you wish to make enhancements beyond what was asked for that is fine but out of scope for this completed and 100% finished task.
(In reply to Luke Kenneth Casson Leighton from comment #3) > > This is a bug in microwatt afaict, I'll be submitting an issue shortly. > > i think they'll really appreciate that. the TLBs get 64 > plrus allocated so it is not a small resource allocation. Fix just merged into microwatt: https://github.com/antonblanchard/microwatt/pull/399