Bug 876

Summary:	Implement and Add Formal Proof for fsub in the fpadd pipeline
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:	NLNet.2019.10.032.Formal	total budget (EUR) for completion of task and all subtasks:	500
budget (EUR) for this task, excluding subtasks' budget:	500	parent task for budget allocation:	196
child tasks for budget allocation:		The table of payments (in EUR) for this task; TOML format:	[jacob] amount = 500 submitted = 2022-07-06 paid = 2022-07-21
Bug Depends on:	835
Bug Blocks:	868

Description Jacob Lifshay 2022-07-01 06:16:46 BST

Added is_sub signal and extended formal proof to check subtraction works correctly:
https://git.libre-soc.org/?p=ieee754fpu.git;a=commit;h=5b37dceef588adc9f544c76da2ec2441f2aade7f

lkcl, please let me know if you think the budget is fine.

Comment 1 Luke Kenneth Casson Leighton 2022-07-01 08:28:54 BST

(In reply to Jacob Lifshay from comment #0)
> Added is_sub signal and extended formal proof to check subtraction works
> correctly:
> https://git.libre-soc.org/?p=ieee754fpu.git;a=commit;
> h=5b37dceef588adc9f544c76da2ec2441f2aade7f
> 
> lkcl, please let me know if you think the budget is fine.

looks really good.