<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>
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.