Bug 1036 - Formal Proof for LDSTCompUnit is needed
Summary: Formal Proof for LDSTCompUnit is needed
Alias: None
Product: Libre-SOC's first SoC
Classification: Unclassified
Component: Formal Verification (show other bugs)
Version: unspecified
Hardware: PC Linux
: --- enhancement
Assignee: Cesar Strauss
Depends on:
Reported: 2023-03-19 11:33 GMT by Luke Kenneth Casson Leighton
Modified: 2023-10-11 15:22 BST (History)
2 users (show)

See Also:
NLnet milestone: NLnet.2022-08-107.ongoing
total budget (EUR) for completion of task and all subtasks: 3000
budget (EUR) for this task, excluding subtasks' budget: 3000
parent task for budget allocation: 961
child tasks for budget allocation:
The table of payments (in EUR) for this task; TOML format:
cesar=2400 lkcl=600


Note You need to log in before you can comment on or make changes to this bug.
Description Luke Kenneth Casson Leighton 2023-03-19 11:33:20 GMT
the ALU CompUnit Formal Proof was very successful and tracked
down a critical bug.  a similar proof is needed for LDSTCompUnit.