AdamHorden has quit [Remote host closed the connection]
AdamHorden has joined #yosys
AdamHorden has quit [Quit: Adam Horden]
AdamHorden has joined #yosys
AdamHorden has quit [Client Quit]
AdamHorden has joined #yosys
AdamHorden has quit [Remote host closed the connection]
AdamHorden has joined #yosys
AdamHorden has quit [Client Quit]
AdamHorden has joined #yosys
FabM has joined #yosys
FabM has joined #yosys
FabM has quit [Changing host]
emeb_mac has joined #yosys
AdamHorden has quit [Quit: Adam Horden]
AdamHorden has joined #yosys
AdamHorden has quit [Quit: Adam Horden]
AdamHorden has joined #yosys
AdamHorden has quit [Quit: Adam Horden]
AdamHorden has joined #yosys
benreynwar_ has joined #yosys
SpaceCoaster_ has joined #yosys
Moe_Icenowy has joined #yosys
mithro_ has joined #yosys
Knarfian______ has joined #yosys
dnm_ has joined #yosys
freshmaker666 has joined #yosys
anticw_ has joined #yosys
mathu_ has joined #yosys
shorne_ has joined #yosys
shoragan_ has joined #yosys
cyrozap-ZNC has joined #yosys
pepijndevos[m] has quit [*.net *.split]
shorne has quit [*.net *.split]
benreynwar has quit [*.net *.split]
shoragan has quit [*.net *.split]
SpaceCoaster has quit [*.net *.split]
Knarfian_____ has quit [*.net *.split]
mithro has quit [*.net *.split]
MoeIcenowy has quit [*.net *.split]
cyrozap has quit [*.net *.split]
anticw has quit [*.net *.split]
mathu has quit [*.net *.split]
greeb has quit [*.net *.split]
dnm has quit [*.net *.split]
benreynwar_ is now known as benreynwar
SpaceCoaster_ is now known as SpaceCoaster
Knarfian______ is now known as Knarfian_____
dnm_ is now known as dnm
mithro_ is now known as mithro
pepijndevos[m] has joined #yosys
ec has joined #yosys
emeb has joined #yosys
FabM has quit [Quit: Leaving]
smkz has quit [Quit: reboot@]
smkz has joined #yosys
kraiskil has joined #yosys
smkz has quit [Quit: reboot@]
smkz has joined #yosys
kraiskil has quit [Ping timeout: 248 seconds]
cr1901_ has joined #yosys
<lkcl>
btw in case anyone's interested, we're doing a Formal Correctness Proof of IEEE754 (using FP16 as the base because z3 wouldn't complete on FP32)
<lkcl>
and would like to do that in nmigen / yosys
<lkcl>
however
<lkcl>
yosys does not support BitVector which is what's needed to be passed-through, soooo....
<lkcl>
as a first-pass "hack", the plan is to add properties - as strings - to be passed through to sby/z3/smt2
cr1901 has quit [Ping timeout: 248 seconds]
<lkcl>
(because adding BitVectors as a "proper" - full - type to yosys is one hell of a lot of work)
<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
kraiskil has joined #yosys
kraiskil has quit [Client Quit]
<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
kraiskil has joined #yosys
<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)
cr1901_ is now known as cr1901
<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
kraiskil has quit [Ping timeout: 246 seconds]
<jix>
not convinced that bitwuzla can crack the 32-bit float version, though, but I'm curious so I'll let it run overnight
<qball>
a few days runtime should still be ok as long as it finishes.
<qball>
(with a useful result :D_
<jix>
sometimes it's really hard to tell whether it's still making progress though
<qball>
that is why you launch it on a server, forget about it while being busy, and remember a few days later
<qball>
(that happens to me from time to time)
<jix>
yeah but even then you don't know if it would finish if you give it another week
<qball>
yeah,
emeb has left #yosys [#yosys]
<lkcl>
jix: ooo, niice.
<lkcl>
i set -v:3 on z3 and it gave me some reasonable progress notification
<lkcl>
cvc5 on the other hand: nothing :)
<jix>
heh, I think even z3's status output is rather useless to figure out if it is worth to keep it running
<jix>
I find cadical's or kissat's output (very similar) much more useful, but part of that is probably familiarity
<lkcl>
jix: i'm pinging programmerjake because he's the one working on this, let's see if he joins this channel
<jix>
but even if it looks like progress, it might just move asymptotically to a place where it's stuck for all practical purposes
<lkcl>
jix, no totally appreciated about the speedup, all these tools they're actually really hard to find: they don't come up in searches
<programmerjake>
jix: my idea for how to add support for fp and real numbers and integers in smtlib2 to yosys is to add a new builtin cell that is an arbitrary smtlib2 expression but restricted so all inputs/outputs are bools/bitvectors.
<programmerjake>
also maybe adding a way to include intermediate smtlib2 values in the vcd generated by symbi-yosys even if those values aren't bitvectors since it will be really useful for debugging why a formal proof failed
<programmerjake>
the reason not to just have a cell for each fp primitive is we also want to use real numbers for stuff like fp sin and reals can't be losslessly stored in a bitvector
<jix>
ah that wasn't what I was trying to suggest
<programmerjake>
(assuming you don't want to encode the primitive polynomial and bounds for the algebraic number as a bitstring and hope your bitvector is long enough)
<jix>
you can already use arbitrary smt2 constraints, as long as the interface to is all bitvectors, without adding any new cells to yosys
<jix>
write_smt2 doesn't generate any smtlib code for modules with the blackbox attribute, so you can supply your own for those
<jix>
currently you still need to manually concat that to write_smt2's output and make sure it's defining things as documented in write_smt2's help
<programmerjake>
ah, I wanted to put it through yosys so manually concatenating isn't necessary.
<programmerjake>
also so yosys can take care of naming and stuff so I don't have to re-implement that
<jix>
yeah I can see how that's more convenient, I'm not sure that adding a custom cell is the best approach though
cr1901_ has joined #yosys
cr1901 has quit [Read error: Connection reset by peer]