Bug 1036

Summary: Formal Proof for LDSTCompUnit is needed
Product: Libre-SOC's first SoC Reporter: Luke Kenneth Casson Leighton <lkcl>
Component: Formal VerificationAssignee: Cesar Strauss <cestrauss>
Status: CONFIRMED ---    
Severity: enhancement CC: libre-soc-bugs, toshaan
Priority: ---    
Version: unspecified   
Hardware: PC   
OS: Linux   
See Also: https://bugs.libre-soc.org/show_bug.cgi?id=350
https://bugs.libre-soc.org/show_bug.cgi?id=318
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

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.