| *** tpb has joined #yosys | 00:00 | |
| *** kristianpaul has quit IRC | 00:01 | |
| *** kristianpaul has joined #yosys | 00:02 | |
| *** Degi has quit IRC | 02:51 | |
| *** Degi has joined #yosys | 02:51 | |
| *** N2TOH has joined #yosys | 03:50 | |
| *** citypw has joined #yosys | 04:18 | |
| *** citypw has quit IRC | 06:27 | |
| *** citypw has joined #yosys | 06:28 | |
| *** emeb_mac has quit IRC | 06:46 | |
| *** jakobwenzel has joined #yosys | 07:22 | |
| z0ttel | Does symbiyosys "prove basecase" differ from bmc and can I give it a separate depth than the induction? | 08:33 |
|---|---|---|
| daveshah | It doesn't differ afaik, but there is no way of giving it a different depth | 08:39 |
| daveshah | I'm not sure why you'd want a different depth though. Lower would render the proof unsound, higher would be superfluous | 08:40 |
| z0ttel | oh, okay I realize my error now, induction depends on $depth steps too... okay, thx | 08:41 |
| z0ttel | But, an optimisation would then be to check induction results after each basecase step and terminate with PASS when induction was successful with less steps than basecase has so far? | 08:52 |
| daveshah | No, because induction differs between the first N-1 steps and the final N step | 08:52 |
| *** chipb has quit IRC | 09:00 | |
| *** chipb has joined #yosys | 09:00 | |
| z0ttel | So the command line output counting down induction steps isn't SymbiYosys trying to solve the full induction with less than $depth? | 09:02 |
| *** vidbina has joined #yosys | 09:22 | |
| *** Asu has joined #yosys | 09:25 | |
| daveshah | No, the way the induction part works is N-1 cycles assuming that assertions are true then checking assertions on the final cycle | 09:26 |
| *** peeps[zen] has joined #yosys | 09:37 | |
| *** peepsalot has quit IRC | 09:37 | |
| z0ttel | I mean, I now realise that a k-induction proof essentially proves: (assertions hold for k-1 steps) -> (assertions holds in step k) with a base case of step 0 to k-1 | 09:41 |
| z0ttel | But Symbiyosys counts down the induction steps starting at k and, depending on what I'm trying to prove, stops the induction step at different steps with a PASS result. | 09:42 |
| *** strobokopp has joined #yosys | 09:48 | |
| *** show1 has quit IRC | 10:37 | |
| *** show has joined #yosys | 10:39 | |
| *** jakobwenzel1 has joined #yosys | 11:31 | |
| *** kristianpaul has quit IRC | 13:01 | |
| *** kristianpaul has joined #yosys | 13:07 | |
| *** emeb has joined #yosys | 14:14 | |
| *** jakobwenzel1 has quit IRC | 16:01 | |
| *** citypw has quit IRC | 16:23 | |
| *** az0re has quit IRC | 17:20 | |
| *** az0re has joined #yosys | 17:22 | |
| ZipCPU | z0ttel: I've asked for this optimization for some time. If induction can prove PASS in 5 steps, the basecase should be ended after 5 steps. | 18:30 |
| ZipCPU | There's another optimization you can do as well, but I don't know that the tool could do it, so sometimes you can end your proof early: If induction finishes in 10 steps, and the basecase is stuck on step 3--but yet you know your design can enter into an idle state on step 2, then you can know that your design will pass | 18:31 |
| *** kraiskil has joined #yosys | 19:30 | |
| thardin | damn the ecp5's are nice. it's looking like finding ADCs to feed them that don't cost an arm and a leg is trickier | 20:01 |
| tnt | for some of them a single kidney is enough. | 20:04 |
| *** emeb_mac has joined #yosys | 20:40 | |
| *** _whitelogger has quit IRC | 21:04 | |
| *** _whitelogger has joined #yosys | 21:07 | |
| *** thardin has quit IRC | 22:21 | |
| *** Asu has quit IRC | 22:25 | |
| cr1901_modern | I don't remember why the k-induction counts down, but it confuses me too (since if you look at the SMT files generated, k-induction will _add_ more states as the k-induction counter counts down) | 22:57 |
| *** kristianpaul has quit IRC | 23:14 | |
| *** kristianpaul has joined #yosys | 23:14 | |
| *** lf has quit IRC | 23:17 | |
| *** lf has joined #yosys | 23:18 | |
| *** kraiskil has quit IRC | 23:26 | |
| *** emeb has left #yosys | 23:32 | |
| *** kraiskil has joined #yosys | 23:43 | |
| *** vidbina has quit IRC | 23:56 | |
Generated by irclog2html.py 2.17.2 by Marius Gedminas - find it at https://mg.pov.lt/irclog2html/!