aboutsummaryrefslogtreecommitdiffstats
path: root/kernel/qcsat.cc
Commit message (Collapse)AuthorAgeFilesLines
* Add $bmux and $demux cells.Marcelina Kościelnicka2022-01-281-1/+1
|
* Refactor common parts of SAT-using optimizations into a helper.Marcelina Kościelnicka2021-08-091-0/+102
This also aligns the functionality: - in all cases, the onehot attribute is used to create appropriate constraints (previously, opt_dff didn't do it at all, and share created one-hot constraints based on $pmux presence alone, which is unsound) - in all cases, shift and mul/div/pow cells are now skipped when importing the SAT problem (previously only memory_share did this) — this avoids creating clauses for hard cells that are unlikely to help with proving the UNSATness needed for optimization