Characterize time-to-proof for IR/Netlist equality checks across ops and arg sizes.

[RobSpringer]

This would be useful for getting some idea of how long we should expect some proofs to take - it's at least a necessary first step.

[RobSpringer]

This ain't done. That patch was just the first step.

[cdleary]

I think the primary motivation here was: if we have a multiplier that's NxM->[N+M] how long can we reasonably expect the proof (LEC of XLS IR vs structural netlist) to take before it closes as we sweep N and M. Without empirical observation there's not a good theoretical basis for knowing how long something might continue to take but characterization curves would help give a feel. With the XLS LEC flow working on the OSS SKY130 backend this can likely be done/demonstrated/tested all in OSS now, but I think this is also on the back burner, so marking as long term enhancement.