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 * DONE: formal verification of correct NaN propagation/generation * DONE: formal verification of all rounding modes * TODO: formal verification of exception flags/traps * Blocked on implementing exception flags/traps in the fadd pipeline * DONE: formal verification of fsub * f32 (if smt solver can handle it): * 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 * DONE: formal verification of correct NaN propagation/generation * DONE: formal verification of all rounding modes * TODO: formal verification of exception flags/traps * Blocked on implementing exception flags/traps in the fadd pipeline * DONE: formal verification of fsub * f64 (if smt solver can handle it): * 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 * TODO: formal verification of exception flags/traps * Blocked on implementing exception flags/traps in the fadd pipeline * TODO: formal verification of fsub
from irc: https://libre-soc.org/irclog/%23libre-soc.2022-06-25.log.html#t2022-06-25T09:42:15 lkcl programmerjake, it's perfectly fine to cut this back drastically 09:42 lkcl https://bugs.libre-soc.org/show_bug.cgi?id=868 09:42 lkcl we absolutely don't have time to do that much work 09:44 lkcl so i'm cutting it back, the budget doesn't change 09:45 lkcl we *need* to set goals that are *achievable within the timeframe* 09:45 lkcl then apply for follow-up grants afterwards 09:46 lkcl and make certain that the available budget right now is 100% allocated and spent on *achievable* tasks within the remaining 12 weeks 09:46 lkcl which makes 869 80% done already 09:48 lkcl i've allocated EUR 2500 to 868, which leaves EUR 2650 remaining to allocate, e.g. to fmul16, and i'd say we're good
(In reply to Jacob Lifshay from comment #1) > from irc: > https://libre-soc.org/irclog/%23libre-soc.2022-06-25.log.html#t2022-06-25T09: > 42:15 > lkcl programmerjake, it's perfectly fine to cut this back drastically 09:42 imho we need to get all of that done wether or not we can finish on-time since it's required by the power isa spec. if you don't think it can be completed by the end of the formal proofs grant, just cut this bug out of the funding tree... #869 is intended to be the bug that can be completed quickly.
also, you had cut out f32/f64 because you thought it'd be too slow...imho it should be fine since it's add, not mul.
(In reply to Jacob Lifshay from comment #2) > imho we need to get all of that done wether or not we can finish on-time > since it's required by the power isa spec. under different (follow-up) grant. get work done, get it done fast, get the RFP in, focus on what the spec says *after* October 1st.
(In reply to Luke Kenneth Casson Leighton from comment #4) > (In reply to Jacob Lifshay from comment #2) > > > imho we need to get all of that done wether or not we can finish on-time > > since it's required by the power isa spec. > > under different (follow-up) grant. > > get work done, get it done fast, get the RFP in, focus on what > the spec says *after* October 1st. then cut this bug out of the funding tree...change #869 so that it has #196 as a budget parent task (don't change Blocks though). change this bug to just track what needs to be done, irrespective of grants/funding/etc. i can do that if you're ok with it...
(In reply to Jacob Lifshay from comment #5) > i can do that if you're ok with it... yep go for it.