| *** tpb <[email protected]> has joined #litex | 00:00 | |
| *** nelgau_ <[email protected]> has joined #litex | 00:48 | |
| *** nelgau <[email protected]> has quit IRC (Ping timeout: 250 seconds) | 00:48 | |
| *** Emantor <[email protected]> has quit IRC (Quit: ZNC - http://znc.in) | 02:20 | |
| *** Emantor <[email protected]> has joined #litex | 02:21 | |
| *** Degi <[email protected]> has quit IRC (Ping timeout: 240 seconds) | 02:25 | |
| *** Degi <[email protected]> has joined #litex | 02:27 | |
| *** Coldberg <[email protected]> has joined #litex | 02:52 | |
| *** C-Man <[email protected]> has quit IRC (Ping timeout: 256 seconds) | 02:56 | |
| *** cr1901_ <cr1901_!~cr1901@2601:8d:8600:911:f905:9a1b:64ea:2992> has joined #litex | 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 | |
| *** sebo <[email protected]> has joined #litex | 05:31 | |
| *** sebo <[email protected]> has quit IRC (Ping timeout: 272 seconds) | 05:39 | |
| *** Martoni <Martoni!~Martoni@2a03:d604:103:600:2ad2:44ff:fe23:2f72> has joined #litex | 06:40 | |
| *** Martoni <Martoni!~Martoni@2a03:d604:103:600:2ad2:44ff:fe23:2f72> has quit IRC (Ping timeout: 252 seconds) | 07:34 | |
| shorne | Anyone have much experience with formal verification? In particular yosys? | 08:16 |
|---|---|---|
| shorne | I have been spending the last few weeks really deep diving into it to formally verify mor1kx dcache and LSU. This was done partially for Google Summer of Code last year, but I am changing the approach | 08:17 |
| shorne | just want to talk out some idea's. So here we go... | 08:17 |
| 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 any valid inputs. | 08:18 |
| shorne | My take-away, the formal verification is only as good as your definition of valid inputs. So its no silver bullet | 08:19 |
| shorne | maybe I should chat on #yosys | 08:19 |
| *** Coldberg <[email protected]> has quit IRC (Ping timeout: 260 seconds) | 09:18 | |
| *** C-Man <[email protected]> has joined #litex | 09:41 | |
| *** sebo <[email protected]> has joined #litex | 10:47 | |
| *** sebo <[email protected]> has quit IRC (Ping timeout: 240 seconds) | 10:57 | |
| *** sebo <[email protected]> has joined #litex | 11:20 | |
| *** sebo <[email protected]> has quit IRC (Ping timeout: 260 seconds) | 11:53 | |
| *** Martoni <Martoni!~Martoni@2a03:d604:103:600:2ad2:44ff:fe23:2f72> has joined #litex | 11:54 | |
| *** Martoni <Martoni!~Martoni@2a03:d604:103:600:2ad2:44ff:fe23:2f72> has quit IRC (Ping timeout: 240 seconds) | 12:01 | |
| *** sebo <[email protected]> has joined #litex | 12:29 | |
| *** sebo <[email protected]> has quit IRC (Ping timeout: 272 seconds) | 12:38 | |
| *** sebo <[email protected]> has joined #litex | 13:05 | |
| *** sebo <[email protected]> has quit IRC (Ping timeout: 272 seconds) | 13:44 | |
| *** RaYmAn <[email protected]> has quit IRC (Ping timeout: 268 seconds) | 14:09 | |
| *** sebo <[email protected]> has joined #litex | 14:12 | |
| *** C-Man <[email protected]> has quit IRC (Ping timeout: 256 seconds) | 14:47 | |
| _florent_ | shorne: I share the same feelings on formal: testbenches and formal verification complement each others. Testbenches are useful to design your system, test it in practical use-cases (and are useful for later for debug, to reinject behavior seen on hardware, etc...) and formal can ease some testing of some specific parts: testing an AsyncFIFO is for example a lot more efficient and will give more confidence with formal). | 15:17 |
| _florent_ | shorne: Injecting randomness on testbenches is also a good intermediary step before doing formal | 15:18 |
| _florent_ | shorne: but yes, saying that your system is formally verified does not have lot more value that saying it's passing the testbenches, both are complementary :) | 15:21 |
| *** sebo <[email protected]> has quit IRC (Ping timeout: 256 seconds) | 15:40 | |
| *** sebo <[email protected]> has joined #litex | 15:42 | |
| *** C-Man <[email protected]> has joined #litex | 15:53 | |
| *** sebo <[email protected]> has quit IRC (Ping timeout: 272 seconds) | 17:12 | |
| *** Martoni <Martoni!~Martoni@2a03:d604:103:600:2ad2:44ff:fe23:2f72> has joined #litex | 17:33 | |
| *** Martoni <Martoni!~Martoni@2a03:d604:103:600:2ad2:44ff:fe23:2f72> has quit IRC (Ping timeout: 252 seconds) | 17:43 | |
| *** Martoni <Martoni!~Martoni@2a03:d604:103:600:2ad2:44ff:fe23:2f72> has joined #litex | 19:42 | |
| *** Martoni <Martoni!~Martoni@2a03:d604:103:600:2ad2:44ff:fe23:2f72> has quit IRC (Ping timeout: 240 seconds) | 20:48 | |
Generated by irclog2html.py 2.17.2 by Marius Gedminas - find it at https://mg.pov.lt/irclog2html/!