<p><span class="h-card" translate="no"><a href="https://mastodon.social/@regehr" class="u-url mention">@<span>regehr</span></a></span> so actually the way most logic synthesizers do techmapping (conversion of sea-of-gates to sea-of-large-lookup-tables) is by cut enumeration, and oftentimes there is a SAT solver involved for area reduction or removing irrelevant inputs or stuff</p><p>we have a LUT mapper that doesn't do any of that but it's not very good. so there's a good chance our _normal_ flow will involve a SAT/SMT solver in it</p>
