| *** tpb <[email protected]> has joined #yosys | 00:00 | |
| *** Xark <[email protected]> has joined #yosys | 01:01 | |
| *** msh <[email protected]> has quit IRC (Ping timeout: 248 seconds) | 02:57 | |
| *** srk- <srk-!~sorki@user/srk> has joined #yosys | 03:28 | |
| *** srk <srk!~sorki@user/srk> has quit IRC (Ping timeout: 252 seconds) | 03:29 | |
| *** srk- is now known as srk | 03:31 | |
| *** srk- <srk-!~sorki@user/srk> has joined #yosys | 03:41 | |
| *** srk <srk!~sorki@user/srk> has quit IRC (Ping timeout: 276 seconds) | 03:44 | |
| *** srk- is now known as srk | 03:44 | |
| *** emeb_mac <[email protected]> has quit IRC (Quit: Leaving.) | 06:59 | |
| *** unkraut <[email protected]> has joined #yosys | 07:45 | |
| *** cr1901 <cr1901!~cr1901@2601:8d:8600:911:7c92:96ff:a989:67c9> has joined #yosys | 07:51 | |
| *** AdamHord- is now known as AdamHorden | 10:32 | |
| *** chaoticryptidz <chaoticryptidz!~quassel@2a01:4f9:c010:8beb::> has quit IRC (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.) | 10:49 | |
| *** chaoticryptidz <chaoticryptidz!~quassel@2a01:4f9:c010:8beb::> has joined #yosys | 10:49 | |
| *** chaoticryptidz <chaoticryptidz!~quassel@2a01:4f9:c010:8beb::> has quit IRC (Client Quit) | 10:51 | |
| *** chaoticryptidz <chaoticryptidz!~quassel@2a01:4f9:c010:8beb::> has joined #yosys | 10:51 | |
| *** chaoticryptidz <chaoticryptidz!~quassel@2a01:4f9:c010:8beb::> has quit IRC (Client Quit) | 10:54 | |
| *** chaoticryptidz <chaoticryptidz!~quassel@2a01:4f9:c010:8beb::> has joined #yosys | 10:54 | |
| *** chaoticryptidz <chaoticryptidz!~quassel@2a01:4f9:c010:8beb::> has quit IRC (Client Quit) | 10:57 | |
| *** chaoticryptidz <chaoticryptidz!~quassel@2a01:4f9:c010:8beb::> has joined #yosys | 10:58 | |
| *** AdamHorden <[email protected]> has quit IRC (Quit: Adam Horden) | 11:30 | |
| *** AdamHorden <[email protected]> has joined #yosys | 11:31 | |
| *** AdamHorden <[email protected]> has quit IRC (Client Quit) | 11:32 | |
| *** AdamHorden <[email protected]> has joined #yosys | 11:34 | |
| *** AdamHorden <[email protected]> has quit IRC (Remote host closed the connection) | 11:34 | |
| *** AdamHorden <[email protected]> has joined #yosys | 11:37 | |
| *** AdamHorden <[email protected]> has quit IRC (Quit: Adam Horden) | 11:43 | |
| *** AdamHorden <[email protected]> has joined #yosys | 11:43 | |
| *** AdamHorden <[email protected]> has quit IRC (Client Quit) | 11:44 | |
| *** AdamHorden <[email protected]> has joined #yosys | 11:49 | |
| *** AdamHorden <[email protected]> has quit IRC (Remote host closed the connection) | 11:49 | |
| *** AdamHorden <[email protected]> has joined #yosys | 11:50 | |
| *** AdamHorden <[email protected]> has quit IRC (Client Quit) | 11:53 | |
| *** AdamHorden <[email protected]> has joined #yosys | 11:54 | |
| *** FabM <FabM!~FabM@2a03:d604:103:600:3390:1fdf:778:6055> has joined #yosys | 12:15 | |
| *** emeb_mac <[email protected]> has joined #yosys | 12:42 | |
| *** AdamHorden <[email protected]> has quit IRC (Quit: Adam Horden) | 13:39 | |
| *** AdamHorden <[email protected]> has joined #yosys | 13:42 | |
| *** AdamHorden <[email protected]> has quit IRC (Quit: Adam Horden) | 13:55 | |
| *** AdamHorden <[email protected]> has joined #yosys | 13:56 | |
| *** AdamHorden <[email protected]> has quit IRC (Quit: Adam Horden) | 14:08 | |
| *** AdamHorden <[email protected]> has joined #yosys | 14:09 | |
| *** benreynwar_ <[email protected]> has joined #yosys | 15:41 | |
| *** SpaceCoaster_ <SpaceCoaster_!~derek@user/spacecoaster> has joined #yosys | 15:41 | |
| *** Moe_Icenowy <Moe_Icenowy!~MoeIcenow@2604:a880:2:d1::1d1:f001> has joined #yosys | 15:41 | |
| *** mithro_ <[email protected]> has joined #yosys | 15:42 | |
| *** Knarfian______ <[email protected]> has joined #yosys | 15:42 | |
| *** dnm_ <[email protected]> has joined #yosys | 15:42 | |
| *** freshmaker666 <[email protected]> has joined #yosys | 15:42 | |
| *** anticw_ <[email protected]> has joined #yosys | 15:44 | |
| *** mathu_ <mathu_!~matt@user/mathu> has joined #yosys | 15:45 | |
| *** shorne_ <[email protected]> has joined #yosys | 15:45 | |
| *** shoragan_ <shoragan_!~shoragan@user/shoragan> has joined #yosys | 15:48 | |
| *** cyrozap-ZNC <[email protected]> has joined #yosys | 15:48 | |
| *** pepijndevos[m] <pepijndevos[m]!~pepijndev@2001:470:69fc:105::b6a8> has quit IRC (*.net *.split) | 15:49 | |
| *** shorne <[email protected]> has quit IRC (*.net *.split) | 15:49 | |
| *** benreynwar <[email protected]> has quit IRC (*.net *.split) | 15:49 | |
| *** shoragan <shoragan!~shoragan@user/shoragan> has quit IRC (*.net *.split) | 15:49 | |
| *** SpaceCoaster <SpaceCoaster!~derek@user/spacecoaster> has quit IRC (*.net *.split) | 15:49 | |
| *** Knarfian_____ <Knarfian_____!sid501585@2a03:5180:f:1::7:a751> has quit IRC (*.net *.split) | 15:49 | |
| *** mithro <[email protected]> has quit IRC (*.net *.split) | 15:49 | |
| *** MoeIcenowy <MoeIcenowy!~MoeIcenow@2604:a880:2:d1::1d1:f001> has quit IRC (*.net *.split) | 15:49 | |
| *** cyrozap <cyrozap!~cyrozap@2604:180:2:69f::45de> has quit IRC (*.net *.split) | 15:50 | |
| *** anticw <[email protected]> has quit IRC (*.net *.split) | 15:50 | |
| *** mathu <mathu!~matt@user/mathu> has quit IRC (*.net *.split) | 15:50 | |
| *** greeb <[email protected]> has quit IRC (*.net *.split) | 15:50 | |
| *** dnm <[email protected]> has quit IRC (*.net *.split) | 15:50 | |
| *** benreynwar_ is now known as benreynwar | 15:50 | |
| *** SpaceCoaster_ is now known as SpaceCoaster | 15:50 | |
| *** Knarfian______ is now known as Knarfian_____ | 15:50 | |
| *** mithro_ is now known as mithro | 15:50 | |
| *** dnm_ is now known as dnm | 15:50 | |
| *** pepijndevos[m] <pepijndevos[m]!~pepijndev@2001:470:69fc:105::b6a8> has joined #yosys | 16:00 | |
| *** ec <ec!~ec@gateway/tor-sasl/ec> has joined #yosys | 16:00 | |
| *** emeb <[email protected]> has joined #yosys | 16:06 | |
| *** FabM <FabM!~FabM@armadeus/team/FabM> has quit IRC (Quit: Leaving) | 16:16 | |
| *** smkz <smkz!~x@user/smkz> has quit IRC (Quit: reboot@) | 16:37 | |
| *** smkz <smkz!~x@user/smkz> has joined #yosys | 16:38 | |
| *** kraiskil <[email protected]> has joined #yosys | 16:52 | |
| *** smkz <smkz!~x@user/smkz> has quit IRC (Quit: reboot@) | 17:04 | |
| *** smkz <smkz!~x@user/smkz> has joined #yosys | 17:06 | |
| *** kraiskil <[email protected]> has quit IRC (Ping timeout: 248 seconds) | 17:23 | |
| *** cr1901_ <cr1901_!~cr1901@2601:8d:8600:911:80a3:6c15:cf66:3389> has joined #yosys | 18:18 | |
| 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) | 18:20 |
|---|---|---|
| lkcl | and would like to do that in nmigen / yosys | 18:20 |
| lkcl | however | 18:20 |
| lkcl | yosys does not support BitVector which is what's needed to be passed-through, soooo.... | 18:21 |
| lkcl | as a first-pass "hack", the plan is to add properties - as strings - to be passed through to sby/z3/smt2 | 18:21 |
| *** cr1901 <cr1901!~cr1901@2601:8d:8600:911:7c92:96ff:a989:67c9> has quit IRC (Ping timeout: 248 seconds) | 18:22 | |
| lkcl | (because adding BitVectors as a "proper" - full - type to yosys is one hell of a lot of work) | 18:22 |
| lkcl | the tracking bug for anyone interested is here https://bugs.libre-soc.org/show_bug.cgi?id=835 | 18:24 |
| tpb | Title: 835 – add support for smtlib2 floating-point to yosys and nmigen (at bugs.libre-soc.org) | 18:24 |
| jix_ | what do you mean with "BitVector" here, when writing smtlib yosys uses BitVecs for signals, so I guess you must mean something else? | 18:31 |
| *** peeps[zen] <peeps[zen]!~peepsalot@openscad/peepsalot> has joined #yosys | 18:32 | |
| *** jix_ is now known as jix | 18:32 | |
| lkcl | jix: yes, quite likely. my memory's slightly odd. i think i meant smt2 FP type (which is experimental) | 18:32 |
| *** peepsalot <peepsalot!~peepsalot@openscad/peepsalot> has quit IRC (Ping timeout: 248 seconds) | 18:33 | |
| lkcl | https://git.libre-soc.org/?p=ieee754fpu.git;a=blob;f=fp16mul_test.smt2;h=6ad9dc798eb34c72357c3d94d953de01493a5795;hb=c17c88ffba83c546ae439238fdd43adce3992f53#l129 | 18:34 |
| tpb | Title: git.libre-soc.org Git - ieee754fpu.git/blob - fp16mul_test.smt2 (at git.libre-soc.org) | 18:34 |
| lkcl | 129 (define-fun f16_to_fp ((v bv16)) Float16 ((_ to_fp 5 11) v)) | 18:34 |
| 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 | 18:35 |
| *** kraiskil <[email protected]> has joined #yosys | 18:44 | |
| *** kraiskil <[email protected]> has quit IRC (Client Quit) | 18:49 | |
| 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? | 18:54 |
| jix | that would only need small changes to sby to allow adding user smt2 statements but no changes to yosys or smtbmc | 18:58 |
| *** kraiskil <[email protected]> has joined #yosys | 19:01 | |
| 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) | 19:44 |
| *** cr1901_ is now known as cr1901 | 19:48 | |
| 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) | 19:53 |
| jix | but incremental solving isn't needed for this smt2 file and for smtbmc it's optional (there's a -noincr option) | 19:55 |
| jix | and bitwuzla with cadical (default SAT backend) is probably still faster than z3 | 19:56 |
| *** kraiskil <[email protected]> has quit IRC (Ping timeout: 246 seconds) | 20:00 | |
| jix | not convinced that bitwuzla can crack the 32-bit float version, though, but I'm curious so I'll let it run overnight | 20:13 |
| qball | a few days runtime should still be ok as long as it finishes. | 20:18 |
| qball | (with a useful result :D_ | 20:18 |
| jix | sometimes it's really hard to tell whether it's still making progress though | 20:19 |
| qball | that is why you launch it on a server, forget about it while being busy, and remember a few days later | 20:19 |
| qball | (that happens to me from time to time) | 20:20 |
| jix | yeah but even then you don't know if it would finish if you give it another week | 20:20 |
| qball | yeah, | 20:22 |
| *** emeb <[email protected]> has left #yosys | 20:23 | |
| lkcl | jix: ooo, niice. | 20:36 |
| lkcl | i set -v:3 on z3 and it gave me some reasonable progress notification | 20:37 |
| lkcl | cvc5 on the other hand: nothing :) | 20:37 |
| jix | heh, I think even z3's status output is rather useless to figure out if it is worth to keep it running | 20:39 |
| jix | I find cadical's or kissat's output (very similar) much more useful, but part of that is probably familiarity | 20:40 |
| lkcl | jix: i'm pinging programmerjake because he's the one working on this, let's see if he joins this channel | 20:40 |
| jix | but even if it looks like progress, it might just move asymptotically to a place where it's stuck for all practical purposes | 20:41 |
| 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 | 20:50 |
| *** programmerjake <programmerjake!~programme@2001:470:69fc:105::172f> has joined #yosys | 20:52 | |
| *** nonchip <[email protected]> has quit IRC (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.) | 22:12 | |
| *** nonchip <[email protected]> has joined #yosys | 22:13 | |
| *** ec <ec!~ec@gateway/tor-sasl/ec> has quit IRC (Quit: ec) | 22:43 | |
| *** shoragan_ <shoragan_!~shoragan@user/shoragan> has quit IRC (Quit: quit) | 23:00 | |
| *** shoragan <shoragan!~shoragan@user/shoragan> has joined #yosys | 23:01 | |
| 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. | 23:12 |
| 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 | 23:14 |
| 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 | 23:32 |
| jix | ah that wasn't what I was trying to suggest | 23:33 |
| 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) | 23:34 |
| jix | you can already use arbitrary smt2 constraints, as long as the interface to is all bitvectors, without adding any new cells to yosys | 23:35 |
| jix | write_smt2 doesn't generate any smtlib code for modules with the blackbox attribute, so you can supply your own for those | 23:36 |
| 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 | 23:40 |
| programmerjake | ah, I wanted to put it through yosys so manually concatenating isn't necessary. | 23:45 |
| programmerjake | also so yosys can take care of naming and stuff so I don't have to re-implement that | 23:46 |
| jix | yeah I can see how that's more convenient, I'm not sure that adding a custom cell is the best approach though | 23:47 |
| *** cr1901_ <cr1901_!~cr1901@2601:8d:8600:911:507a:a18b:6a75:4106> has joined #yosys | 23:55 | |
| *** cr1901 <cr1901!~cr1901@2601:8d:8600:911:80a3:6c15:cf66:3389> has quit IRC (Read error: Connection reset by peer) | 23:55 | |
| *** cr1901 <cr1901!~cr1901@2601:8d:8600:911:507a:a18b:6a75:4106> has joined #yosys | 23:56 | |
| *** cr1901_ <cr1901_!~cr1901@2601:8d:8600:911:507a:a18b:6a75:4106> has quit IRC (Ping timeout: 240 seconds) | 23:59 | |
Generated by irclog2html.py 2.17.2 by Marius Gedminas - find it at https://mg.pov.lt/irclog2html/!