| *** tpb <[email protected]> has joined #yosys | 00:00 | |
| *** emeb <[email protected]> has quit IRC (Quit: Leaving.) | 00:00 | |
| *** adjtm_ <[email protected]> has joined #yosys | 00:41 | |
| *** adjtm <[email protected]> has quit IRC (Read error: Connection reset by peer) | 00:42 | |
| *** adjtm <[email protected]> has joined #yosys | 00:45 | |
| *** adjtm_ <[email protected]> has quit IRC (Ping timeout: 240 seconds) | 00:46 | |
| *** nelgau_ <[email protected]> has joined #yosys | 00:48 | |
| *** nelgau <[email protected]> has quit IRC (Ping timeout: 250 seconds) | 00:48 | |
| *** Klotz <Klotz!~Klotzoman@gateway/tor-sasl/klotz> has quit IRC (Quit: Klotz) | 01:37 | |
| *** tlwoerner <[email protected]> has quit IRC (Quit: Leaving) | 02:05 | |
| *** tlwoerner <[email protected]> has joined #yosys | 02:34 | |
| *** citypw <citypw!~citypw@gateway/tor-sasl/citypw> has joined #yosys | 03:11 | |
| *** cr1901_ <cr1901_!~cr1901@2601:8d:8600:911:f905:9a1b:64ea:2992> has joined #yosys | 04:17 | |
| *** cr1901 <cr1901!~cr1901@2601:8d:8600:911:258e:a763:608d:bfea> has quit IRC (Ping timeout: 252 seconds) | 04:19 | |
| *** cr1901_ is now known as cr1901 | 04:38 | |
| *** emeb_mac <[email protected]> has quit IRC (Quit: Leaving.) | 04:59 | |
| *** X-Scale <[email protected]> has quit IRC (Ping timeout: 240 seconds) | 06:29 | |
| *** X-Scale` <X-Scale`[email protected]> has joined #yosys | 06:29 | |
| *** X-Scale` is now known as X-Scale | 06:30 | |
| *** kristianpaul <kristianpaul!~paul@user/kristianpaul> has quit IRC (Ping timeout: 252 seconds) | 07:03 | |
| *** kristianpaul <kristianpaul!~paul@user/kristianpaul> has joined #yosys | 07:04 | |
| *** shorne <[email protected]> has joined #yosys | 08:19 | |
| shorne | Well, hello, I have spent the last few weeks deep diving into formal verification with yosys. I am re-defining our formal verification properties in the OpenRISC mor1kx core around the Load/Store Unit including, rams, dcache, dmmu and now LSU. | 08:21 |
|---|---|---|
| shorne | Someone said Test benches are for ensuring you system is valid for the TB provided inputs. Formal verification is for ensuring your system works for all valid inputs. | 08:22 |
| shorne | I find this formal verification is no silver bullet, as defining the valid inputs is the tricky part. | 08:23 |
| gatecat | Yeah, the particular danger is with `assume` statements which restrict the input/state space | 08:38 |
| shorne | yea, or like for me now is I put some assume's to start simple | 08:39 |
| shorne | i.e. assume (!dbus_err_i); | 08:39 |
| shorne | then I just leave that there :) | 08:39 |
| gatecat | Mm | 08:40 |
| *** Klotz <Klotz!~Klotzoman@gateway/tor-sasl/klotz> has joined #yosys | 12:06 | |
| *** citypw <citypw!~citypw@gateway/tor-sasl/citypw> has quit IRC (Ping timeout: 240 seconds) | 12:50 | |
| *** citypw <citypw!~citypw@gateway/tor-sasl/citypw> has joined #yosys | 12:53 | |
| *** emeb <[email protected]> has joined #yosys | 14:41 | |
| cr1901 | shorne: https://github.com/cr1901/yosys-experiments/tree/master/sat/dffhold It's not always possible to do k-induction either | 15:17 |
| *** citypw <citypw!~citypw@gateway/tor-sasl/citypw> has quit IRC (Ping timeout: 240 seconds) | 15:37 | |
| *** emeb <[email protected]> has quit IRC (Quit: Leaving.) | 16:43 | |
| *** emeb <[email protected]> has joined #yosys | 16:45 | |
| *** emeb <[email protected]> has quit IRC (Quit: Leaving.) | 18:56 | |
| *** emeb <[email protected]> has joined #yosys | 18:58 | |
| jix | adding simple-path constraints makes k-induction complete in theory (whether it's useful in practice, I don't know yet, also not sure if any of the sby engines/solvers support it) | 20:53 |
| *** adamse <adamse!sid72084@user/adamse> has left #yosys | 22:33 | |
| lkcl | shorne, the generally-accepted "word" on formal correctness proofs is that they're much more useful - to everyone including you - when several people implement the same design and use the same formal correctness proof | 23:04 |
| lkcl | the logic behind that being that you can accidentally make assumptions about the assumes/asserts. | 23:05 |
| lkcl | the other thing that is a royal pain in the ass: inputs (or even combinations of bits *in* inputs) that you don't use, didn't put in the assumes, and the formal correctness engines go | 23:07 |
| lkcl | "oh yeah i found this permutation of input bits you never thought possible could ever be set and hadn't covered in any switch statements (etc) but *if* you ever set them the output is borked, there you go" | 23:08 |
| lkcl | :) | 23:08 |
| lkcl | this one drove 2 people absolutely nuts for several weeks when trying to do a formal correctness proof for the libre-soc Power ISA rotate module | 23:09 |
Generated by irclog2html.py 2.17.2 by Marius Gedminas - find it at https://mg.pov.lt/irclog2html/!