[Libre-soc-bugs] [Bug 869] New: Formal verification of fadd for just round-nearest-ties-to-even without exception flags/traps

[bugzilla-daemon at libre-soc.org]

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

            Bug ID: 869
           Summary: Formal verification of fadd for just
                    round-nearest-ties-to-even 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 868
 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
* 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
* 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


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.