| *** tpb has joined #yosys | 00:00 | |
| *** Degi_ has joined #yosys | 00:17 | |
| *** Degi has quit IRC | 00:19 | |
| *** Degi_ is now known as Degi | 00:19 | |
| *** peeps[zen] has joined #yosys | 00:25 | |
| *** peepsalot has quit IRC | 00:26 | |
| *** FFY00_ has quit IRC | 02:50 | |
| *** citypw has joined #yosys | 03:20 | |
| *** peeps[zen] is now known as peepsalot | 04:33 | |
| *** danvet has joined #yosys | 07:49 | |
| *** danvet has quit IRC | 08:30 | |
| *** jophish has joined #yosys | 09:22 | |
| jophish | Hi all | 09:23 |
|---|---|---|
| jophish | I've got a blink.vhdl example, and I'd like to be sure that the LED will be both on and off. I've specified this as PSL, however I can't seem to get this to work with symbiyosys (for example when I make the design break, it still reports everything is A-OK | 09:29 |
| jophish | This is the source and the sby spec, along with its stout: https://gist.github.com/61562eaa4980d5a9b09e3d03d4c6229c | 09:31 |
| jophish | it complains that my reset signal is never touched, and I suspect that this might be part of the problem | 09:31 |
| gatecat | jophish: I think you might need to pass -fpsl to ghdl? | 09:55 |
| gatecat | probably at the analysis stage | 09:55 |
| jophish | ah, I did indeed figure that out and forgot to report here! | 09:56 |
| jophish | thanks gatecat | 09:56 |
| jophish | (although ghdl then goes on to choke on my psl comments) | 09:56 |
| jophish | have got the same problem with systemverilog however: https://gist.github.com/cf9b14fdc58a45fb9c030cf59c2e2a8a | 09:57 |
| jophish | here I'm asserting that a const `0` is covered :) | 09:57 |
| jophish | I'm sure that it's because of this funky reset | 09:59 |
| gatecat | Yosys doesn't support PSL comments in SystemVerilog | 10:07 |
| gatecat | `always @(posedge clk_i) cover(s_0);`, outside of a comment, should work, though | 10:08 |
| jophish | ah, these are SVA comments I believe | 10:09 |
| gatecat | right, SVA comments aren't supported either | 10:09 |
| gatecat | only a subset of SVA, not in comments, are supported by Yosys (at least the OSS version) | 10:09 |
| gatecat | Tabby CAD (Yosys with a Verific based frontend) supports a much bigger range of SVA features, but I still believe it requires the SVA to be in the body of the code and not in comments | 10:10 |
| jophish | ah, gotcha, indeed it works when they're not in comments | 10:10 |
| jophish | Is there a name for the commented mode and non commented mode so I can properly make a feature request for clash? | 10:10 |
| jophish | Also, is there an example anywhere of SVA being used with Yosys | 10:24 |
| jophish | I seem to be getting a syntax error trying to use a property statement | 10:25 |
| jophish | https://gist.github.com/5830708604f948e60f15eb7bff5be8ab | 10:25 |
| jophish | complains about that `TOK_PROPERTY` | 10:25 |
| jophish | actually to avoid an X-Y problem, is there a way to name properties so that instead of `Unreached cover statement at blink.sv:43.26-43.36.` I can get some pretty name? | 10:36 |
| jophish | ah, ` always @(posedge clk_i) isOn: cover (result);` | 10:40 |
| gatecat | 11:10 AM <jophish> Is there a name for the commented mode and non commented mode so I can properly make a feature request for clash? | 10:43 |
| gatecat | I've only ever seen the commented mode used for PSL before | 10:43 |
| gatecat | I didn't even know it was an option for SVA until now... | 10:43 |
| jophish | well, I think I've about implemented Yosys compatible covers and assertions for clash :D | 10:45 |
| *** danvet has joined #yosys | 11:25 | |
| *** vidbina has joined #yosys | 12:12 | |
| jophish | hmm, `nextpnr-ecp5` errors out when given code with a `cover` directive in: `ERROR: cell type '$cover' is unsupported (instantiated as 'isOff')` | 12:59 |
| jophish | Do I need to wrap these in `ifdef formal` or something? | 13:00 |
| jophish | seems as though they could (in theory) provide some useful information to the compiler... | 13:02 |
| *** citypw has quit IRC | 13:39 | |
| *** jakobwenzel1 has joined #yosys | 13:52 | |
| *** roamingr1 has joined #yosys | 14:11 | |
| *** roamingr1 has quit IRC | 15:14 | |
| *** jakobwenzel1 has quit IRC | 15:33 | |
| Lofty | jophish: yes, they're not synthesisable. | 15:37 |
| jophish | :thu | 15:37 |
| jophish | 👍️ * | 15:37 |
| *** FFY00_ has joined #yosys | 18:04 | |
| *** moony has quit IRC | 19:47 | |
| *** moony has joined #yosys | 19:53 | |
| *** krispaul has quit IRC | 20:02 | |
| *** krispaul has joined #yosys | 20:03 | |
| *** danvet has quit IRC | 22:01 | |
| *** lf_ has quit IRC | 23:16 | |
| *** lf has joined #yosys | 23:16 | |
Generated by irclog2html.py 2.17.2 by Marius Gedminas - find it at https://mg.pov.lt/irclog2html/!