The code is not very good.. :) It was more of an experiment than something that one should use in practice. (Also: It's pretty slow.)
-
And there are some heuristics to re-use SAT instances by picking pairs that introduce a low number of new nodes to the last problem.
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.
- 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.