Author here. The theme is "You could have invented BDDs" -- the article works up to them in hopefully-natural steps, with some applications along the way. The Python code is shorter than I've been able to find elsewhere.
Fabian Giesen pointed out last night that the example "carry-lookahead adder" was misnamed and it's a kind of https://en.wikipedia.org/wiki/Carry-select_adder. Oops. Going to fix that soon. I'd read the carry-lookahead article and was like "this derivation seems right but I don't see how you might invent it." Trying to fix that ended up reinventing something different. I should've noted there in the article that I felt iffy about what I'd called the circuit, even though it was functionally equivalent. (Better still of course to code up Wikipedia's version and check structural equivalence, if there'd been time.)
> We just checked whether two different 64-bit adder circuits produce the same outputs for all 2^129 of the possible values of A, B, and carry. It took only a moment in interpreted Python. Magic!
This kind of processing is what makes me wonder on how computer, nowadays, still have foundations on _simple_ and _basic_ logic, combined and processed at zillions of repetitions per second.
I'm not sure I understand your comment. It isn't like it actually ran all 2^129 inputs. It created a BDD for each and determined they were the same. (Right?)
No, I understand that running such range would be impossible. What amazes me is how you can (sometimes) simplify things, and the "power" that being able do to zillions of calculations can have when you have already simplified your problem to some general proof. :) Well, that's what I meant.
I think this needs a bit more motivation (why do I want to know about BDDs) and more pictures. The code is great for playing with things and remembering better but the fundamental concepts would be clearer with more pictures.
Fabian Giesen pointed out last night that the example "carry-lookahead adder" was misnamed and it's a kind of https://en.wikipedia.org/wiki/Carry-select_adder. Oops. Going to fix that soon. I'd read the carry-lookahead article and was like "this derivation seems right but I don't see how you might invent it." Trying to fix that ended up reinventing something different. I should've noted there in the article that I felt iffy about what I'd called the circuit, even though it was functionally equivalent. (Better still of course to code up Wikipedia's version and check structural equivalence, if there'd been time.)