Alan Mishchenko
|
dd29ca30a6
|
New technology mapper.
|
2013-07-14 23:12:05 -07:00 |
Alan Mishchenko
|
c0ac159888
|
New technology mapper.
|
2013-07-14 15:04:25 -07:00 |
Alan Mishchenko
|
b3e0f5b2e9
|
New technology mapper.
|
2013-07-13 23:40:51 -07:00 |
Alan Mishchenko
|
118e40b809
|
New technology mapper.
|
2013-07-13 12:20:53 -07:00 |
Alan Mishchenko
|
4a50b09c67
|
New technology mapper.
|
2013-07-13 11:12:36 -07:00 |
Alan Mishchenko
|
7efe9f2afd
|
New technology mapper.
|
2013-07-12 19:33:46 -07:00 |
Alan Mishchenko
|
b0bd2025c6
|
Compiler warnings.
|
2013-07-12 13:16:12 -07:00 |
Alan Mishchenko
|
804e0261ab
|
Compiler warnings.
|
2013-07-12 13:14:44 -07:00 |
Alan Mishchenko
|
fba33fbba4
|
New technology mapper.
|
2013-07-12 13:02:32 -07:00 |
Alan Mishchenko
|
589e2edec2
|
Compiler problem.
|
2013-07-01 23:05:57 -07:00 |
Alan Mishchenko
|
e7504c6dab
|
Compiler problem.
|
2013-07-01 23:03:23 -07:00 |
Alan Mishchenko
|
32e58b8883
|
Fixing a typo.
|
2013-07-01 22:57:28 -07:00 |
Alan Mishchenko
|
60bb6dbf69
|
Adding commands 'bm2' and 'saucy3' developed by Hadi Katebi, Igor Markov, and Karem Sakallah at U Michigan.
|
2013-07-01 18:06:09 -07:00 |
Alan Mishchenko
|
4e247281d2
|
Updating new mapper.
|
2013-06-29 23:45:04 -07:00 |
Alan Mishchenko
|
8c7ca72ea9
|
Adding timeout to command 'ind'.
|
2013-06-28 12:21:48 -07:00 |
Alan Mishchenko
|
e93cfb18ee
|
Data-structure experiment.
|
2013-06-27 13:54:44 -07:00 |
Alan Mishchenko
|
a66dc0afb6
|
Unifying representation of mapping in GIA.
|
2013-06-25 23:05:51 -07:00 |
Alan Mishchenko
|
0985491dce
|
Improving integration of the 'if' mapper with GIA.
|
2013-06-25 19:46:07 -07:00 |
Alan Mishchenko
|
ed319531be
|
Improving integration of the 'if' mapper with GIA.
|
2013-06-25 17:19:44 -07:00 |
Alan Mishchenko
|
94b26fe5a2
|
Improving CEC (command 'dcec') by integrating XOR balancing.
|
2013-06-25 11:49:25 -07:00 |
Alan Mishchenko
|
faa220401c
|
New random FSM generation command 'genfsm'.
|
2013-06-22 14:03:23 -07:00 |
Alan Mishchenko
|
7ea3cdffb4
|
Limiting runtime limit checks in 'pdr'.
|
2013-06-22 11:56:34 -07:00 |
Alan Mishchenko
|
9eaa290b1f
|
Limiting runtime limit checks in 'pdr'.
|
2013-06-22 11:54:58 -07:00 |
Alan Mishchenko
|
a7339fdb99
|
Fix constant propagation after 'if'.
|
2013-06-18 13:56:46 -07:00 |
Alan Mishchenko
|
ac4962eb2d
|
Compiler warnings.
|
2013-06-18 11:32:24 -07:00 |
Alan Mishchenko
|
90a88462c4
|
New MFS package.
|
2013-05-31 02:01:36 -07:00 |
Alan Mishchenko
|
ba309121d7
|
New MFS package.
|
2013-05-31 00:56:10 -07:00 |
Alan Mishchenko
|
3c97892514
|
New MFS package.
|
2013-05-30 14:09:50 -07:00 |
Alan Mishchenko
|
c50c1fc662
|
Multiplexer profiling.
|
2013-05-27 17:48:17 -07:00 |
Alan Mishchenko
|
37077748a1
|
Moving one declaration to the header file.
|
2013-05-27 15:21:11 -07:00 |
Alan Mishchenko
|
19c25fd6aa
|
Adding a wrapper around clock() for more accurate time counting in ABC.
|
2013-05-27 15:09:23 -07:00 |
Alan Mishchenko
|
94356f0d1f
|
Several small changes to the MFS packages.
|
2013-05-27 14:39:08 -07:00 |
Alan Mishchenko
|
755935a6df
|
Added switch -M to set max size of two-cube divisors to extract (often helps both runtime and quality).
|
2013-05-27 13:34:22 -07:00 |
Alan Mishchenko
|
0cad45fa90
|
New MFS package.
|
2013-05-27 09:49:13 -07:00 |
Alan Mishchenko
|
fb6eaaf5d9
|
New MFS package.
|
2013-05-26 16:12:44 -07:00 |
Alan Mishchenko
|
ed3d3dfc8e
|
New MFS package.
|
2013-05-26 13:34:24 -07:00 |
Alan Mishchenko
|
8e639c3d79
|
New command 'putontop' to concatenate networks for don't-care-based optimization.
|
2013-05-25 22:13:46 -07:00 |
Alan Mishchenko
|
94a75fe6d8
|
New MFS package.
|
2013-05-25 18:10:45 -07:00 |
Alan Mishchenko
|
f47cc6cefc
|
New MFS package.
|
2013-05-25 11:14:12 -07:00 |
Alan Mishchenko
|
9268c10023
|
New MFS package.
|
2013-05-25 00:45:22 -07:00 |
Alan Mishchenko
|
d5234332fb
|
New MFS package.
|
2013-05-24 22:35:22 -07:00 |
Alan Mishchenko
|
283abd4795
|
New MFS package.
|
2013-05-24 19:54:28 -07:00 |
Alan Mishchenko
|
28e065b0ae
|
Counter-example depth minimization.
|
2013-05-22 11:02:56 -07:00 |
Alan Mishchenko
|
b7d670ecf2
|
Bug fix in saving CEXes and CEX vectors.
|
2013-05-21 17:28:15 -07:00 |
Alan Mishchenko
|
67357cda2f
|
Added new switched to command &frames.
|
2013-05-19 10:58:36 -07:00 |
Alan Mishchenko
|
354333f98a
|
Changing command 'history' to have simpler interface.
|
2013-05-18 23:24:29 -07:00 |
Alan Mishchenko
|
e86e4b6698
|
Added switch -I <file_name> to &sim to perform simulation with the user's simulation pattern.
|
2013-05-18 23:19:51 -07:00 |
Alan Mishchenko
|
68e1a07fdb
|
Improvements to 'bmc3'.
|
2013-05-18 17:31:23 -07:00 |
Alan Mishchenko
|
7bc2fb5199
|
SAT variable profiling.
|
2013-05-18 11:20:07 -07:00 |
Alan Mishchenko
|
f9da2c790f
|
SAT variable profiling.
|
2013-05-18 11:03:32 -07:00 |
Alan Mishchenko
|
e04ded5640
|
Undoing commit from Nov 12, 2012: Extending GIA to represent pintypes and pins.
|
2013-05-17 12:05:28 -07:00 |
Alan Mishchenko
|
760c1f60d2
|
Adding new command &mprove for proving groups of properties.
|
2013-05-17 11:50:16 -07:00 |
Alan Mishchenko
|
7be3e3e6b4
|
Adding 'zeropo -o' to replace a given PO by const 1.
|
2013-05-15 00:17:06 -07:00 |
Alan Mishchenko
|
533ff6984e
|
Commenting assertion that does not hold in AIGER 1.9, accoring to Baruch Sterin.
|
2013-05-13 23:25:34 -07:00 |
Alan Mishchenko
|
3880623c9b
|
Extending cube representation to handle SOPs with many cubes.
|
2013-05-12 23:23:18 -07:00 |
Alan Mishchenko
|
9d219eee4b
|
New MFS package.
|
2013-05-12 19:09:28 -07:00 |
Alan Mishchenko
|
6610f1c78e
|
Preprocessing SOPs given to 'fx' to be D1C-free and SCC-free. Handling the case of non-prime SOPs.
|
2013-05-11 17:16:09 -07:00 |
Alan Mishchenko
|
f2abd6b8a9
|
Preprocessing SOPs given to 'fx' to be D1C-free and SCC-free. Handling the case of non-prime SOPs.
|
2013-05-11 17:01:13 -07:00 |
Alan Mishchenko
|
cac32a32c7
|
Enabled switch 'fx -N <num>' to extract a fixed number of divisors.
|
2013-05-09 12:51:18 -07:00 |
Alan Mishchenko
|
22806448c1
|
Adding comment about using 'dprove' for sequential synthesis.
|
2013-05-09 12:01:29 -07:00 |
Alan Mishchenko
|
7c7d527755
|
Changing per-output runtime limit to be in miliseconds.
|
2013-05-09 11:35:04 -07:00 |
Alan Mishchenko
|
027dbbd492
|
Making fanin ordering available for netlists, not only networks.
|
2013-05-07 18:57:40 -07:00 |
Alan Mishchenko
|
a735d95a5b
|
SAT sweeping under constraints (bug fix).
|
2013-05-07 18:11:29 -07:00 |
Alan Mishchenko
|
51db560206
|
Procedures for sorting fanins of the nodes.
|
2013-05-06 18:51:48 -07:00 |
Alan Mishchenko
|
f02888635f
|
Procedures for sorting fanins of the nodes.
|
2013-05-06 18:19:20 -07:00 |
Alan Mishchenko
|
05f7cd9ed2
|
Integration of the liveness property prover developed by Sayak Ray.
|
2013-05-05 21:08:55 -07:00 |
Alan Mishchenko
|
98cf5698a1
|
New fast extract.
|
2013-05-05 18:57:51 -07:00 |
Alan Mishchenko
|
7a78e30390
|
New fast extract.
|
2013-05-05 14:33:28 -07:00 |
Alan Mishchenko
|
eacfad7622
|
Changing the queue to work in the same the array of costs is realloced.
|
2013-05-05 09:04:14 -07:00 |
Alan Mishchenko
|
7d3301584a
|
New fast extract.
|
2013-05-05 01:56:16 -07:00 |
Alan Mishchenko
|
a762c695d7
|
New fast extract.
|
2013-05-05 01:54:11 -07:00 |
Alan Mishchenko
|
4aff2d134d
|
C++ compiler errors.
|
2013-05-04 20:28:05 -07:00 |
Alan Mishchenko
|
13ee4998c3
|
C++ compiler errors.
|
2013-05-04 20:24:53 -07:00 |
Alan Mishchenko
|
36d5ef4e62
|
Making changes suggested by Mark Jarvin.
|
2013-05-04 11:10:25 -07:00 |
Alan Mishchenko
|
95571be503
|
Changes to the ABC data-structures to allow for larger designs.
|
2013-05-04 10:48:46 -07:00 |
Alan Mishchenko
|
50df0813fb
|
Allowing 'constr' to reset remove currently defined constraints.
|
2013-05-03 19:59:18 -07:00 |
Alan Mishchenko
|
50095be5ac
|
Adding runtime limit per output to multi-output DPR (pdr -H <num_sec>).
|
2013-05-03 19:58:25 -07:00 |
Alan Mishchenko
|
a59968ce8c
|
Adding runtime limit per output to multi-output BMC (bmc3 -H <num_sec>).
|
2013-05-03 18:26:18 -07:00 |
Alan Mishchenko
|
6a49d1f4c6
|
Reading/writing MiniAIG and several minor changes.
|
2013-05-03 15:45:50 -07:00 |
Alan Mishchenko
|
bc50421928
|
Minor changes and improvement in PO partitioning (command &popart).
|
2013-05-01 12:45:34 -07:00 |
Alan Mishchenko
|
1f573cfe58
|
Compiler warnings.
|
2013-05-01 00:13:29 -07:00 |
Alan Mishchenko
|
b94766bce5
|
Faster isomorphism detection (command &iso).
|
2013-05-01 00:10:53 -07:00 |
Alan Mishchenko
|
c53eb0b9e1
|
Changing the print-out of &iso.
|
2013-04-30 10:46:07 -07:00 |
Alan Mishchenko
|
3b1ebbaa28
|
SAT sweeping under constraints.
|
2013-04-28 19:17:59 -07:00 |
Alan Mishchenko
|
9e1765216b
|
Added option 'int -I <filename>' to specify file names to dump invariants.
|
2013-04-28 16:55:25 -07:00 |
Alan Mishchenko
|
266667d8b2
|
Improving local BDD construction from local SOPs and local AIGs.
|
2013-04-28 16:33:42 -07:00 |
Alan Mishchenko
|
58e1041ad8
|
Modified command 'eliminate' to perform traditional 'eliminate -1'.
|
2013-04-28 16:21:58 -07:00 |
Alan Mishchenko
|
a33821ab38
|
Added alias for 'eliminate'.
|
2013-04-28 15:41:29 -07:00 |
Alan Mishchenko
|
48d867f77d
|
Modified command 'eliminate' to perform traditional 'eliminate -1'.
|
2013-04-28 15:02:03 -07:00 |
Alan Mishchenko
|
8db0b9c0c6
|
Improving local BDD construction from local SOPs and local AIGs.
|
2013-04-28 12:34:03 -07:00 |
Alan Mishchenko
|
b09926e8e2
|
SAT sweeping under constraints.
|
2013-04-28 01:25:29 -07:00 |
Alan Mishchenko
|
17a0d944b3
|
SAT sweeping under constraints.
|
2013-04-27 22:38:01 -07:00 |
Alan Mishchenko
|
324d73c29a
|
New fast extract.
|
2013-04-27 15:23:12 -07:00 |
Alan Mishchenko
|
486eacc542
|
SAT sweeping under constraints.
|
2013-04-25 15:32:30 -07:00 |
Alan Mishchenko
|
e0462d8d2e
|
Adding print-out of SOP literals with 'ps -f'.
|
2013-04-19 09:35:30 -07:00 |
Alan Mishchenko
|
df198d2cef
|
Enabled 'cec' to be applied to networks derived from BLIF with EXDCs.
|
2013-04-18 18:32:58 -07:00 |
Alan Mishchenko
|
c80fce00fe
|
Enabled reading the EXDC network by the default BLIF reader.
|
2013-04-18 17:39:13 -07:00 |
Alan Mishchenko
|
96b784ecd7
|
Fixing both AIGER readers (read_aiger and &r) to work with AIGER 1.9 (except for liveness properties).
|
2013-04-18 00:05:11 -07:00 |
Alan Mishchenko
|
61ecc9c633
|
Fixing both AIGER readers (read_aiger and &r) to work with AIGER 1.9 (except for liveness properties).
|
2013-04-17 23:48:58 -07:00 |
Alan Mishchenko
|
06ba3d3e6c
|
Adding command &filter_equiv to filter candidate equivalence classes using indexes of disproved POs after handling SRM as a multi-output miter.
|
2013-04-17 22:18:43 -07:00 |
Alan Mishchenko
|
7808ee8e70
|
Adding parameter structure for rarity simulation.
|
2013-04-17 19:40:02 -07:00 |
Alan Mishchenko
|
9b6efa34ad
|
Bug fix in 'write_pla'.
|
2013-04-15 22:59:54 -07:00 |
Alan Mishchenko
|
45d82477b7
|
Saving network name in 'blockpo'.
|
2013-04-12 00:10:21 -07:00 |
Alan Mishchenko
|
4876f1e21c
|
Added switch '-x' to save CEXes in 'bmc3' and 'pdr' in multi-output mode.
|
2013-04-09 16:26:28 -07:00 |
Alan Mishchenko
|
b902b00779
|
Small changes to LMS code.
|
2013-04-01 21:41:53 -07:00 |
Alan Mishchenko
|
f99e5cd9d6
|
Shrink for 6-LUTs.
|
2013-04-01 20:21:34 -07:00 |
Alan Mishchenko
|
28f12c5f06
|
Shrink for 6-LUTs.
|
2013-04-01 19:25:21 -07:00 |
Alan Mishchenko
|
5ec77b66e1
|
Updating 'sim3' to move the design into the last rare state.
|
2013-04-01 18:41:56 -07:00 |
Alan Mishchenko
|
48fce79453
|
Updating 'sim3' to move the design into the last rare state.
|
2013-04-01 18:39:42 -07:00 |
Alan Mishchenko
|
2650f94598
|
Shrink for 6-LUTs.
|
2013-03-31 23:09:51 -07:00 |
Alan Mishchenko
|
ca7c801150
|
Improving verbose printout of 'sim3' when solving multiple outputs.
|
2013-03-30 15:15:26 -07:00 |
Alan Mishchenko
|
05ea180902
|
Compiler warnings.
|
2013-03-30 14:20:10 -07:00 |
Alan Mishchenko
|
1d4674e548
|
Compiler warnings.
|
2013-03-30 14:17:10 -07:00 |
Alan Mishchenko
|
270d36ac05
|
Improved 'trim' and added 'dropsat' to replace sat POs by constant 0.
|
2013-03-30 14:11:39 -07:00 |
Alan Mishchenko
|
5ace683835
|
Updating bmc3 printout to show the number of failed outputs.
|
2013-03-30 13:02:32 -07:00 |
Alan Mishchenko
|
cc7d3e3747
|
Added dumping QDIMACS files in command 'qbf'.
|
2013-03-28 22:21:05 -07:00 |
Alan Mishchenko
|
b7cd22786e
|
Changed to 'print_level' to be less verbose by default.
|
2013-03-28 20:09:08 -07:00 |
Alan Mishchenko
|
fdb8d83f7a
|
Adding command &miter2 to derive a specified sequential miter.
|
2013-03-28 12:30:27 -07:00 |
Alan Mishchenko
|
7a2132b237
|
Added dumping QDIMACS files in command 'qbf'.
|
2013-03-27 17:21:08 -07:00 |
Alan Mishchenko
|
272089221a
|
Removing hard-coded limit on the number of solving iterations in command 'qbf'.
|
2013-03-27 12:51:57 -07:00 |
Alan Mishchenko
|
e64cad10e2
|
Adding command &miter2 to derive a specified sequential miter.
|
2013-03-27 12:43:00 -07:00 |
Alan Mishchenko
|
17af45424f
|
Commenting out undesirable warnings/assertions.
|
2013-03-26 14:32:21 -07:00 |
Alan Mishchenko
|
bf795e57cf
|
Handling special case in 'fold' when the network is combinational.
|
2013-03-13 11:47:17 +01:00 |
Alan Mishchenko
|
1eb4059f05
|
PO partitioning algorithm.
|
2013-03-09 13:33:12 -08:00 |
Alan Mishchenko
|
eee8ceb0fa
|
PO partitioning algorithm.
|
2013-03-09 12:19:11 -08:00 |
Alan Mishchenko
|
a3bdba6875
|
Modified command 'init' to allow for specific init values.
|
2013-03-07 20:38:55 -08:00 |
Alan Mishchenko
|
1ce537e992
|
Misc changes.
|
2013-03-07 13:04:16 -08:00 |
Alan Mishchenko
|
1a6354c22f
|
Improvements to the hierarchy/timing manager.
|
2013-03-05 17:01:41 -08:00 |
Alan Mishchenko
|
dcc8907161
|
Improvements to the hierarchy/timing manager.
|
2013-03-05 16:53:18 -08:00 |
Alan Mishchenko
|
4ff5203f4c
|
Improvements to the hierarchy/timing manager.
|
2013-03-05 13:13:15 -08:00 |
Alan Mishchenko
|
0c9337f627
|
User-controlable SAT sweeper.
|
2013-03-04 00:33:36 -08:00 |
Alan Mishchenko
|
a27a7bc827
|
User-controlable SAT sweeper and other small changes.
|
2013-02-27 12:12:23 -05:00 |
Alan Mishchenko
|
69dd1337b0
|
Started PO partitioning command.
|
2013-02-24 09:27:25 -08:00 |
Alan Mishchenko
|
1c744cf10a
|
K-hot STG encoding.
|
2013-02-23 13:53:22 -08:00 |
Alan Mishchenko
|
91ca83e864
|
Adding new features to 'dualrail'.
|
2013-02-21 22:51:25 -08:00 |
Alan Mishchenko
|
dfe5f511b2
|
Adding new features to 'dualrail'.
|
2013-02-21 22:46:53 -08:00 |
Alan Mishchenko
|
dd52905fa3
|
Enabling two-timeframe property check in the interpolation procedure.
|
2013-02-21 12:10:35 -08:00 |
Alan Mishchenko
|
a82b0a8ad5
|
New command &cycle, which is faster than 'cycle'.
|
2013-02-19 23:51:13 -08:00 |
Alan Mishchenko
|
59fe3268a7
|
Adding STG generation (&era -d) and STG encoding (&read_stg <file>).
|
2013-02-19 23:07:29 -08:00 |
Alan Mishchenko
|
99a9718355
|
Integrating sweeping information.
|
2013-02-19 12:56:36 -08:00 |
Alan Mishchenko
|
baa944e6a2
|
Added 'gap timeout' to pdr.
|
2013-02-16 14:54:11 -08:00 |
Alan Mishchenko
|
fd0ff0171e
|
Added 'gap timeout' to bmc3 and sim3.
|
2013-02-15 16:47:18 -08:00 |
Alan Mishchenko
|
8866a1aa6d
|
Fixing performance problem in 'cone -s'
|
2013-02-13 19:42:11 -08:00 |
Alan Mishchenko
|
930369f36f
|
Integration of timing manager.
|
2013-02-03 18:02:22 +08:00 |
Alan Mishchenko
|
30ec58fcda
|
Added switch 'zeropo -s' to skip comb sweep after removing a PO.
|
2013-02-01 03:57:17 +07:00 |
Alan Mishchenko
|
7e598cd231
|
Fixing compilation problems on Linux-32 related to constants of type unsigned long long.
|
2013-01-30 16:15:53 +07:00 |
Alan Mishchenko
|
557448400e
|
Added new Python API is_const_po( int iPoNum ), which returns 0/1 if current network is an AIG and the given PO has const 0/1 function.
|
2013-01-25 10:25:34 +07:00 |
Alan Mishchenko
|
853222ee7b
|
Fixed a corner-case when 'sim3 -a' does not work for costant POs.
|
2013-01-25 06:49:49 +07:00 |
Alan Mishchenko
|
edd4b2a29c
|
Added switch &trim -V <num> to remove const POs with specific value <num>.
|
2013-01-25 06:19:51 +07:00 |
Alan Mishchenko
|
aa9c87cf8d
|
Extending verification status file format to allow for SAT status without CEX.
|
2013-01-25 05:59:56 +07:00 |