Commit Graph

785 Commits

Author SHA1 Message Date
Alan Mishchenko f2e4ceb0e3 Update to "lutexact". 2024-11-10 19:12:40 -08:00
Alan Mishchenko c787e32f86 Adding postiive minterm count for random functions generated by "lutexact". 2024-11-05 22:01:07 -08:00
Alan Mishchenko 091ff4e7a9 Adding generation of random functions to "lutexact" 2024-11-05 19:23:04 -08:00
alanminko a239dd8c0b
Merge pull request #328 from heshpdx/master
Perf improvement in satsolver
2024-10-21 01:38:40 -07:00
Alan Mishchenko 2e3384390a Updating "lutexact" to run on symmetric functions. 2024-10-07 14:10:02 +07:00
Mahesh Madhav ad8f8a2aab Convert the other divide to a multiply 2024-09-03 04:48:07 +00:00
Mahesh Madhav cd711089d7 Perf improvement in satsolver
Switch one FP divide to an FP multiply (variable is constant).
Calculate ratio inside of verbosity clause, since that is where it is used.
2024-09-03 04:30:14 +00:00
Alan Mishchenko c2391686ea Adding BLIF dumping to "lutexact". 2024-08-13 20:03:18 -07:00
Alan Mishchenko 81fcf8494e Updating "lutexact" to support single-rail LUT cascade. 2024-08-12 16:26:55 -07:00
alanminko 0129b4c60a
Merge pull request #316 from YosysHQ/povik/yosyshq-commands
Pull command changes from YosysHQ fork
2024-08-08 14:59:31 -07:00
Martin Povišer 1383c76464 Pull YosysHQ read_cex/write_cex changes
See

 - YosysHQ/abc#19
 - YosysHQ/abc#16
 - commit 6234e18d
 - YosysHQ/abc#14
 - YosysHQ/abc#12
 - YosysHQ/abc#11

Co-authored-by: Jannis Harder <me@jix.one>
Co-authored-by: Claire Xenia Wolf <claire@clairexen.net>
Co-authored-by: Miodrag Milanovic <mmicko@gmail.com>
2024-08-07 15:46:43 +02:00
Martin Povišer 57c3bd36f2 Patch to support WASI builds
Co-authored-by: whitequark <whitequark@whitequark.org>
2024-08-07 14:49:13 +02:00
Robert O'Callahan e0a9c29e5a Instead of throwing C++ exceptions, just print an error message and abort
Many C++ projects forbid the use of exceptions. These are not recoverable
errors anyway, so just abort.
2024-08-06 17:51:15 +00:00
Robert O'Callahan 6c6260465e Make `lbool` explicitly signed
This avoids issues due to some platforms making `char` signed and others
unsigned. For example, currently the result of promoting `(lbool)-1` to `int`
can differ on different platforms. See
50ffa10848/lib/bill/bill/sat/interface/abc_bsat2.hpp (L156)
for an example of that.
2024-06-28 01:07:10 +00:00
Alan Mishchenko 8ec95e85c6 Bug fix. 2024-05-19 15:03:12 -07:00
Alan Mishchenko c64f927828 Various changes and bug fixes. 2024-05-19 14:47:18 -07:00
Alan Mishchenko 2c02ae89a0 Updating the previous commit. 2024-05-15 09:41:14 -07:00
Alan Mishchenko c906dfb748 Upgrading "twoexact" to read relations in an updated format. 2024-05-15 09:33:57 -07:00
Alan Mishchenko bc725b85de Bug fix in CNF generation for &glucose (three more places). 2024-04-15 20:29:38 -07:00
Alan Mishchenko 2d6b5c9adc Bug fix in CNF generation for &glucose. 2024-04-15 20:25:43 -07:00
Alan Mishchenko b0d2ff1c63 Exact synthesis using NAND-gates. 2024-03-24 00:10:08 +09:00
Allen Ho d87b1cd543 fixed some warnings in bsat2 2024-03-04 10:16:14 +08:00
Alan Mishchenko eb24d29777 More changes. 2024-03-02 17:10:30 -08:00
Alan Mishchenko b73f1030a6 More changes. 2024-03-02 17:03:42 -08:00
Alan Mishchenko b627aa7cb5 More changes. 2024-03-02 16:57:00 -08:00
Alan Mishchenko ce44eda85a More changes. 2024-03-02 16:46:09 -08:00
Alan Mishchenko f6f542c873 More changes to compile with namespaces. 2024-03-02 16:38:16 -08:00
Alan Mishchenko 4de4605836 More changees to compile new code with namespaces. 2024-03-02 16:31:41 -08:00
Alan Mishchenko a1159d98df Fixing a compiler problem with namespaces. 2024-03-02 16:10:37 -08:00
Alan Mishchenko 1bf21626c0 Bug fix. 2023-10-23 11:04:35 -07:00
Alan Mishchenko 538ecb4515 Updating printouts. 2023-10-23 09:38:24 -07:00
Alan Mishchenko 55aba1731c Fixing a typo. 2023-09-08 19:57:45 +07:00
alanminko 3daa630a03
Merge pull request #242 from DanielG/spelling-fixes
treewide: Fix spelling mistakes
2023-09-05 13:31:50 +07:00
Alan Mishchenko 1cdb2dacee Problem fix: <unistd.h> is not properly defined. 2023-09-04 08:13:00 +07:00
Daniel Gröber b7d1435db1 treewide: Fix spelling mistakes
A particularly pedantic set of changes currently used in Debian

Authored-By: Ruben Undheim <ruben.undheim@gmail.com>
2023-08-27 14:13:20 +02:00
Alan Mishchenko 756e21a81d Problem fix: <unistd.h> is not properly defined. 2023-08-20 15:50:59 +07:00
Alan Mishchenko 039f05cb56 Adding preprocessing to command &splitsat. 2023-07-27 20:50:02 -07:00
Alan Mishchenko 74157fc0ab New command &splitsat. 2023-07-27 16:00:17 -07:00
Alan edb7fb100d Removing checking for the binary in the current dir. 2023-07-26 20:27:17 -07:00
Alan Mishchenko d9f6af51af Experiment with CNF cofactoring. 2023-07-24 16:21:42 -07:00
alanminko ea40a95830
Merge pull request #196 from hzeller/20221121-fix-ub
Fix undefined behavior in signed/unsigned shifting.
2023-05-18 22:33:01 -07:00
Alan Mishchenko a5f4841486 Adding BLIF dumping to MiniAIG. 2023-03-13 20:51:40 +07:00
Alan Mishchenko c1b2a64c2e Alternative binary name on Linux. 2023-03-11 20:29:04 +07:00
Alan Mishchenko 8742534db8 More compiler warnings. 2023-03-01 01:12:36 -08:00
Alan Mishchenko b57b546494 Compiler warnings. 2023-02-28 15:16:31 +07:00
Alan Mishchenko 38ad178e9e Changes and bug fixes in exact synthesis. 2023-02-13 06:39:10 +01:00
Alan Mishchenko 66a5fe7aec Experiments with exact synthesis. 2022-12-29 17:15:53 -08:00
Alan Mishchenko 27b8cce3fe Experiments with precomputation. 2022-12-18 20:06:07 -08:00
Alan Mishchenko 6e6c728b65 Another way of dumping QBF problem into a file. 2022-12-03 20:29:06 -08:00
Henner Zeller 74740dc894 Fix undefined behavior in signed/unsigned shifting.
Discovered by UBSAN as invalid attempts at shifting signed integers.

Signed-off-by: Henner Zeller <hzeller@google.com>
2022-11-21 12:36:41 -08:00