| Summary: | Formal proof for nmutil byterev.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 | ||
| 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-04 08:08:53 BST
Finished formal proof. https://git.libre-soc.org/?p=nmutil.git;a=blob;f=src/nmutil/formal/test_byterev.py;h=6df71bda009411ae8390bde879f11e0928fac616;hb=02ce4630db0814025c25a97d38f9a9357062bca3 byte_reverse zeroing everything other than the `length` least-significant bits threw me off for a while...I added a note to the docs specifically pointing that out so others don't get confused. (In reply to Jacob Lifshay from comment #1) > byte_reverse zeroing everything other than the `length` least-significant > bits threw me off for a while...I added a note to the docs specifically > pointing that out so others don't get confused. ah good, yes sensible. breaking expectations bad. |