4 ms·

Cool! Very similar techniques can be used in the hardware domain. For these types of problems, at least, I have found SRI's yices solver to be much, much more

Cool! Very similar techniques can be used in the hardware domain. For these types of problems, at least, I have found SRI's yices solver to be much, much more performant than Armando's CEGIS solver. Do you have any tips on other solvers you've found to be faster for exists-forall problems? Here's a raw example of a 32-bit adder super-optimized according to rough delay, gate complexity, and wire complexity models embedded in the 2QBF: https://share.riseup.net/#xg2ySn41zmhtHtmrlQWn5Q https://share.riseup.net/#xg2ySn41zmhtHtmrlQWn5Q . According to post-PAR results from Innovus, it can actually (barely) beat DesignWare adders at some points in the trade-off space.

rbodik 7y ago
Hi, this looks like a strong result. Congratulations! Short answer: to scale up hardware synthesis, it may be necessary to change the encoding rather than look for a better solver. More details: I should first say that I have limited experience with synthesizing hardware. My lessons come from [1], where synthesized a small Wallace Tree multiplier. What that taught me is that hardware arithmetic circuits should perhaps not be formulated as a 2QBF problem -- because you might need too many counterexample inputs to terminate the CEGIS loop. Instead, I believe that the circuit synthesis should use algebraic reasoning (for correctness) and combinatorial reasoning to explore the space of candidate circuits. Since one symbolic input is sufficient to show correctness, the problem simplifies from 2QBF to SAT. This idea is briefly explained in Sec 4.1 in [3], a project that synthesizes software expressions that look very much like hardware circuits (permutations and such) [2]. I am happy to discuss this in person if it might be helpful to your work. Both Mangpo (the author of [2,3]) and I will be at the conference. [1] https://ieeexplore.ieee.org/document/5227085 https://ieeexplore.ieee.org/document/5227085 [2] https://github.com/mangpo/swizzle-inventor https://github.com/mangpo/swizzle-inventor [3] https://github.com/mangpo/mangpo.github.io/blob/master/papers/swizzle-inventor-asplos19.pdf https://github.com/mangpo/mangpo.github.io/blob/master/paper...,

rbodik 7y ago

Hi, this looks like a strong result. Congratulations! Short answer: to scale up hardware synthesis, it may be necessary to change the encoding rather than look for a better solver. More details: I should first say that I have limited experience with synthesizing hardware. My lessons come from [1], where synthesized a small Wallace Tree multiplier. What that taught me is that hardware arithmetic circuits should perhaps not be formulated as a 2QBF problem -- because you might need too many counterexample inputs to terminate the CEGIS loop. Instead, I believe that the circuit synthesis should use algebraic reasoning (for correctness) and combinatorial reasoning to explore the space of candidate circuits. Since one symbolic input is sufficient to show correctness, the problem simplifies from 2QBF to SAT. This idea is briefly explained in Sec 4.1 in [3], a project that synthesizes software expressions that look very much like hardware circuits (permutations and such) [2]. I am happy to discuss this in person if it might be helpful to your work. Both Mangpo (the author of [2,3]) and I will be at the conference. [1] https://ieeexplore.ieee.org/document/5227085 https://ieeexplore.ieee.org/document/5227085 [2] https://github.com/mangpo/swizzle-inventor https://github.com/mangpo/swizzle-inventor [3] https://github.com/mangpo/mangpo.github.io/blob/master/papers/swizzle-inventor-asplos19.pdf https://github.com/mangpo/mangpo.github.io/blob/master/paper...,