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
Alan Mishchenko
5a47990043
Disabling formula cleaner to avoid problems with reading GENLIB on some libraries.
2016-02-21 18:15:05 -08:00
Alan Mishchenko
460a13a102
Re-doing the same change.
2016-02-15 00:27:27 -08:00
Alan Mishchenko
e663db6638
Temporarily undoing one of the recent changes.
2016-02-15 00:26:59 -08:00
Alan Mishchenko
c8962e94e2
Improving bit-blasting of a multiplier and squarer.
2016-02-13 18:51:42 -08:00
Alan Mishchenko
390a145f0a
Adding support for a different bit-blasting of a multiplier and squarer.
2016-02-13 15:15:01 -08:00
Alan Mishchenko
e0616441b3
Adding support for a different bit-blasting of a multiplier and squarer.
2016-02-12 09:46:49 -08:00
Alan Mishchenko
66796c3808
Experiments with SAT-based mapping.
2016-02-08 16:29:36 -08:00
Alan Mishchenko
67f4f1adae
Experiments with SAT-based mapping.
2016-02-07 21:13:33 -08:00
Alan Mishchenko
59aea7639f
Bug fix in liberty parser and change suggested by Clifford.
2016-02-07 12:54:13 -08:00
Alan Mishchenko
0224039132
Added recursive bit-blasting of a carry-lookahead adder.
2016-02-06 12:08:23 -08:00
Alan Mishchenko
355865e81b
GENLIB parsing bug, which led to a crash.
2016-02-06 12:07:42 -08:00
Alan Mishchenko
76670892c2
Fixing the problem of identically named signals in 'retime'.
2016-02-05 16:21:37 -08:00
Alan Mishchenko
fc1897fb18
Making flop names after 'retime' more meaningful.
2016-02-03 13:56:47 -08:00
Alan Mishchenko
be35a13a4c
Preserving internal signal names when 'strash' is not used.
2016-02-03 13:56:27 -08:00
Alan Mishchenko
8bcf8fd3c9
Supporting X-valued constants in Wlc_Ntk_t.
2016-02-02 16:40:29 -08:00
Alan Mishchenko
094c68f921
Supporting X-valued constants in Wlc_Ntk_t.
2016-02-02 16:20:19 -08:00
Alan Mishchenko
c81b6cb515
Supporting X-valued constants in Wlc_Ntk_t.
2016-02-02 15:43:19 -08:00
Alan Mishchenko
02725c9eca
An add-on to write Verilog for circuits mapped into simple gates.
2016-02-01 15:56:53 -08:00
Alan Mishchenko
81dade194e
Rare bug fix in 'dch' resulting in choice nodes having internal fanout.
2016-01-31 16:38:49 -08:00
Alan Mishchenko
367b20f04d
Fixing mismatch in the TLS flow induced by adding cell configs in the DSD manager.
2016-01-30 20:59:57 -08:00
Alan Mishchenko
951ca48b9c
Small changes to sort for timing.
2016-01-24 15:32:12 -08:00
Alan Mishchenko
9ef447658e
Bug fix in 'aig', for the case of non-min-base SOPs.
2016-01-20 15:01:53 -08:00
Alan Mishchenko
df34a26216
Generating sorting network as a PLA file.
2016-01-20 15:01:27 -08:00
Alan Mishchenko
f5ee46eb3c
New command to dump LUT network.
2016-01-16 17:35:46 -08:00
Alan Mishchenko
334f4a29ca
Compiler warning.
2016-01-14 20:44:45 -08:00
Alan Mishchenko
c4446189a9
Changes to PDR to compute f-inf clauses and import invariant (or clauses) as a network.
2016-01-14 20:42:22 -08:00
Alan Mishchenko
f30facfec8
Experiments with SAT-based mapping.
2016-01-14 14:03:53 -08:00
Alan Mishchenko
4ecf43f1f0
Adding a way to derive cardinality constraint as a sorting network.
2016-01-13 20:32:26 -08:00
Alan Mishchenko
87f6828d50
Adding support for delay/area tradeoff.
2016-01-13 12:13:54 -08:00
Alan Mishchenko
8dd31fb4a9
Integrating new CNF generation into &bmc.
2016-01-12 22:07:01 -08:00
Alan Mishchenko
de695c9d4c
Better print-out of SOPs. Changing default of 'fx'. Updating 'satclp' to fine prine SOPs.
2016-01-12 11:55:50 -08:00