diff options
| author | Marcelina Kościelnicka <mwk@0x04.net> | 2021-08-04 00:02:16 +0200 |
|---|---|---|
| committer | Marcelina Kościelnicka <mwk@0x04.net> | 2021-08-09 16:54:35 +0200 |
| commit | d25b9088c83ba68b938ef9f0d97793a08001a9fe (patch) | |
| tree | 850d768b062d231f0ff7d9fbc3bab8d642a861c6 /README.md | |
| parent | d8fcf1ab2568ae88aa3a2c9548578b899cc4d383 (diff) | |
| download | yosys-d25b9088c83ba68b938ef9f0d97793a08001a9fe.tar.gz yosys-d25b9088c83ba68b938ef9f0d97793a08001a9fe.tar.bz2 yosys-d25b9088c83ba68b938ef9f0d97793a08001a9fe.zip | |
Refactor common parts of SAT-using optimizations into a helper.
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
Diffstat (limited to 'README.md')
0 files changed, 0 insertions, 0 deletions