Claire Xen  🏳️‍⚧️ 🏳️‍🌈 🧙🏻‍♀️ BLM  🏴 🚩

@johnregehr I just watched your 2014 talk on Souper at UW on YouTube. Fascinating how similar it is (was at the time) to "freduce" in Yosys.

The code is not very good.. :) It was more of an experiment than something that one should use in practice. (Also: It's pretty slow.)

Because in hardware you can wire any bit anywhere it must compare bits, not words, and there are n^2/2 pairs..

I wrote it in 2013, so I don't have a very fresh memory from writing it, but the basic idea is this: 1/ (oh I wish I already had 280 :)

I do not consider things from previous cycles, so flip-flops are essentially my "stop condition".

So I have a couple of DAGs. I throw random inputs at them and see which behave the same. Then I mark then as potentially the same node.

Then I create SAT instances to see if they actually are the same. If not I use the counter example as additional simulation input to..

.. break other pairs that are still marked as candidates, then I create a SAT instance for the next candidate pair, and so on.