Alan Mishchenko
a6db8bc157
Extending command 'dump_equv' to match inputs by name.
2016-07-27 18:07:51 -07:00
Bruno Schmitt
5604657bdb
Make fx able to handle degenerate divisors:
...
- Constant-1 (a + !a)
- Divisors "a + !ab" and "a!b + b" are equal to "a + b"
Change the way divisors are printed.
Removal of dead code from fx.
2016-07-26 23:53:34 -03:00
Alan Mishchenko
42309cacaa
Extending command 'exact' to handle delay constraints.
2016-07-23 13:13:07 -07:00
Alan Mishchenko
4c6444e34a
Bug fix in 'dump_equiv'.
2016-07-22 13:36:22 -07:00
Alan Mishchenko
3c2c19ce51
Adding new command 'dump_equiv'.
2016-07-21 16:47:30 -07:00
Alan Mishchenko
bfe7333f41
Adding new command 'dump_equiv'.
2016-07-21 16:40:56 -07:00
Alan Mishchenko
aa3d8a65b4
Fix in reading initial state for edge-detection.
2016-07-20 12:55:50 -07:00
Alan Mishchenko
2ba46d52f0
Extension in the detection code.
2016-07-19 20:44:02 -07:00
Alan Mishchenko
190dc37600
Fix in reading initial state for edge-detection.
2016-07-19 13:26:24 -07:00
Alan Mishchenko
0f59f00c74
Tuning &blut implementation.
2016-07-18 20:52:24 -07:00
Alan Mishchenko
2f86667326
Adding output range support to %blast.
2016-07-18 08:34:05 -07:00
Alan Mishchenko
32d1516c64
Adding command 'exact' developed by Mathias Soeken to implement Knuth's exact synthesis algorithm.
2016-07-16 07:51:58 -07:00
Alan Mishchenko
abdf39711f
Several corner-case bugs in %read, &cec, and st.
2016-07-16 07:28:20 -07:00
Alan Mishchenko
1343b8a80c
Fixes and adjustments for the edge computation flow.
2016-07-15 19:56:34 -07:00
Alan Mishchenko
3f8b5cd890
Small fixes and improvements in reporting node counts.
2016-07-15 19:11:17 -07:00
Alan Mishchenko
8bfe8d5210
Adding a debug way to print cuts used in the CNF-generator.
2016-07-13 10:35:02 -07:00
Alan Mishchenko
42ae280089
Removing verbose output in &cec and &syn4.
2016-07-13 09:00:39 -07:00
Alan Mishchenko
3b76bc2792
Bug-fix in SMT-LIB parser (incorrect handling of arithmetic right-shift).
2016-07-12 13:34:06 -07:00
Alan Mishchenko
4ffc14fd56
Small change to make &if not abort the scripts.
2016-07-04 23:54:07 -07:00
Alan Mishchenko
3ad4be259e
Bit-blasting Booth multipliers.
2016-07-04 20:41:50 -07:00
Alan Mishchenko
f3ecc3ffaa
Experiments with edge-based mapping (bug fix).
2016-07-02 12:14:18 -07:00
Alan Mishchenko
84a277b491
Bug fix in blasting shifters with large bit-width.
2016-06-29 15:37:37 -07:00
Alan Mishchenko
d02f9dd4df
Bug fix in blasting shifters with large bit-width.
2016-06-29 15:36:31 -07:00
Alan Mishchenko
7dcba3e27b
Experiments with edge-based mapping.
2016-06-29 15:29:24 -07:00
Alan Mishchenko
688f0269db
Bug fix in blasting shifters with large bit-width.
2016-06-28 09:53:09 -07:00
Ana Petkovska
8e5af90c41
Return the class representative of each function.
2016-06-18 18:51:38 +02:00
Ana Petkovska
6842b8cdbc
Group based exact NPN classification.
2016-06-18 18:42:57 +02:00
Alan Mishchenko
a309569390
New multi-output PLA reader and preprocessor (read_plamo) (updated dist-1 merge).
2016-06-17 22:30:54 -07:00
Alan Mishchenko
720d025234
Complier fix.
2016-06-17 21:54:50 -07:00
Alan Mishchenko
22406e7101
Merged in boschmitt/abc (pull request #28 )
...
Handling D1C and SCC in FXCH
2016-06-17 21:53:04 -07:00
Alan Mishchenko
c912875261
New command 'phase_map'.
2016-06-17 20:21:39 -07:00
Alan Mishchenko
92a448e6ab
Experiments with edge-based mapping.
2016-06-17 19:57:30 -07:00
Bruno Schmitt
85428a60cc
Enables FXCH to handle Distance-1 cubes (D1C) and Single Cube Containment (SCC) as by product of extraction.
...
D1C: Whenever they appear a constant divisor (x! + x) will be created and handle as any other divisor.
SCC: Will be taken care of as soon as they appear.
2016-06-17 17:24:58 -03:00
Alan Mishchenko
3c3a770a17
New multi-output PLA reader and preprocessor (read_plamo) (added dist-1 merge).
2016-06-16 21:09:39 -07:00
Alan Mishchenko
e06c04a3ef
Change to BENCH reader to read DFF with four inputs.
2016-06-16 16:48:45 -07:00
Alan Mishchenko
0923d543ad
Adding a switch 'retime -o' to use old flop naming conventions.
2016-06-16 16:13:13 -07:00
Alan Mishchenko
ada21a655f
New multi-output PLA reader and preprocessor (read_plamo).
2016-06-16 15:22:03 -07:00
Alan Mishchenko
e1b51d1863
Experiments with edge-based mapping.
2016-06-15 18:47:10 -07:00
Alan Mishchenko
db43d6fbd8
Adding switch -P <num> to command 'cover'.
2016-06-14 20:43:50 -07:00
Alan Mishchenko
0a1b6f8fcc
Detecting properties of internal nodes.
2016-06-14 15:37:59 -07:00
Alan Mishchenko
a18da5c878
Detecting properties of internal nodes.
2016-06-12 19:07:46 -07:00
Alan Mishchenko
699dd39035
Support bit-blasting of shifts with more than 32 bits (fix).
2016-06-08 22:25:12 -05:00
Alan Mishchenko
cad3d8d419
Support bit-blasting of shifts with more than 32 bits.
2016-06-07 15:20:38 -07:00
Alan Mishchenko
820a48b2cb
Changes to Wlc to accommodate signed signals in SMT-LIB.
2016-06-07 15:05:21 -07:00
Alan Mishchenko
4efbd7b3ca
Detecting properties of internal nodes.
2016-06-07 14:32:38 -07:00
Alan Mishchenko
998aeff15e
Improvement to CNF encoding of cardinality constraints proposed by Mathias Soaken.
2016-06-07 00:22:32 -07:00
Alan Mishchenko
31b2e8bebd
Switch 'fx -x' to use only canonical divisors in 'fx'.
2016-06-06 19:31:56 -07:00
Alan Mishchenko
00242f2fb2
New profiling features for word-level optimizations.
2016-06-04 17:31:15 -07:00
Alan Mishchenko
93c785e802
Small changes for today's experiments.
2016-06-03 13:22:24 -07:00
Alan Mishchenko
e33d6e8d9d
Small changes to compile on Windows.
2016-06-03 10:12:00 -07:00
Bruno Schmitt
fe6a647f37
Merged alanmi/abc into default
2016-06-02 20:30:04 -03:00
Bruno Schmitt
b6ab087952
Removing the memory saving mode, it is no longer necessary.
2016-06-02 17:26:12 -03:00
Bruno Schmitt
4937fb09ed
Minimizing memory usage. The implementation was using twice as much memory as necessary.
2016-06-02 17:23:35 -03:00
Alan Mishchenko
e1b32ee756
Silencing several messages.
2016-06-01 11:57:29 -07:00
Alan Mishchenko
1d26d58a17
Adding switch 'pdr -o' to control using property output in induction.
2016-05-25 13:47:38 -07:00
Alan Mishchenko
58c81ec097
Improving SMT-LIB parser.
2016-05-23 11:15:37 -07:00
Alan Mishchenko
c688d1b158
Improving SMT-LIB parser.
2016-05-23 10:42:53 -07:00
Alan Mishchenko
0f29f0aec9
Improving SMT-LIB parser.
2016-05-21 20:08:05 -07:00
Alan Mishchenko
34c5ac88d4
Improving SMT-LIB parser.
2016-05-20 20:38:43 -07:00
Alan Mishchenko
7b570b6241
Enabling AIGs without structural hashing (&get -c to import logic network).
2016-05-20 18:01:01 -07:00
Alan Mishchenko
ce126db5f5
Enabling AIGs without structural hashing.
2016-05-20 16:37:58 -07:00
Alan Mishchenko
3b62ee4575
Enabling AIGs without structural hashing.
2016-05-20 16:23:48 -07:00
Alan Mishchenko
27c44fd644
Switch &miter -y to convert a two-word miter into a dual-output miter.
2016-05-20 14:03:07 -07:00
Alan Mishchenko
555ed0b158
Enabling AIGs without structural hashing.
2016-05-20 13:50:19 -07:00
Alan Mishchenko
c6a290ee97
Merged in boschmitt/abc (pull request #26 )
...
Fix the problem of not identifying divisors when its originating cubes had only 2 literals.
2016-05-19 23:34:20 -07:00
Alan Mishchenko
2ded89cca5
Added switch 'bmc3 -r' to disable periodic restarts in the SAT solver.
2016-05-19 22:33:40 -07:00
Alan Mishchenko
2d0a8fb4cb
Improving SMT-LIB parser.
2016-05-19 22:07:52 -07:00
Bruno Schmitt
fe6bb87e54
Merged alanmi/abc into default
2016-05-19 22:11:14 -03:00
Bruno Schmitt
f93fbc2303
Fix the problem of not identifying divisors when its originating cubes had only 2 literals.
...
With this change, 'empty' sub-cubes (sub-cubes with an ID equal to zero) are inserted in the 0th bin of the hash table.
2016-05-19 22:10:30 -03:00
Alan Mishchenko
07d074fd88
New feature for area minimization in standard cell mapping.
2016-05-19 15:22:25 -07:00
Baruch Sterin
031015e7f8
fix end of line problem that prevents the cmake build system from working
2016-05-17 15:21:03 -07:00
Alan Mishchenko
d7912acfca
Bug fix in &demiter.
2016-05-16 17:34:25 -07:00
Alan Mishchenko
7c089a3ac6
Factoring out library preprocessing code in &nf and putting it elsewhere.
2016-05-16 16:50:01 -07:00
Alan Mishchenko
20a2b0a0f2
Added switch 'read_genlib -n' to anonymize Genlib library.
2016-05-16 15:44:54 -07:00
Alan Mishchenko
fa111ff81b
Experiments with generating sat assignments.
2016-05-15 16:43:10 -07:00
Alan Mishchenko
8a56721494
Experiments with generating sat assignments.
2016-05-15 16:18:23 -07:00
Alan Mishchenko
be769ca3e8
Experiments with generating sat assignments.
2016-05-15 14:25:55 -07:00
Alan Mishchenko
0533fc7de9
Experiments with generating sat assignments.
2016-05-15 14:24:38 -07:00
Alan Mishchenko
12688ac9ee
Experiments with generating sat assignments.
2016-05-14 23:14:20 -07:00
Alan Mishchenko
4ffbd0b2df
Adding switch -r to &dch to prevent combo-loops.
2016-05-13 13:40:08 -07:00
Alan Mishchenko
5b6e5b8178
New command 'expand' to expand SOPs against the offset.
2016-05-12 22:41:20 -07:00
Alan Mishchenko
ea7d10d45d
Adding 'read_pla -d' to read dc-set along with on-set (useful to derive offset).
2016-05-12 13:59:30 -07:00
Alan Mishchenko
9e4d24aa5d
Cosmetic changes after incorporating new code of 'fxch'.
2016-05-11 20:04:58 -07:00
Alan Mishchenko
c5befad518
Cosmetic changes after incorporating new code of 'fxch'.
2016-05-11 20:03:13 -07:00
Alan Mishchenko
c30819cb05
Cosmetic changes after incorporating new code of 'fxch'.
2016-05-11 19:59:56 -07:00
Bruno Schmitt
3cf495c831
Add a new module which implements the fast extract with cube hashing (fxch) algorithm.
...
Removes old partial implementation of this algorithm from the "pla" module.
2016-05-11 19:41:31 -03:00
Alan Mishchenko
6e8efec57d
Experiments with CEC for arithmetic circuits.
2016-05-11 11:07:34 -07:00
Alan Mishchenko
c89f987dc7
Invalidate packing after mapping is updated.
2016-05-09 11:25:26 -07:00
Alan Mishchenko
652b279234
Experiments with CEC for arithmetic circuits.
2016-05-08 19:01:46 -07:00
Alan Mishchenko
4771b598c0
Experiments with CEC for arithmetic circuits.
2016-05-07 19:50:09 -07:00
Alan Mishchenko
236d412255
Experiments with CEC for arithmetic circuits.
2016-05-07 19:47:02 -07:00
Alan Mishchenko
40d90ae69c
Small changes.
2016-05-04 13:46:07 -07:00
Alan Mishchenko
21896ba6bc
Update to &show to show AIGs with XORs and MUXes (derived by &st -m).
2016-05-04 07:22:13 -07:00
Alan Mishchenko
28cbb280b7
Update to &show to show AIGs with XORs and MUXes (derived by &st -m).
2016-05-04 07:05:43 -07:00
Alan Mishchenko
11f1a249ae
Updating GIG parser.
2016-05-01 17:43:50 -07:00
Alan Mishchenko
a093091004
Fanout restriction in &edge.
2016-04-30 17:47:23 -07:00
Alan Mishchenko
e3e6236663
This code was accidentally deleted from the SAT solver (effectively disabling restarts!)
2016-04-30 10:42:10 -07:00
Alan Mishchenko
2de8f04c0d
Suggested bug fix in st__strhash().
2016-04-30 10:40:54 -07:00
Alan Mishchenko
59f3389c9b
Experiments with arithmetic circuits.
2016-04-28 20:54:38 -07:00
Alan Mishchenko
53e8647719
Adding option to rehash AIG after mapping.
2016-04-27 18:33:23 -07:00
Alan Mishchenko
e8f961671c
Extending &satlut to work for 6-LUTs.
2016-04-27 18:12:41 -07:00
Alan Mishchenko
62f13100d0
Adding missing code to 'dress'.
2016-04-27 17:33:36 -07:00
Alan Mishchenko
53ca51f61a
Using seed assignment of edges in &edge.
2016-04-27 16:27:48 -07:00
Alan Mishchenko
6f370462d1
Bug fix in bit-blasting of remainder.
2016-04-26 20:24:46 -07:00
Alan Mishchenko
b87554b98a
Improved algo for edge computation.
2016-04-24 22:06:03 +03:00
Alan Mishchenko
e37ec2aac5
Improved algo for edge computation.
2016-04-24 20:49:05 +03:00
Alan Mishchenko
f91f23bed0
Adding new switch 'bdd -s' to translate SOP directly into BDD.
2016-04-24 00:13:07 +03:00
Alan Mishchenko
67bfb4ba09
Improved algo for edge computation.
2016-04-23 15:13:22 +03:00
Alan Mishchenko
1b550cb87b
Improved algo for edge computation.
2016-04-22 08:36:05 +03:00
Alan Mishchenko
813b0e5851
Experimental algorithm for edge optimization.
2016-04-13 15:54:14 -07:00
Alan Mishchenko
b9e403b46e
Bug fix: change in the ordering of the reset flop (should be last, not first).
2016-04-13 09:14:54 -07:00
Alan Mishchenko
89d4ac5029
Adding new implementation of LEXSAT.
2016-04-12 19:44:21 -07:00
Alan Mishchenko
8de7383edd
Restructing sat_solver_solve() method for pushing/popping assumptions.
2016-04-12 19:43:15 -07:00
Alan Mishchenko
b4bb88ae5d
Removing unused feature of the SAT solver (user-guided variable ordering).
2016-04-12 12:04:03 -07:00
Alan Mishchenko
3a553e15ac
Removing unused feature of the SAT solver (native support for cardinality constraint).
2016-04-12 11:58:55 -07:00
Alan Mishchenko
847ac96f6e
Updates to Exorcism package
2016-04-11 22:55:06 -07:00
Alan Mishchenko
9522aeea19
Updates to Exorcism package
2016-04-11 22:29:37 -07:00
Alan Mishchenko
a02be725e9
Updates to Exorcism package
2016-04-11 21:48:54 -07:00
Alan Mishchenko
2d6a6f6654
Added Exorcism package, reading ESOP (read_pla -x file.esop) and deriving AIG (cubes -x; st).
2016-04-11 21:42:00 -07:00
Alan Mishchenko
2d1d315ece
Supporting edge information during mapping.
2016-04-11 18:41:18 -07:00
Alan Mishchenko
d0a0cf6395
Command &esop to convert AIG into ESOP.
2016-04-09 17:00:46 -07:00
Alan Mishchenko
8b07237bf5
Adding hashing of windows in &satlut.
2016-04-07 20:52:49 -07:00
Alan Mishchenko
3b694a7089
Adding AIG rehashing after LUT mapping in Gia.
2016-04-07 20:03:31 -07:00
Alan Mishchenko
26ec3868f6
Adding AIG rehashing after LUT mapping in Gia.
2016-04-07 19:16:51 -07:00
Alan Mishchenko
887f3c21cc
Supporting edges in delay-optimization in &satlut.
2016-04-07 17:15:24 -07:00
Alan Mishchenko
f05986f7b3
Supporting edges in delay-optimization in &satlut.
2016-04-07 15:54:50 -07:00
Alan Mishchenko
95ab749087
Supporting edges in delay-optimization in &satlut.
2016-04-07 13:20:41 -07:00
Alan Mishchenko
b31b6fec77
Supporting edge information during mapping.
2016-04-06 15:43:03 -07:00
Alan Mishchenko
ee17cbbf4b
Supporting negative and reverse ranges of word-level variables in Wlc.
2016-04-04 18:09:41 -07:00
Alan Mishchenko
ac7a799076
Improvements to delay-optimization in &satlut.
2016-04-04 14:27:14 -07:00
Alan Mishchenko
720082753f
Improvements to delay-optimization in &satlut.
2016-04-04 12:51:05 -07:00
Alan Mishchenko
4a954c1b23
Improvements to delay-optimization in &satlut.
2016-04-04 08:43:22 -07:00
Alan Mishchenko
e0ad9de7ea
Improvements to delay-optimization in &satlut.
2016-04-03 16:44:13 -07:00
Alan Mishchenko
d53161a7e1
Enabling native Gia visualization in &show.
2016-04-03 15:42:08 -07:00
Alan Mishchenko
9074d19d69
Allowing Cba manager to be derived from another Cba manager.
2016-04-02 16:04:15 -07:00
Alan Mishchenko
7724dfcca2
Windowing for technology mapping.
2016-03-30 21:51:50 -07:00
Alan Mishchenko
31430043c2
Windowing for technology mapping.
2016-03-29 20:16:30 -07:00
Alan Mishchenko
e026f05ae3
Bug fix in truth table reading for funcs with less than 6 vars.
2016-03-28 10:18:17 -07:00
Alan Mishchenko
81b70c4d20
Corner-case bug fix in 'satclp' with conflict limit.
2016-03-25 13:51:05 -07:00
Alan Mishchenko
72ffddb0ad
Sorting multiplier inputs based on the number of constant bits.
2016-03-24 17:45:51 -07:00
Alan Mishchenko
ecb2780a72
Procedure to check inductive invariant for Gia package.
2016-03-21 15:47:29 -07:00
Alan Mishchenko
a4d6e2f8c9
Typo in operator in Wlc_Ntk_t.
2016-03-18 20:47:21 -07:00
Alan Mishchenko
65ee47c515
Supporting bit-wise XNOR operator in Wlc_Ntk_t.
2016-03-18 13:58:22 +08:00
Alan Mishchenko
b2ad140adb
Supporting complemented reduction operators.
2016-03-11 15:12:52 +09:00
Alan Mishchenko
22a5ab19c8
Adding API to convert Genlib into a simple Liberty.
2016-03-11 00:15:13 +09:00
Alan Mishchenko
74328f52da
Supporting complemented reduction operators.
2016-03-10 23:03:53 +09:00
Alan Mishchenko
847d661bee
Change error to warning in 'scorr'.
2016-03-09 09:33:10 +09:00
Alan Mishchenko
73cbe319ff
Bug fix in &fftest: not outputting test patterns when user test patterns are given.
2016-03-09 09:28:31 +09:00
Alan Mishchenko
12fac91fba
Supporting ~^ as equality operator in Wlc.
2016-03-04 09:17:39 +09:00
Alan Mishchenko
cf702af6f1
New hierarchical TT NPN matching.
2016-02-26 18:20:57 +08:00