[Libre-soc-bugs] [Bug 835] add support for smtlib2 floating-point to yosys and nmigen

[bugzilla-daemon at libre-soc.org]

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

Luke Kenneth Casson Leighton <lkcl at lkcl.net> changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
                 CC|                            |lkcl at lkcl.net

--- Comment #1 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
helpful insights from jix on yosys irc:

<lkcl> Float16 (and Float32) isn't recognised by yosys. that's what we have to
"pass through" in some easy form that doesn't involve a massive amount of work
<jix> why not use blackbox modules for the fp primitives you need that use
normal signals (i.e. BitVecs) for their ports and supply your own smt2
definition for them that internally can convert to floating point types?
<jix> that would only need small changes to sby to allow adding user smt2
statements but no changes to yosys or smtbmc
<jix> lkcl: also fwiw bitwuzla using kissat as SAT backend solves
fp16mul_test.smt2 a lot faster than z3 (after inlining f16_to_fp and changing
all (define-const foo ...) to (define-fun foo () ...) to make bitwuzla's parser
happy)
<jix> kissat upstream doesn't support incremental solving yet, but I do have
experimental patches for kissat to add that (and a patch to bitwuzla to enable
that)
<jix> but incremental solving isn't needed for this smt2 file and for smtbmc
it's optional (there's a -noincr option)
<jix> and bitwuzla with cadical (default SAT backend) is probably still faster
than z3
<jix> not convinced that bitwuzla can crack the 32-bit float version, though,
but I'm curious so I'll let it run overnight

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