| Summary: | Formal proof of nmutil/plru.py | ||
|---|---|---|---|
| Product: | Libre-SOC's first SoC | Reporter: | Jacob Lifshay <programmerjake> |
| Component: | Formal Verification | Assignee: | Jacob Lifshay <programmerjake> |
| Status: | RESOLVED FIXED | ||
| Severity: | enhancement | CC: | libre-soc-bugs, lkcl, programmerjake |
| Priority: | --- | ||
| Version: | unspecified | ||
| Hardware: | PC | ||
| OS: | Linux | ||
| See Also: | https://bugs.libre-soc.org/show_bug.cgi?id=913 | ||
| NLnet milestone: | --- | total budget (EUR) for completion of task and all subtasks: | 0 |
| budget (EUR) for this task, excluding subtasks' budget: | 0 | parent task for budget allocation: | |
| child tasks for budget allocation: | The table of payments (in EUR) for this task; TOML format: | ||
| Bug Depends on: | |||
| Bug Blocks: | 198 | ||
|
Description
Jacob Lifshay
2022-08-18 07:27:41 BST
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 |