[Libre-soc-bugs] [Bug 874] New: Implementation and Formal verification of fadd for all rounding modes but without exception flags/traps

[bugzilla-daemon at libre-soc.org]

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

            Bug ID: 874
           Summary: Implementation and Formal verification of fadd for all
                    rounding modes but without exception flags/traps
           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
    parent task for 196
 budget allocation:

* f16:
    * WIP: implement other rounding modes in the fadd pipeline
        I already added support to fpbase.Overflow to add all the rounding
        modes, now I just need to pass the rounding mode in through all the
        pipeline stages.
    * TODO: formal verification of all rounding modes
* f32 (if smt solver can handle it):
    * WIP: implement other rounding modes in the fadd pipeline
    * TODO: formal verification of all rounding modes
* f64 (if smt solver can handle it):
    * WIP: implement other rounding modes in the fadd pipeline
    * TODO: formal verification of all rounding modes


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.