clifford changed the topic of #yosys to: Yosys Open SYnthesis Suite: http://www.clifford.at/yosys/ -- Channel Logs: https://irclog.whitequark.org/yosys
tpb has quit [Remote host closed the connection]
tpb has joined #yosys
Degi_ has joined #yosys
Degi has quit [Ping timeout: 265 seconds]
Degi_ is now known as Degi
peeps[zen] has joined #yosys
peepsalot has quit [Ping timeout: 265 seconds]
FFY00_ has quit [Ping timeout: 276 seconds]
citypw has joined #yosys
peeps[zen] is now known as peepsalot
danvet has joined #yosys
danvet has quit [Ping timeout: 248 seconds]
jophish has joined #yosys
<jophish> Hi all
<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
<jophish> This is the source and the sby spec, along with its stout: https://gist.github.com/61562eaa4980d5a9b09e3d03d4c6229c
<jophish> it complains that my reset signal is never touched, and I suspect that this might be part of the problem
<gatecat> jophish: I think you might need to pass -fpsl to ghdl?
<gatecat> probably at the analysis stage
<jophish> ah, I did indeed figure that out and forgot to report here!
<jophish> thanks gatecat
<jophish> (although ghdl then goes on to choke on my psl comments)
<jophish> have got the same problem with systemverilog however: https://gist.github.com/cf9b14fdc58a45fb9c030cf59c2e2a8a
<jophish> here I'm asserting that a const `0` is covered :)
<jophish> I'm sure that it's because of this funky reset
<gatecat> Yosys doesn't support PSL comments in SystemVerilog
<gatecat> `always @(posedge clk_i) cover(s_0);`, outside of a comment, should work, though
<jophish> ah, these are SVA comments I believe
<gatecat> right, SVA comments aren't supported either
<gatecat> only a subset of SVA, not in comments, are supported by Yosys (at least the OSS version)
<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
<jophish> ah, gotcha, indeed it works when they're not in comments
<jophish> Is there a name for the commented mode and non commented mode so I can properly make a feature request for clash?
<jophish> Also, is there an example anywhere of SVA being used with Yosys
<jophish> I seem to be getting a syntax error trying to use a property statement
<jophish> complains about that `TOK_PROPERTY`
<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?
<jophish> ah, ` always @(posedge clk_i) isOn: cover (result);`
<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?
<gatecat> I've only ever seen the commented mode used for PSL before
<gatecat> I didn't even know it was an option for SVA until now...
<jophish> well, I think I've about implemented Yosys compatible covers and assertions for clash :D
danvet has joined #yosys
vidbina has joined #yosys
<jophish> hmm, `nextpnr-ecp5` errors out when given code with a `cover` directive in: `ERROR: cell type '$cover' is unsupported (instantiated as 'isOff')`
<jophish> Do I need to wrap these in `ifdef formal` or something?
<jophish> seems as though they could (in theory) provide some useful information to the compiler...
citypw has quit [Ping timeout: 240 seconds]
jakobwenzel1 has joined #yosys
roamingr1 has joined #yosys
roamingr1 has quit [Ping timeout: 260 seconds]
jakobwenzel1 has quit [Ping timeout: 260 seconds]
<Lofty> jophish: yes, they're not synthesisable.
<jophish> :thu
<jophish> 👍️ *
FFY00_ has joined #yosys
moony has quit [Quit: Bye!]
moony has joined #yosys
krispaul has quit [Ping timeout: 265 seconds]
krispaul has joined #yosys
danvet has quit [Ping timeout: 260 seconds]
lf_ has quit [Ping timeout: 250 seconds]
lf has joined #yosys