Bug 163

Summary: Formally Verify the FPMAX module
Product: Libre-SOC's first SoC Reporter: Michael Nolan <mtnolan2640>
Component: Formal VerificationAssignee: Michael Nolan <mtnolan2640>
Status: PAYMENTPENDING FIXED    
Severity: enhancement CC: libre-soc-bugs, lkcl
Priority: ---    
Version: unspecified   
Hardware: PC   
OS: Linux   
NLnet milestone: NLNet.2019.10.032.Formal total budget (EUR) for completion of task and all subtasks: 150
budget (EUR) for this task, excluding subtasks' budget: 150 parent task for budget allocation: 196
child tasks for budget allocation: The table of payments (in EUR) for this task; TOML format:
mnolan={amount=150, paid=2020-05-01}
Bug Depends on:    
Bug Blocks: 196    

Description Michael Nolan 2020-01-31 14:18:10 GMT
A formal proof for the fpmax module has been created here: https://git.libre-riscv.org/?p=ieee754fpu.git;a=blob;f=src/ieee754/fpmax/formal/proof_fmax_mod.py;h=700811963a89b4608d87b2d34791d392ddb60d6d;hb=HEAD

It can be run by running: python -m ieee754.fpmax.formal.proof_fmax_mod