[Libre-soc-bugs] [Bug 909] Formal proof of nmutil/plru.py

[bugzilla-daemon at libre-soc.org]

https://bugs.libre-soc.org/show_bug.cgi?id=909

--- Comment #1 from Jacob Lifshay <programmerjake at gmail.com> ---
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.

-- 
You are receiving this mail because:
You are on the CC list for the bug.