| *** tpb has joined #yosys | 00:00 | |
| *** kraiskil has quit IRC | 00:03 | |
| *** emeb_mac has joined #yosys | 00:47 | |
| mwk | pepijndevos: in gowin, why do all the FFs have the INIT parameter? it seems to me that init value is basically determined by the cell type (0 if it has reset, 1 if it has set), and thus the parameter is both unnecessary and invalid (ie. cells with set have INIT of 0 by default. and the techmap rules don't change that default, resulting in sim mismatch) | 01:03 |
|---|---|---|
| *** emeb_mac has quit IRC | 01:20 | |
| Lofty | I think it's to match the vendor model, mwk | 01:21 |
| *** emeb has quit IRC | 01:21 | |
| mwk | Lofty: I'd prefer correct models to vendor-matching models | 01:21 |
| mwk | either the synth flow is buggy and we're using the FFs with set wrong, or the sim library is | 01:22 |
| *** emeb has joined #yosys | 01:23 | |
| *** emeb_mac has joined #yosys | 01:25 | |
| *** Degi has quit IRC | 01:51 | |
| *** Degi has joined #yosys | 01:53 | |
| *** citypw has joined #yosys | 02:03 | |
| *** proteusguy has quit IRC | 02:04 | |
| *** citypw has quit IRC | 03:30 | |
| *** emeb has left #yosys | 03:50 | |
| *** az0re has joined #yosys | 04:08 | |
| *** az0re has quit IRC | 04:24 | |
| *** FFY00 has quit IRC | 05:47 | |
| *** acertain has joined #yosys | 06:42 | |
| *** emeb_mac has quit IRC | 06:46 | |
| acertain | i'm trying to use yosys as a frontend for verification tools (& not actually for synthesis), is there a way to unset a reg/cause the generated transition rel to under some conditions not implicitly set next var = var? | 06:48 |
| acertain | actually seems like btor2 might not support this? | 06:49 |
| *** nengel has joined #yosys | 07:03 | |
| *** jakobwenzel has joined #yosys | 07:52 | |
| *** dys has quit IRC | 07:56 | |
| *** dys has joined #yosys | 08:10 | |
| *** kraiskil has joined #yosys | 08:24 | |
| *** adjtm_ has quit IRC | 08:24 | |
| *** Asu has joined #yosys | 08:27 | |
| *** citypw has joined #yosys | 09:05 | |
| *** citypw has quit IRC | 09:10 | |
| *** citypw has joined #yosys | 09:22 | |
| *** Asu has quit IRC | 09:37 | |
| *** Asu has joined #yosys | 09:39 | |
| *** Asu has quit IRC | 09:41 | |
| *** X-Scale has quit IRC | 09:49 | |
| *** X-Scale` has joined #yosys | 09:49 | |
| *** X-Scale` is now known as X-Scale | 09:49 | |
| *** proteusguy has joined #yosys | 09:52 | |
| *** Asu has joined #yosys | 10:14 | |
| *** _whitelogger has quit IRC | 10:21 | |
| *** _whitelogger has joined #yosys | 10:23 | |
| *** Asu has quit IRC | 10:39 | |
| *** Asu has joined #yosys | 10:40 | |
| *** Asu has quit IRC | 11:05 | |
| *** Asu has joined #yosys | 11:10 | |
| *** kraiskil has quit IRC | 11:15 | |
| *** kraiskil has joined #yosys | 11:28 | |
| *** kraiskil has joined #yosys | 11:30 | |
| *** kraiskil has joined #yosys | 11:32 | |
| *** AdamHorden has quit IRC | 11:44 | |
| *** AdamHorden has joined #yosys | 11:56 | |
| *** maartenBE has quit IRC | 12:02 | |
| *** smarter has quit IRC | 12:10 | |
| *** smarter_ has joined #yosys | 12:10 | |
| *** ZipCPU has quit IRC | 12:12 | |
| *** ZipCPU has joined #yosys | 12:15 | |
| *** FFY00 has joined #yosys | 12:16 | |
| *** minicom has joined #yosys | 13:02 | |
| ZipCPU | acertain: What is it you are trying to do? I'm not sure I get it, and I'm also not sure I get why it can't be done in logic in the first place | 13:21 |
| *** TFKyle has quit IRC | 13:24 | |
| *** TFKyle has joined #yosys | 13:25 | |
| acertain | in this case i want to check if an incomplete implementation is sufficient for proving a property | 13:38 |
| *** kraiskil has quit IRC | 13:52 | |
| acertain | regs start as undefined? and verification tools can check if there exists a bad initial value for regs? so i want to be able to set them back to undefined to check the safety property without having to fully specify everything | 13:53 |
| acertain | i guess i could have a big array reg & take bits from it as needed? but i think that would be very inefficient | 14:00 |
| *** jakobwenzel has quit IRC | 14:06 | |
| *** kraiskil has joined #yosys | 14:07 | |
| *** jakobwenzel has joined #yosys | 14:07 | |
| FL4SHK | So I'm doing `cover(past_rst && bus.empty)` | 14:08 |
| FL4SHK | this does not seem to be working | 14:09 |
| FL4SHK | `if (rst) begin past_rst <= 1'b1; end` | 14:09 |
| FL4SHK | it also won't work for `cover(past_rst)` | 14:09 |
| *** FFY00 has quit IRC | 14:21 | |
| *** kraiskil has quit IRC | 14:55 | |
| *** jakobwenzel has quit IRC | 15:10 | |
| *** FFY00 has joined #yosys | 15:45 | |
| *** FFY00 has quit IRC | 15:46 | |
| *** FFY00 has joined #yosys | 15:47 | |
| *** FFY00 has quit IRC | 15:48 | |
| *** FFY00 has joined #yosys | 15:50 | |
| *** citypw has quit IRC | 16:22 | |
| *** jeanthom has joined #yosys | 16:25 | |
| *** FFY00 has quit IRC | 16:44 | |
| *** FFY00 has joined #yosys | 16:45 | |
| *** craigo has joined #yosys | 16:53 | |
| *** craigo has quit IRC | 16:59 | |
| *** craigo has joined #yosys | 16:59 | |
| ZipCPU | FL4SHK: Did you double check that past_rst was initialized to zero? | 17:01 |
| ZipCPU | 'cause ... it should work just fine in a cover statement--it's just logic. | 17:01 |
| FL4SHK | ZipCPU: I'm not sure it got initialized properly given that this is nmigen | 17:01 |
| *** craigo has quit IRC | 17:02 | |
| ZipCPU | In order for past_valid to work, it needs to be initialized. | 17:02 |
| FL4SHK | I think I initialized it wrongly | 17:02 |
| *** craigo has joined #yosys | 17:05 | |
| FL4SHK | ZipCPU: so I'm probably doing this wrongly, but I'm trying to ensure that `cover` doesn't hit an invalid state | 17:09 |
| ZipCPU | Why not assert that the invalid state will never happen? | 17:10 |
| *** kraiskil has joined #yosys | 17:12 | |
| *** anticw has quit IRC | 17:15 | |
| *** Max-P has quit IRC | 17:15 | |
| *** bluesceada has quit IRC | 17:15 | |
| *** anticw has joined #yosys | 17:18 | |
| *** show1 has joined #yosys | 17:18 | |
| *** Degi has quit IRC | 17:18 | |
| *** Max-P has joined #yosys | 17:19 | |
| *** bluesceada has joined #yosys | 17:20 | |
| *** Degi has joined #yosys | 17:25 | |
| *** oldtopman has quit IRC | 17:26 | |
| *** alexhw has quit IRC | 17:26 | |
| *** bzztploink has quit IRC | 17:26 | |
| *** gtw has quit IRC | 17:26 | |
| *** thardin has quit IRC | 17:26 | |
| *** somlo has quit IRC | 17:26 | |
| *** FL4SHK has quit IRC | 17:26 | |
| *** josi has quit IRC | 17:26 | |
| *** pepijndevos has quit IRC | 17:26 | |
| *** oldtopman has joined #yosys | 17:29 | |
| *** alexhw has joined #yosys | 17:29 | |
| *** thardin has joined #yosys | 17:29 | |
| *** bzztploink has joined #yosys | 17:29 | |
| *** gtw has joined #yosys | 17:29 | |
| *** somlo has joined #yosys | 17:29 | |
| *** FL4SHK has joined #yosys | 17:29 | |
| *** josi has joined #yosys | 17:29 | |
| *** pepijndevos has joined #yosys | 17:29 | |
| *** SpaceCoaster has joined #yosys | 18:03 | |
| *** N2TOH has joined #yosys | 18:05 | |
| *** N2TOH_ has quit IRC | 18:09 | |
| *** dys has quit IRC | 18:37 | |
| *** smarter_ is now known as smarter | 19:23 | |
| *** kraiskil has quit IRC | 19:31 | |
| *** fevv8[m] has quit IRC | 19:45 | |
| *** fevv8[m] has joined #yosys | 19:48 | |
| *** az0re has joined #yosys | 19:59 | |
| *** emeb_mac has joined #yosys | 20:38 | |
| *** Asu has quit IRC | 21:34 | |
| *** cr1901_modern has quit IRC | 21:35 | |
| *** cr1901_modern has joined #yosys | 21:36 | |
| *** emeb has joined #yosys | 22:42 | |
| *** kraiskil has joined #yosys | 22:48 | |
| *** emeb has quit IRC | 23:46 | |
Generated by irclog2html.py 2.17.2 by Marius Gedminas - find it at https://mg.pov.lt/irclog2html/!