| Max Depth: |
Bug 196 depends on 10 bugs:
view as bug list-
196:
Formal correctness proof needed for the IEEE754 FPU
[RESOLVED FIXED; assigned to lkcl]
-
596:
formal correctness proof for nmigen integration of Dynamic Partitioned Signal
[CONFIRMED; assigned to mail]
-
868:
Formal verification of fadd/fsub
[IN_PROGRESS; assigned to programmerjake]
-
835:
add support for smtlib2 floating-point to yosys and nmigen
[RESOLVED FIXED; assigned to programmerjake]
-
869:
Formal verification of fadd for just round-nearest-ties-to-even without exception flags/traps
[RESOLVED FIXED; assigned to programmerjake]
-
874:
Implementation and Formal verification of fadd for all rounding modes but without exception flags/traps
[RESOLVED FIXED; assigned to programmerjake]
-
876:
Implement and Add Formal Proof for fsub in the fpadd pipeline
[RESOLVED FIXED; assigned to programmerjake]
-
835:
add support for smtlib2 floating-point to yosys and nmigen
[RESOLVED FIXED; assigned to programmerjake]
-
162:
Formally Verify the FSGNJ module
[PAYMENTPENDING FIXED; assigned to mtnolan2640]
-
163:
Formally Verify the FPMAX module
[PAYMENTPENDING FIXED; assigned to mtnolan2640]
-
165:
Formally verify the FPCMP (FEQ, FLE, FLT) module
[PAYMENTPENDING FIXED; assigned to mtnolan2640]
-
835:
add support for smtlib2 floating-point to yosys and nmigen
[RESOLVED FIXED; assigned to programmerjake]
(*)
-
877:
implementation and formal correctness proof for fp fused-mul-add pipeline excluding ieee754 exception flags
[RESOLVED FIXED; assigned to programmerjake]
-
596:
formal correctness proof for nmigen integration of Dynamic Partitioned Signal
[CONFIRMED; assigned to mail]
Bug 196 blocks 4 bugs:
view as bug list-
196:
Formal correctness proof needed for the IEEE754 FPU
[RESOLVED FIXED; assigned to lkcl]
| Max Depth: |