Bug 876 - Implement and Add Formal Proof for fsub in the fpadd pipeline
Summary: Implement and Add Formal Proof for fsub in the fpadd pipeline
Status: RESOLVED FIXED
Alias: None
Product: Libre-SOC's first SoC
Classification: Unclassified
Component: Formal Verification (show other bugs)
Version: unspecified
Hardware: PC Linux
: --- enhancement
Assignee: Jacob Lifshay
URL:
Depends on: 835
Blocks: 868
  Show dependency tree / graph
 
Reported: 2022-07-01 06:16 BST by Jacob Lifshay
Modified: 2022-07-22 05:10 BST (History)
3 users (show)

See Also:
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

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 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.