philzook · HackerTrans

2 months agodiscuss

It's a really neat board. You can get kits from aliexpress etc. I wrote up some notes here https://www.philipzucker.com/td4-4bit-cpu/ . English descriptions are not so readily available.

I also had some fun modelling the chips in verilog and model checking a verilog interpreter against them. https://www.philipzucker.com/td4_ebmc/ George Rennie got a similar thing working using the yosys toolchain https://github.com/georgerennie/philip_zucker_sby_demo

4 months agodiscuss

Interesting. I think there is even more similarity if you are trying to find a "best" list from which two other lists are thinned.

6 months agodiscuss

https://www.philipzucker.com/ I blog regularly about egraphs, SMT solvers, assembly verification, theorem proving

8 months agodiscuss

I'm a fan. I've been building a proof assistant directly on the z3py api. https://pypi.org/project/knuckledragger/0.1.3/

9 months agodiscuss

I'm working on Knuckledragger, a proof assistant shallowly based upon z3py https://github.com/philzook58/knuckledragger

Yesterday I proved the infinitude of primes, which I was pretty happy with. https://www.philipzucker.com/knuckle_primes/ A trivial theorem in the scheme of things, but one for which z3 certainly can't do it on it's own.

comments