[Libre-soc-bugs] [Bug 876] New: Implement and Add Formal Proof for fsub in the fpadd pipeline

[bugzilla-daemon at libre-soc.org]

https://bugs.libre-soc.org/show_bug.cgi?id=876

            Bug ID: 876
           Summary: Implement and Add Formal Proof for fsub in the fpadd
                    pipeline
           Product: Libre-SOC's first SoC
           Version: unspecified
          Hardware: PC
                OS: Linux
            Status: IN_PROGRESS
          Severity: enhancement
          Priority: ---
         Component: Formal Verification
          Assignee: programmerjake at gmail.com
          Reporter: programmerjake at gmail.com
                CC: libre-soc-bugs at lists.libre-soc.org,
                    programmerjake at gmail.com
        Depends on: 835
            Blocks: 868
   NLnet milestone: NLNet.2019.10.032.Formal
 total budget (EUR) 500
  for completion of
       task and all
          subtasks:
   budget (EUR) for 500
         this task,
          excluding
  subtasks' budget:
    parent task for 196
 budget allocation:
       The table of jacob=500
  payments (in EUR)
     for this task;
       TOML format:

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.


Referenced Bugs:

https://bugs.libre-soc.org/show_bug.cgi?id=835
[Bug 835] add support for smtlib2 floating-point to yosys and nmigen
https://bugs.libre-soc.org/show_bug.cgi?id=868
[Bug 868] Formal verification of fadd/fsub
-- 
You are receiving this mail because:
You are on the CC list for the bug.