I might be able to weigh in here.<p>Having these tools as open source and freely available is a huge deal for so many industries. I've worked with these tools at an academic level and now at a startup, and it's amazing the magnitude of this enabling technology. Just the tooling investment will be huge, making the core solvers and algorithms more accessible should spawn a whole new wave of startups/research in effectivley employing them. Just these days, I've heard of my friends building theorem provers for EVM bytecode to formally check smart contracts to eliminate bugs like these [0].<p>These synthesis tools roughly break down like this:<p>1. Specify your "program"<p>- In EDA tools, your program is specified in Verilog/VHDL and turns into a netlist, the actual wiring of the gates together.<p>- In 3D printers, your "program" is the CAD model, which can be represented as a series of piecewise triple integrals<p>- In some robots, your program is the set of goals you'd like to accomplish<p>In this stage, it's representation and user friendliness that is king. CAD programs make intuitive sense, and have the expressive power to be able to describe almost anything.
Industrial tools will leverage this high-level representation for a variety of uses, like in the CAD of an airplane, checking if maintenance techs can physically reach every screw, or in EDA providing enough information for simulation of the chip or high-level compilation (Chisel)<p>2. Restructure things until you get to a an NP-complete problem, ideally in the form "Minimize cost subject to some constraints". The result of this optimization can be used to construct a valid program in a lower-level language.<p>- In EDA, this problem looks like "minimize the silicon die area used and layers used and power used subject to the timing requirements of the original Verilog", where the low level representation is the physical realization of the chip<p>- In 3D printers it's something like "minimize time spent printing subject to it being possible to print with the desired infill". Support generation and other things can be rolled in to this to make it possible to print.<p>Here, fun pieces of software in this field of optimization are used; Things like Clasp for Answer Set Programming, Gurobi/CPLEX for Mixed Integer programming or Linear programs, SMT/SAT solvers like Z3 or CVC4 for formal logic proving.<p>A lot of engineering work goes into these solvers, with domain specific extensions driving a lot of progress[1]. We owe a substantial debt to the researchers and industries that have developed solving strategies for these problems, it makes up a significant amount of why we can have nice things, from what frequencies your phone uses [2], to how the NBA decides to schedule basketball games.
This is the stuff that really helps to have as public knowledge. The solvers at their base are quite good, but seeding them with the right domain-specific heuristics makes so many classes of real-world problems solvable.<p>3. Extract your solution and generate code<p>- I'm not sure what this looks like in EDA, my rough guess is a physical layout or mask set with the proper fuckyness to account for the strange effects at that small of a scale.<p>- For 3D printers, this is the emitted G-code<p>- For robots, it's a full motion plan that results in all goals being completed in an efficient manner.<p>[0] <a href="https://hackernoon.com/what-caused-the-latest-100-million-ethereum-bug-and-a-detection-tool-for-similar-bugs-7b80f8ab7279?gi=e1d1a15e098a" rel="nofollow">https://hackernoon.com/what-caused-the-latest-100-million-et...</a><p>[1] <a href="https://slideplayer.com/slide/11885400/" rel="nofollow">https://slideplayer.com/slide/11885400/</a><p>[2] <a href="https://www.youtube.com/watch?v=Xz-jNQnToA0&t=1s" rel="nofollow">https://www.youtube.com/watch?v=Xz-jNQnToA0&t=1s</a>