[Libre-soc-bugs] [Bug 196] Formal correctness proof needed for the IEEE754 FPU

[bugzilla-daemon at libre-soc.org]

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

--- Comment #22 from Jacob Lifshay <programmerjake at gmail.com> ---
(In reply to Jacob Lifshay from comment #21)
> (In reply to Luke Kenneth Casson Leighton from comment #17)
> > (In reply to Jacob Lifshay from comment #13)
> >     
> > >     It's probably correct, z3 ran longer than I bothered to wait, it usually
> > > stops relatively quickly if there's an error in the logic.
> > 
> > yes, mul is awful.  fpadd would have been much faster
> 
> I specifically chose fmul because it's slower...the idea is that if fmul is
> feasible, nearly everything we'd want to implement will be feasible.

I ran z3 for 84min on my phone, it still didn't finish. imho it's not feasible
for at least z3 4.8.17.

imho we should try it on other smt engines, they may work faster.

one other option worth trying is figuring out how to export the hw into coq
format, since coq allows interactive proofs -- aka it'll ask a human (or a file
we write containing the expected answers) for help when it gets stuck. coq
should work much better than most smt engines since they tend to end up
brute-forcing it when they're stuck, which only works for simple cases.

-- 
You are receiving this mail because:
You are on the CC list for the bug.