ChanServ changed the topic of #yosys to: Yosys Open SYnthesis Suite: https://github.com/YosysHQ/yosys/ | Channel logs: https://libera.irclog.whitequark.org/yosys/
tpb has quit [Remote host closed the connection]
tpb has joined #yosys
freemint has quit [Quit: Leaving]
gsmecher has quit [Ping timeout: 240 seconds]
GenTooMan has quit [Ping timeout: 250 seconds]
GenTooMan has joined #yosys
GenTooMan has quit [Ping timeout: 250 seconds]
GenTooMan has joined #yosys
GenTooMan has quit [Ping timeout: 250 seconds]
GenTooMan has joined #yosys
FabM has joined #yosys
FabM has joined #yosys
FabM has quit [Changing host]
oldtopman has quit [Ping timeout: 252 seconds]
Sarayan has quit [Remote host closed the connection]
emeb_mac has quit [Quit: Leaving.]
cr1901 has quit [Ping timeout: 240 seconds]
oldtopman has joined #yosys
vidbina has joined #yosys
pepijndevos[m] has joined #yosys
adjtm has quit [Quit: Leaving]
piegames has quit [Ping timeout: 256 seconds]
cr1901 has joined #yosys
indy has quit [Quit: ZNC 1.8.2 - https://znc.in]
indy has joined #yosys
piegames has joined #yosys
<piegames> How can I do "negative" cover statements?
<piegames> Like "if A happens, B should never happen"
<piegames> Or on a more broader level, "this operation never takes longer than four cycles"
GenTooMan has quit [Ping timeout: 250 seconds]
GenTooMan has joined #yosys
GenTooMan has quit [Ping timeout: 250 seconds]
GenTooMan has joined #yosys
vidbina has quit [Ping timeout: 250 seconds]
z0ttel has joined #yosys
z0ttel has quit [Client Quit]
z0ttel has joined #yosys
peepsalot has quit [Ping timeout: 240 seconds]
peepsalot has joined #yosys
vidbina has joined #yosys
FabM has quit [Ping timeout: 240 seconds]
z0ttel has quit [Ping timeout: 250 seconds]
z0ttel has joined #yosys
smkz has quit [Quit: reboot]
smkz has joined #yosys
adjtm has joined #yosys
adjtm has quit [Remote host closed the connection]
GenTooMan has quit [Ping timeout: 240 seconds]
vidbina has quit [Ping timeout: 252 seconds]
GenTooMan has joined #yosys
gsmecher has joined #yosys
z0ttel has quit [Quit: https://quassel-irc.org - Komfortabler Chat. Überall.]
<mwk> piegames: that sounds like a straightforward assertion, assert !(a_happened && b)?
<tnt> Is there any way to compare two synthesis results from a "topology" PoV ? Like the names of signals/cells is not stable obviously but looking at LUT INIT values, and how they're connected to each other and to FF, it should be possible to find equivalent to match the two graphs and find the parts that are different.
<killjoy> This sounds like LEC.
<killjoy> I don't know about opensource tools to do that, but this is what Cadence's Conformal LEC does. (They probably renamed it, they went through a rebranding a few years ago.)
<tnt> yeah. I mean I know they are _not_ equivalent, but trying to find the differences.
<killjoy> Yeah, you could ask lec these questions and it would show you.
<killjoy> Names didn't really matter, it basically did graph comparisons.
<tnt> I know I used a LVS tool to do SKY130 stuff, comparing the post-synthesis netlist with the extracted netlist after pnr.
<tnt> Maybe I could use that.
<killjoy> It's usually used to verify that synthesis didn't do something weird, but at a high level it really just diffs two designs.
<killjoy> LVS != LEC, not sure if you can do that really.
<killjoy> :shrug: I dunno.
<tnt> Yeah I know they're different, but here I expect the LUT / FF to exist "as-is" exactly the same. LEC would check if they do the same thing (no matter how they are arranged), LVS would check if they're wired the same way.
<killjoy> A quick google shows nothing in this realm.
<killjoy> According to https://openlane.readthedocs.io/en/develop/#openlane-architecture it looks like yosys can do LEC?
<tpb> Title: OpenLANE — OpenLANE documentation (at openlane.readthedocs.io)
<killjoy> Digging deeper I don't see anything. I'm curious if you get LVS to work for this.
<piegames> mwk: I was thinking to deep in implications so it actually took me a while to figure that one out. But yes, that works
vidbina has joined #yosys
vidbina has quit [Ping timeout: 250 seconds]
adjtm has joined #yosys
emeb_mac has joined #yosys
<tnt> mmm ... lvs wants structural verilog only, so can't have constants in there, they need to be replaced with GND / VCC cells ... not sure if yosys can do that.
<gatecat> tnt: hilomap
<tnt> gatecat: Ah nice ! I had a look at the command list and missed it.
vidbina has joined #yosys
vidbina has quit [Ping timeout: 250 seconds]
adjtm has quit [Ping timeout: 250 seconds]
<tnt> Next issue is that it doesn't seem to look at params so I'd need to turn ever parametrized instance into something with a unique name encoding the params in the name ...
<tnt> (realistically I'd just need the INIT for the LUT4, the rest doesn't matter much)
V has joined #yosys
<killjoy> The more you go through this, the more I think you really need LEC.
gsmecher has quit [Ping timeout: 250 seconds]