3 ms·

The language of choice

150 points by panic 9y ago

woliveirajr 9y ago
> 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.
- taeric 9y ago
  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?)
  - woliveirajr 9y ago
    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.
SonOfLilit 9y ago
Been a while since I felt smarter after reading something. Read this, and make the effort to follow along :-)
- abecedarius 9y ago
  That's such a great compliment. Thanks!
abecedarius 9y ago
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 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.)
HurrdurrHodor 9y ago
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.
- abecedarius 9y ago
  Yes, I agree -- I ran out of time trying to get the animations I wanted with d3.js. Thanks for the feedback.
  - SonOfLilit 9y ago
    Maybe circuit diagrams of both kinds of adders and "by the end of this article we will prove that these are equivalent for all 2^192 possible inputs"?

150 points by panic 9y ago

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

taeric 9y ago
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?)
- woliveirajr 9y ago
  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.

SonOfLilit 9y ago

Been a while since I felt smarter after reading something. Read this, and make the effort to follow along :-)

abecedarius 9y ago
That's such a great compliment. Thanks!

abecedarius 9y ago

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

HurrdurrHodor 9y ago

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.

abecedarius 9y ago
Yes, I agree -- I ran out of time trying to get the animations I wanted with d3.js. Thanks for the feedback.
- SonOfLilit 9y ago
  Maybe circuit diagrams of both kinds of adders and "by the end of this article we will prove that these are equivalent for all 2^192 possible inputs"?