Then I create SAT instances to see if they actually are the same. If not I use the counter example as additional simulation input to..
-
-
Replying to @oe1cxw @johnregehr
.. break other pairs that are still marked as candidates, then I create a SAT instance for the next candidate pair, and so on.
1 reply 0 retweets 0 likes -
Replying to @oe1cxw @johnregehr
There is some additional handling for when to signals are the exact opposite, then I replace one with the inverse of the other.
1 reply 0 retweets 0 likes -
Replying to @oe1cxw @johnregehr
There is also some special handling for constant zero and constant one.
1 reply 0 retweets 1 like -
Replying to @oe1cxw @johnregehr
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.
1 reply 0 retweets 0 likes -
Replying to @oe1cxw @johnregehr
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.
1 reply 0 retweets 0 likes -
Replying to @oe1cxw @johnregehr
But "freduce" can operate on a more coarse grain circuit representation (with adds and shifts and other word-wide operations).
1 reply 0 retweets 0 likes -
Replying to @oe1cxw @johnregehr
This is thanks to the SatGen class in Yosys that essentially implement an SMT solver in Yosys.
1 reply 0 retweets 0 likes -
Replying to @oe1cxw @johnregehr
(When I wrote that, btw, I simply did not know that SMT solvers existed. Otherwise I wouldn't have re-invented the wheel. :)
1 reply 0 retweets 1 like -
Replying to @oe1cxw @johnregehr
So it can operate on a circuit on a coarse grain description, but it only performs bit-level optimizations: rewiring and maybe add inverters
1 reply 0 retweets 0 likes
Replying to @oe1cxw @johnregehr
I think that's pretty much it. </tweetstorm> :)
1:03 PM - 28 Sep 2017
0 replies
0 retweets
1 like
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.