Bug 162 - Formally Verify the FSGNJ module
Summary: Formally Verify the FSGNJ module
Status: PAYMENTPENDING FIXED
Alias: None
Product: Libre-SOC's first SoC
Classification: Unclassified
Component: Formal Verification (show other bugs)
Version: unspecified
Hardware: PC Linux
: --- enhancement
Assignee: Michael Nolan
URL:
Depends on:
Blocks: 196
  Show dependency tree / graph
 
Reported: 2020-01-31 14:15 GMT by Michael Nolan
Modified: 2022-10-07 20:07 BST (History)
2 users (show)

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

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 Michael Nolan 2020-01-31 14:15:45 GMT 
A formal proof for the FSGNJ module has been created here: https://git.libre-riscv.org/?p=ieee754fpu.git;a=blob;f=src/ieee754/fsgnj/formal/proof_fsgnj_mod.py;h=b960a85c111c0caee39b99eded831d86b02903ad;hb=HEAD

The proof can be run by the following command:

python -m ieee754.fsgnj.formal.proof_fsgnj_mod