Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Refactor common parts of SAT-using optimizations into a helper. | Marcelina Kościelnicka | 2021-08-09 | 1 | -0/+76 |
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 |