Bug 1036 - Formal Proof for LDSTCompUnit is needed
Summary: Formal Proof for LDSTCompUnit is needed
Status: CONFIRMED
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
URL:
Depends on:
Blocks:
 
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

Attachments
Add an attachment (proposed patch, testcase, etc.)

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.