| *** tpb has joined #yosys | 00:00 | |
| *** xtro has joined #yosys | 00:09 | |
| *** xtro has quit IRC | 00:11 | |
| *** LJ_cache has quit IRC | 00:53 | |
| *** citypw has joined #yosys | 02:18 | |
| *** emeb has left #yosys | 02:37 | |
| *** kristianpaul has quit IRC | 03:07 | |
| *** citypw has quit IRC | 03:07 | |
| *** kristianpaul has joined #yosys | 03:08 | |
| *** citypw has joined #yosys | 03:10 | |
| *** Degi has quit IRC | 03:16 | |
| *** Degi has joined #yosys | 03:16 | |
| awygle | hm. how would i go about asserting "this state machine can't get stuck in any state but IDLE forever"? | 03:39 |
|---|---|---|
| awygle | i can think of a few ways but they feel hacky to me | 03:39 |
| awygle | (this is a question about formal verification in case that wasn't clear) | 03:39 |
| awygle | seems like i'd have to put a bound on it, instead of "forever", which is fine, i can do that math | 03:41 |
| awygle | but then i have to do like "assert state == idle or past state == idle or past past state == idle or......" | 03:42 |
| awygle | actually that's not too bad is it. just have a counter that gets reset when state is idle and assert it never gets above bound. | 03:42 |
| awygle | thanks rubber duck irc channel :) | 03:42 |
| *** az0re has quit IRC | 04:00 | |
| *** emeb has joined #yosys | 04:06 | |
| *** Forty-Bot has quit IRC | 04:10 | |
| *** Forty-Bot has joined #yosys | 04:10 | |
| awygle | hm either yosys is just doing whatever with this design or i've done something terribly wrong | 04:56 |
| awygle | probably the latter | 04:56 |
| *** az0re has joined #yosys | 05:19 | |
| *** emeb_mac has quit IRC | 06:40 | |
| *** emeb has quit IRC | 06:42 | |
| *** mmicko has quit IRC | 07:11 | |
| *** mmicko has joined #yosys | 07:13 | |
| *** Asu has joined #yosys | 08:40 | |
| *** cr1901_modern has quit IRC | 09:00 | |
| *** cr1901_modern has joined #yosys | 09:04 | |
| *** cr1901_modern has quit IRC | 09:08 | |
| *** cr1901_modern has joined #yosys | 09:10 | |
| *** cr1901_modern has quit IRC | 09:11 | |
| *** cr1901_modern has joined #yosys | 09:14 | |
| *** cr1901_modern has quit IRC | 09:22 | |
| *** cr1901_modern has joined #yosys | 09:47 | |
| *** cr1901_modern has quit IRC | 09:49 | |
| *** cr1901_modern has joined #yosys | 09:49 | |
| *** cr1901_modern has quit IRC | 09:55 | |
| *** cr1901_modern has joined #yosys | 10:16 | |
| *** cr1901_modern has quit IRC | 10:18 | |
| *** cr1901_modern has joined #yosys | 10:18 | |
| *** cr1901_modern has quit IRC | 10:19 | |
| *** cr1901_modern has joined #yosys | 10:20 | |
| *** cr1901_modern has quit IRC | 10:21 | |
| *** cr1901_modern has joined #yosys | 10:22 | |
| *** cr1901_modern has quit IRC | 10:27 | |
| *** cr1901_modern has joined #yosys | 11:11 | |
| thardin | awygle: use the induction, luke | 11:14 |
| *** cr1901_modern has quit IRC | 11:15 | |
| lambda | awygle: proving liveness is kinda difficult in my experience, at least tooling-wise | 11:27 |
| whitequark | yosys does have some built-in support for proving liveness but i second what lambda says | 11:29 |
| ZipCPU | awygle: I'd use a counter. Clear the counter when you are in the idle state, otherwise add 1 per clock. Assert it stays below some value. | 11:29 |
| ZipCPU | The challenge is that either 1) your induction length now needs to be at least as long as the counters limit, or 2) you need to tie counter bounds to various FSM states | 11:30 |
| daveshah | Yeah I think only the more esoteric aiger solvers support liveness with symbiyosys | 11:30 |
| *** cr1901_modern has joined #yosys | 11:47 | |
| *** fcserr has quit IRC | 11:47 | |
| *** cr1901_modern has quit IRC | 11:52 | |
| *** cr1901_modern has joined #yosys | 12:21 | |
| *** cr1901_modern has quit IRC | 12:25 | |
| *** cr1901_modern has joined #yosys | 13:18 | |
| *** cr1901_modern has quit IRC | 13:22 | |
| *** Asu has quit IRC | 13:53 | |
| *** Asuu has joined #yosys | 13:53 | |
| *** thoughtpolice_ has joined #yosys | 13:57 | |
| *** y2kbugger_ has joined #yosys | 13:57 | |
| *** ktemkin_ has joined #yosys | 13:57 | |
| *** bubble_buster_ has joined #yosys | 13:57 | |
| *** flammit_ has joined #yosys | 13:57 | |
| *** benreynwar_ has joined #yosys | 13:57 | |
| *** ric96_ has joined #yosys | 13:57 | |
| *** gruetze_ has joined #yosys | 13:58 | |
| *** lukego has quit IRC | 14:00 | |
| *** ktemkin has quit IRC | 14:00 | |
| *** ric96 has quit IRC | 14:00 | |
| *** bubble_buster has quit IRC | 14:00 | |
| *** benreynwar has quit IRC | 14:00 | |
| *** flammit has quit IRC | 14:00 | |
| *** unkraut has quit IRC | 14:00 | |
| *** thoughtpolice has quit IRC | 14:00 | |
| *** lambda has quit IRC | 14:00 | |
| *** y2kbugger has quit IRC | 14:00 | |
| *** Sarayan has quit IRC | 14:00 | |
| *** cyrozap has quit IRC | 14:00 | |
| *** gruetzkopf has quit IRC | 14:00 | |
| *** z0ttel has quit IRC | 14:00 | |
| *** whitequark has quit IRC | 14:00 | |
| *** emilazy has quit IRC | 14:00 | |
| *** ktemkin_ is now known as ktemkin | 14:00 | |
| *** bubble_buster_ is now known as bubble_buster | 14:00 | |
| *** benreynwar_ is now known as benreynwar | 14:00 | |
| *** emilazy_ has joined #yosys | 14:00 | |
| *** flammit_ is now known as flammit | 14:00 | |
| *** y2kbugger_ is now known as y2kbugger | 14:00 | |
| *** thoughtpolice_ is now known as thoughtpolice | 14:00 | |
| *** ric96_ is now known as ric96 | 14:00 | |
| *** emilazy_ is now known as emilazy | 14:00 | |
| *** maartenBE has quit IRC | 14:02 | |
| *** cyrozap has joined #yosys | 14:04 | |
| *** filt3r has quit IRC | 14:06 | |
| *** filt3r has joined #yosys | 14:07 | |
| *** lukego has joined #yosys | 14:07 | |
| *** maartenBE has joined #yosys | 14:08 | |
| *** lambda has joined #yosys | 14:09 | |
| *** cr1901_modern has joined #yosys | 14:14 | |
| *** gruetze_ is now known as gruetzkopf | 14:37 | |
| *** kristianpaul has quit IRC | 15:00 | |
| *** kristianpaul has joined #yosys | 15:01 | |
| *** ross_s has joined #yosys | 15:31 | |
| *** AdamHorden has quit IRC | 15:32 | |
| ross_s | Does yosys have any support for converting reals to bits? Looking at frontends/ast/simplify.cc I don't spot anything. Are there other methods if one wanted to generate a look up table of floating point values at synthesis time? | 15:44 |
| awygle | thanks for the suggestions everybody | 15:46 |
| awygle | i'm going with the counter approach (because the counter length is pretty easy to bound) but now my bounded model check seems to be taking impossible FSM transitions, so i gotta figure that out this morning | 15:46 |
| awygle | yosys formal won't recode my FSM states will it? i'm only doing `read_ilang` and `prep` | 15:47 |
| *** AdamHorden has joined #yosys | 15:51 | |
| awygle | hm i updated yosys and now i get "unsupported cell type sdffe" errors. mwk is this related to https://github.com/YosysHQ/yosys/pull/1818/commits? gonna try checking out the version right before that | 15:55 |
| awygle | oh, helps to update sby, my bad | 15:57 |
| mwk | pretty much yes | 15:57 |
| awygle | works now (or, uh, fails to work in the same way as before the update). sorry to bother you :) | 15:58 |
| mwk | ... and yeah, the formal won't do FSM recoding | 16:03 |
| mwk | (not that FSM recoding actually works all that often) | 16:03 |
| *** citypw has quit IRC | 16:41 | |
| *** emeb has joined #yosys | 18:26 | |
| *** kristianpaul has quit IRC | 20:22 | |
| *** kristianpaul has joined #yosys | 20:23 | |
| *** emeb_mac has joined #yosys | 20:33 | |
| *** kristianpaul has quit IRC | 21:09 | |
| *** kristianpaul has joined #yosys | 21:10 | |
| *** kristianpaul has quit IRC | 21:12 | |
| *** kristianpaul has joined #yosys | 21:19 | |
| *** Asuu has quit IRC | 22:24 | |
| *** lf has quit IRC | 23:31 | |
| *** lf has joined #yosys | 23:32 | |
| *** emeb has quit IRC | 23:39 | |
Generated by irclog2html.py 2.17.2 by Marius Gedminas - find it at https://mg.pov.lt/irclog2html/!