[Libre-soc-bugs] [Bug 868] New: Formal verification of fadd/fsub

[bugzilla-daemon at libre-soc.org]

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

            Bug ID: 868
           Summary: Formal verification of fadd/fsub
           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: 196
   NLnet milestone: NLNet.2019.10.032.Formal
    parent task for 196
 budget allocation:

Steps:
* f16:
    * DONE: formal verification of fadd for just
      round-nearest-ties-to-even where NaNs are not distinguished from
      each other and exception flags/traps aren't checked
https://git.libre-soc.org/?p=ieee754fpu.git;a=commitdiff;h=98bf485dc96efc74e259809ad2829ccad6324cd4
    * TODO: formal verification of correct NaN propagation/generation
    * TODO: formal verification of all rounding modes
        * Blocked on implementing other rounding modes in the fadd pipeline
    * TODO: formal verification of exception flags/traps
        * Blocked on implementing exception flags/traps in the fadd pipeline
    * TODO: formal verification of fsub
        * Blocked on adding fsub support to the fadd pipeline
* f32:
    * TODO: formal verification of fadd for just
      round-nearest-ties-to-even where NaNs are not distinguished from
      each other and exception flags/traps aren't checked
    * TODO: formal verification of correct NaN propagation/generation
    * TODO: formal verification of all rounding modes
        * Blocked on implementing other rounding modes in the fadd pipeline
    * TODO: formal verification of exception flags/traps
        * Blocked on implementing exception flags/traps in the fadd pipeline
    * TODO: formal verification of fsub
        * Blocked on adding fsub support to the fadd pipeline
* f64:
    * TODO: formal verification of fadd for just
      round-nearest-ties-to-even where NaNs are not distinguished from
      each other and exception flags/traps aren't checked
    * TODO: formal verification of correct NaN propagation/generation
    * TODO: formal verification of all rounding modes
        * Blocked on implementing other rounding modes in the fadd pipeline
    * TODO: formal verification of exception flags/traps
        * Blocked on implementing exception flags/traps in the fadd pipeline
    * TODO: formal verification of fsub
        * Blocked on adding fsub support to the fadd pipeline


Referenced Bugs:

https://bugs.libre-soc.org/show_bug.cgi?id=196
[Bug 196] Formal correctness proof needed for the IEEE754 FPU
https://bugs.libre-soc.org/show_bug.cgi?id=835
[Bug 835] add support for smtlib2 floating-point to yosys and nmigen
-- 
You are receiving this mail because:
You are on the CC list for the bug.