Because in hardware you can wire any bit anywhere it must compare bits, not words, and there are n^2/2 pairs..
-
I think stuff like this for gate level circuits is as least as old as SAT solvers. Probably older, since BDDs can be used for that also.
But "freduce" can operate on a more coarse grain circuit representation (with adds and shifts and other word-wide operations).
-
-
This is thanks to the SatGen class in Yosys that essentially implement an SMT solver in Yosys.
-
(When I wrote that, btw, I simply did not know that SMT solvers existed. Otherwise I wouldn't have re-invented the wheel. :)
- Show replies
New conversation -
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.