Alan Mishchenko
|
cb845d4488
|
Changing default values.
|
2013-09-30 13:39:14 -07:00 |
Alan Mishchenko
|
846da1d2c7
|
Changing default values.
|
2013-09-30 13:33:39 -07:00 |
Alan Mishchenko
|
726e70392c
|
Changing default values.
|
2013-09-30 01:00:25 -07:00 |
Alan Mishchenko
|
62439be84d
|
New logic sharing extraction.
|
2013-09-29 23:14:00 -07:00 |
Alan Mishchenko
|
2a83a97164
|
Changing default values.
|
2013-09-28 23:56:08 -07:00 |
Alan Mishchenko
|
797cb49584
|
Changing default values.
|
2013-09-28 23:14:43 -07:00 |
Alan Mishchenko
|
68011de615
|
Improving printouts in sharing extraction.
|
2013-09-28 22:42:01 -07:00 |
Alan Mishchenko
|
5f97f5cffa
|
New logic sharing extraction.
|
2013-09-28 20:19:53 -07:00 |
Alan Mishchenko
|
61ee156b72
|
New logic sharing extraction.
|
2013-09-28 18:35:38 -07:00 |
Alan Mishchenko
|
a7fcdf20ab
|
Performance balancing command &b.
|
2013-09-27 18:50:23 -07:00 |
Alan Mishchenko
|
4a74b7ced9
|
Generation of plain AIG after mapping.
|
2013-09-27 14:45:55 -07:00 |
Alan Mishchenko
|
940cf7f98b
|
Generation of plain AIG after mapping.
|
2013-09-27 13:30:36 -07:00 |
Alan Mishchenko
|
debbf4d807
|
Bug fix.
|
2013-09-27 10:09:57 -07:00 |
Alan Mishchenko
|
531657105b
|
Improving DAG-aware unmapping.
|
2013-09-25 15:29:01 -07:00 |
Alan Mishchenko
|
ee11ee1833
|
Changes to enable decomposition of non-DSD functions.
|
2013-09-25 13:18:21 -07:00 |
Alan Mishchenko
|
cab8301065
|
Changing switch -R <num> in &gla to mean the max allowed size of abstraction. Adding switch -Q <num> to stop when the number of objects exceeds num % _during_refinement_.
|
2013-09-23 10:57:15 -07:00 |
Alan Mishchenko
|
eec94a70f1
|
Adding API to return the mapped network.
|
2013-09-22 23:18:40 -07:00 |
Alan Mishchenko
|
d61bedc627
|
Adding API to return the mapped network.
|
2013-09-22 16:23:57 -07:00 |
Alan Mishchenko
|
cfebcae125
|
Adding resource limit to stop &gla when the number of remaining objects is less than R/2 during refinement.
|
2013-09-21 17:55:59 -04:00 |
Alan Mishchenko
|
d4bd7846c3
|
Added bridge integration for multi-output 'bmc3 -a'.
|
2013-09-17 23:19:54 -07:00 |
Alan Mishchenko
|
efa6b54b5e
|
Debugging and finetuning the flow.
|
2013-09-17 21:47:39 -07:00 |
Alan Mishchenko
|
73a997a8bd
|
Adding commands to set and print timing constraints.
|
2013-09-17 14:47:34 -07:00 |
Alan Mishchenko
|
7d3976a763
|
Unifying standard cell library representations.
|
2013-09-17 13:16:20 -07:00 |
Alan Mishchenko
|
105648bf7c
|
Adding switch to enable reuse of proof-obligations in the last timeframe.
|
2013-09-16 22:57:50 -07:00 |
Alan Mishchenko
|
2ba12a76ff
|
Adding new switch to &if to relax the delay.
|
2013-09-16 22:50:39 -07:00 |
Alan Mishchenko
|
653dc8cff5
|
Added bridge integration for multi-output 'pdr -a'.
|
2013-09-16 14:46:07 -07:00 |
Alan Mishchenko
|
3b1cf0976c
|
Added bridge integration for multi-output 'pdr -a'.
|
2013-09-16 14:39:37 -07:00 |
Alan Mishchenko
|
ff5d3591d1
|
Infrastructure to support full Liberty format and unitification of library representations.
|
2013-09-15 18:23:49 -07:00 |
Alan Mishchenko
|
a4087e45f0
|
Enabling additional printouts in 'pdr'.
|
2013-09-13 17:36:29 -07:00 |
Alan Mishchenko
|
27be3d0185
|
Added command &struct for profiling non-dec structures.
|
2013-09-13 17:25:31 -07:00 |
Alan Mishchenko
|
dfb43b2f58
|
Fix a bug in 'zeropo'.
|
2013-09-13 09:52:54 -07:00 |
Alan Mishchenko
|
7312ff3c4a
|
Improvements to the new technology mapper.
|
2013-09-12 23:14:39 -07:00 |
Alan Mishchenko
|
75fee10708
|
Improvements to the new technology mapper.
|
2013-09-12 22:37:26 -07:00 |
Alan Mishchenko
|
14606c473e
|
Improvements to the new technology mapper.
|
2013-09-12 17:53:41 -07:00 |
Alan Mishchenko
|
b1b0202c05
|
Command '&slice' to cut out the bottom part of the AIG.
|
2013-09-11 14:38:08 -07:00 |
Alan Mishchenko
|
66b1d4de54
|
Small performance bug in new 'fx'.
|
2013-09-11 13:10:31 -07:00 |
Alan Mishchenko
|
0e256dc2c2
|
Updates for the new BMC engine.
|
2013-09-10 22:12:42 -07:00 |
Alan Mishchenko
|
8430b6dad4
|
New API to return the set of all reachable states as an AIG.
|
2013-09-10 14:51:47 -07:00 |
Alan Mishchenko
|
d4c70cb6c1
|
Updates for the new BMC engine.
|
2013-09-09 23:12:01 -07:00 |
Alan Mishchenko
|
48db1c3a04
|
Improvements to the new technology mapper.
|
2013-09-09 00:15:01 -07:00 |
Alan Mishchenko
|
00bc43982e
|
Improvements to the &ps.
|
2013-09-08 00:49:35 -07:00 |
Alan Mishchenko
|
5201509597
|
Improvements to the new technology mapper.
|
2013-09-07 18:49:32 -07:00 |
Alan Mishchenko
|
137a766207
|
Improvements to the new technology mapper.
|
2013-09-07 16:41:35 -07:00 |
Alan Mishchenko
|
23879f9200
|
Unifying parameters for the &ps command.
|
2013-09-05 20:40:50 -07:00 |
Alan Mishchenko
|
9d14b0c094
|
Updates for the new BMC engine.
|
2013-09-05 19:32:45 -07:00 |
Alan Mishchenko
|
8de1080272
|
Updates for the new BMC engine.
|
2013-09-05 15:54:52 -07:00 |
Alan Mishchenko
|
e9d0466494
|
Updates for the new BMC engine.
|
2013-09-05 15:39:18 -07:00 |
Alan Mishchenko
|
e651e22788
|
Adding check to &sim3 for the case when the AIG is combinational.
|
2013-09-05 12:57:55 -07:00 |
Alan Mishchenko
|
f53e56e822
|
Improved unrolling manager.
|
2013-09-05 01:44:44 -07:00 |
Alan Mishchenko
|
f591f1cd9a
|
Added Python API status_get_vector() similar to cex_get_vector().
|
2013-09-04 17:25:40 -07:00 |
Alan Mishchenko
|
30c2c48a65
|
Adding switch 'ps -s' to skip counting buffers/inverters as nodes.
|
2013-09-02 23:21:55 -07:00 |
Alan Mishchenko
|
d1b9ade535
|
Adding switch 'ps -s' to skip counting buffers/inverters as nodes.
|
2013-09-02 23:15:15 -07:00 |
Alan Mishchenko
|
b6cb626a12
|
Removing some old useless code.
|
2013-09-02 22:14:20 -07:00 |
Alan Mishchenko
|
e16e3edae8
|
Removing some old useless code.
|
2013-09-02 22:10:27 -07:00 |
Alan Mishchenko
|
9914c16868
|
Adding interpolant computation sat_solver2.
|
2013-09-02 15:14:49 -07:00 |
Alan Mishchenko
|
57b9a9fe13
|
Modify level computation to take discretized arrival times into account.
|
2013-09-02 11:07:05 -07:00 |
Alan Mishchenko
|
5023be4aa0
|
Adding switch &get -m to import mapped network into the &-space.
|
2013-09-01 19:37:47 -07:00 |
Alan Mishchenko
|
e2f11e14d0
|
Adding switch &get -m to import mapped network into the &-space.
|
2013-09-01 19:34:32 -07:00 |
Alan Mishchenko
|
a495163f74
|
Buf fixes and minor changes to the &if mapper.
|
2013-08-29 14:41:01 -07:00 |
Alan Mishchenko
|
1ad363c156
|
Added switch &sim -g to enable flop grouping.
|
2013-08-20 08:46:31 -07:00 |
Alan Mishchenko
|
3459683e3b
|
Extending 'permute' to handle user-specified flop permutation.
|
2013-08-16 13:13:38 -07:00 |
Alan Mishchenko
|
0916417e2e
|
Enabling LUT decomposition in two special cases.
|
2013-08-14 12:10:55 -07:00 |
Alan Mishchenko
|
ee1e20ddf8
|
Enabling additional matching feature in the LUT mapper.
|
2013-08-12 23:34:54 -07:00 |
Alan Mishchenko
|
fcfafb0601
|
Enabling additional matching feature in the LUT mapper.
|
2013-08-12 23:27:20 -07:00 |
Alan Mishchenko
|
d4ad3b4156
|
Improvements to buffering and sizing.
|
2013-08-09 19:47:58 -07:00 |
Alan Mishchenko
|
881b2ec46f
|
Integrated buffering and sizing.
|
2013-08-08 18:23:00 -07:00 |
Alan Mishchenko
|
8576e4b440
|
Improvements to buffering and sizing.
|
2013-08-06 22:51:39 -07:00 |
Alan Mishchenko
|
7a6f335ea6
|
Improvements to buffering and sizing.
|
2013-08-06 12:22:13 -07:00 |
Alan Mishchenko
|
1a55882ad9
|
Adding new (un)buffering with phase information.
|
2013-08-05 18:33:38 -07:00 |
Alan Mishchenko
|
f1615dccd5
|
Code for parsing the transcripts.
|
2013-08-02 23:15:37 -07:00 |
Alan Mishchenko
|
da60781c13
|
SAT solver with dynamic CNF loading.
|
2013-08-01 19:01:53 -07:00 |
Alan Mishchenko
|
f253e7aa41
|
Code for parsing the transcripts.
|
2013-07-30 21:48:02 -07:00 |
Alan Mishchenko
|
f10480f9bc
|
Parametrizing standard-cell mapper to account for the fanout delay.
|
2013-07-30 00:18:57 -07:00 |
Alan Mishchenko
|
f09a704250
|
Added commands 'maxsize' and 'unbuffer'.
|
2013-07-29 21:01:05 -07:00 |
Alan Mishchenko
|
675f2bbf2d
|
Compiler warning.
|
2013-07-29 19:13:09 -07:00 |
Alan Mishchenko
|
a206287b21
|
Adding support for input slew and output capacitance to timer and gate-sizer (bug fix).
|
2013-07-24 11:42:37 -07:00 |
Alan Mishchenko
|
00d023713b
|
Tuning standard-cell mapping flow.
|
2013-07-24 09:54:53 -07:00 |
Alan Mishchenko
|
84c0b9d69b
|
Tuning standard-cell mapping flow.
|
2013-07-23 16:15:03 -07:00 |
Alan Mishchenko
|
038f296453
|
Bug fix and warning print.
|
2013-07-22 23:11:04 -07:00 |
Alan Mishchenko
|
a9afe7e8b7
|
Improvements to post-mapping re-sizing.
|
2013-07-21 14:56:30 -07:00 |
Alan Mishchenko
|
710835f8d6
|
Memory leaks.
|
2013-07-21 01:28:54 -07:00 |
Alan Mishchenko
|
1ed823c67d
|
Adding support for input slew and output capacitance to timer and gate-sizer.
|
2013-07-21 01:01:53 -07:00 |
Alan Mishchenko
|
ab84c73eb0
|
Adding support for input slew (.input_drive) and output capacitance (.output_load) in BLIF reader/writer.
|
2013-07-21 00:15:24 -07:00 |
Alan Mishchenko
|
a35599960b
|
New technology mapper.
|
2013-07-18 13:03:01 -07:00 |
Alan Mishchenko
|
10c90de054
|
New technology mapper.
|
2013-07-17 14:19:33 -07:00 |
Alan Mishchenko
|
fce4605f58
|
Improved printout of XOR/MUX/AND in 'print_stats'.
|
2013-07-16 16:46:37 -07:00 |
Alan Mishchenko
|
5f97612951
|
Imporvements to 'eliminate'.
|
2013-07-16 16:06:21 -07:00 |
Alan Mishchenko
|
e731d3b1f4
|
Adding another network duplicator.
|
2013-07-16 00:44:51 -07:00 |
Alan Mishchenko
|
fd80bf20da
|
Adding another network duplicator.
|
2013-07-16 00:34:26 -07:00 |
Alan Mishchenko
|
f8f37d261b
|
New technology mapper.
|
2013-07-15 15:22:05 -07:00 |
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 |
Alan Mishchenko
|
6863688789
|
Enabled detecting CEXes in multiple POs without stopping (sim3 -a).
|
2013-01-23 12:37:44 +07:00 |
Alan Mishchenko
|
ac1207abea
|
Enabled detecting CEXes in multiple POs without stopping (sim3 -a).
|
2013-01-23 02:07:50 +07:00 |
Alan Mishchenko
|
1b6662ce4a
|
Fixing C++ compilation issues.
|
2013-01-08 14:16:59 +08:00 |
Alan Mishchenko
|
562b612691
|
Fixing C++ compilation issues.
|
2013-01-08 14:15:39 +08:00 |
Alan Mishchenko
|
a625caa17d
|
Fixing C++ compilation issues.
|
2013-01-08 13:56:20 +08:00 |
Alan Mishchenko
|
f26e760e9d
|
Fixing C++ compilation issues.
|
2013-01-08 13:33:17 +08:00 |
Alan Mishchenko
|
81a1d97079
|
Fixing C++ compilation issues.
|
2013-01-08 13:14:45 +08:00 |
Alan Mishchenko
|
a8dad4ed61
|
Fixing C++ compilation issues.
|
2013-01-08 13:12:28 +08:00 |
Alan Mishchenko
|
a0819f62ab
|
Adding support of flops to the conversion of MiniAIG into ABC network.
|
2013-01-08 06:42:25 +08:00 |
Alan Mishchenko
|
79f3ecb15f
|
Technology mapper.
|
2013-01-08 05:50:37 +08:00 |
Alan Mishchenko
|
e1a5556e8c
|
New unrolling manager.
|
2012-12-24 08:16:19 +07:00 |
Alan Mishchenko
|
bfad654205
|
Assembling timing/hierarchy manager from input data.
|
2012-12-15 17:39:34 -08:00 |
Alan Mishchenko
|
82050bbe11
|
Assembling timing/hierarchy manager from input data.
|
2012-12-13 15:18:53 -08:00 |
Alan Mishchenko
|
2575a5d683
|
Unifification of custom extensions.
|
2012-12-10 13:56:40 -08:00 |
Alan Mishchenko
|
f7b7ab59cf
|
Retiring old 'fpga' command and package.
|
2012-12-10 01:14:55 -08:00 |
Alan Mishchenko
|
dc843b03c9
|
Renaming If_Lut_t into If_LibLut_t.
|
2012-12-10 01:07:41 -08:00 |
Alan Mishchenko
|
5eedc74a15
|
Adding box library.
|
2012-12-10 00:59:54 -08:00 |
Alan Mishchenko
|
8355eb1d41
|
Enabling multi-output solving in 'pdr'.
|
2012-12-09 17:52:34 -08:00 |
Alan Mishchenko
|
ce63869fe7
|
Enabling multi-output solving in 'pdr'.
|
2012-12-09 17:33:44 -08:00 |
Alan Mishchenko
|
8761942258
|
Renaming multi-output mode enable switch 'bmc3 -s' to be 'bmc3 -a'.
|
2012-12-09 16:56:43 -08:00 |
Alan Mishchenko
|
9fc1cd0b3f
|
Enabling multi-output solving in 'pdr'.
|
2012-12-09 15:12:40 -08:00 |
Alan Mishchenko
|
58d4012a55
|
Enabling multi-output solving in 'pdr'.
|
2012-12-09 14:46:16 -08:00 |
Alan Mishchenko
|
9f396a0d7e
|
Enabling multi-output solving in 'pdr'.
|
2012-12-09 10:11:52 -08:00 |
Alan Mishchenko
|
b65ae7349a
|
Enabling multi-output solving in 'pdr'.
|
2012-12-09 09:47:48 -08:00 |
Alan Mishchenko
|
0058cefee3
|
Deriving CEX after phase/tempor/reparam.
|
2012-12-09 00:19:18 -08:00 |
Alan Mishchenko
|
a68593c4f2
|
Deriving CEX after phase/tempor/reparam.
|
2012-12-08 12:44:08 -08:00 |
Alan Mishchenko
|
8e5d771feb
|
Deriving CEX after phase/tempor/reparam.
|
2012-12-08 12:38:31 -08:00 |
Alan Mishchenko
|
f1749fa594
|
Enabling additional stat printouts.
|
2012-12-02 01:44:17 -08:00 |
Alan Mishchenko
|
4d67a04b19
|
Enabling additional stat printouts.
|
2012-12-02 01:25:53 -08:00 |
Alan Mishchenko
|
a797ea0cc7
|
Enabling additional stat printouts.
|
2012-12-02 00:00:29 -08:00 |
Alan Mishchenko
|
86fcba60c2
|
Enabling command &append for combiming multiple AIGs.
|
2012-12-01 23:13:24 -08:00 |
Alan Mishchenko
|
01bea8ef3a
|
Enabling additional stat printouts.
|
2012-12-01 22:16:22 -08:00 |
Alan Mishchenko
|
cd32ae50c4
|
Counter-example analysis and optimization.
|
2012-11-30 17:22:44 -08:00 |
Alan Mishchenko
|
f1a5288904
|
Counter-example analysis and optimization.
|
2012-11-30 11:38:05 -08:00 |
Alan Mishchenko
|
661265984c
|
Counter-example analysis and optimization.
|
2012-11-28 16:18:39 -08:00 |
Alan Mishchenko
|
b2fd119933
|
DSD manager.
|
2012-11-20 21:34:40 -08:00 |
Alan Mishchenko
|
ffbe3bc576
|
DSD manager.
|
2012-11-19 23:42:05 -08:00 |
Alan Mishchenko
|
a0052e22b4
|
Added switch 'cexcut -m' to generate bad states for all frames after G.
|
2012-11-15 16:00:29 -08:00 |
Alan Mishchenko
|
c2e467d55b
|
Added switch 'cexcut -n' to generate only one bad state.
|
2012-11-15 10:59:57 -08:00 |
Alan Mishchenko
|
2eb2402b01
|
Added command 'cexcut' and 'cexmerge'.
|
2012-11-14 20:50:18 -08:00 |
Alan Mishchenko
|
9173799c96
|
Added command 'cexcut' and 'cexmerge'.
|
2012-11-14 18:22:13 -08:00 |
Alan Mishchenko
|
be29f37baa
|
Added command 'cexcut' and 'cexmerge'.
|
2012-11-14 18:20:35 -08:00 |
Alan Mishchenko
|
9d5d804610
|
Added command 'cexcut' and 'cexmerge'.
|
2012-11-14 16:09:49 -08:00 |
Alan Mishchenko
|
d8e0403296
|
Added command 'cexsave' and 'cexload'.
|
2012-11-14 14:33:27 -08:00 |
Alan Mishchenko
|
be7a4e4259
|
Isolating BMC code into a separate package.
|
2012-11-14 13:55:24 -08:00 |
Alan Mishchenko
|
aba8ff4ba0
|
Modifying parameter limits to allow mapping into 2-LUTs.
|
2012-11-14 12:56:45 -08:00 |
Alan Mishchenko
|
30b8c3d422
|
Made print-out of frontier cut an option ('-c') in '&ps'.
|
2012-11-12 14:08:10 -08:00 |
Alan Mishchenko
|
566c7d7152
|
Extending GIA to represent pintypes and pins.
|
2012-11-12 13:57:51 -08:00 |
Alan Mishchenko
|
21e6a59ed8
|
Improved DSD.
|
2012-11-11 13:26:36 -08:00 |
Alan Mishchenko
|
ee789ba902
|
Improved DSD.
|
2012-11-10 19:37:53 -08:00 |
Alan Mishchenko
|
e0f27f5ac3
|
Improved DSD.
|
2012-11-10 17:26:01 -08:00 |
Alan Mishchenko
|
fdcbb2cf37
|
Performance bug fix in choice generation.
|
2012-11-09 12:43:03 -08:00 |
Alan Mishchenko
|
db7852bba7
|
Improvements to LMS code.
|
2012-11-06 18:04:23 -08:00 |
Alan Mishchenko
|
7ba37f4901
|
Improved DSD.
|
2012-11-03 00:38:17 -07:00 |
Alan Mishchenko
|
c899645b10
|
Adding dumping truth tables from LMS manager.
|
2012-11-02 18:59:14 -07:00 |
Alan Mishchenko
|
96d3348d8f
|
Fixing out-of-bound problem when collecting GIA nodes.
|
2012-11-02 12:02:16 -07:00 |
Alan Mishchenko
|
7a7173c80e
|
Improvements to LMS code.
|
2012-11-02 00:27:34 -07:00 |
Alan Mishchenko
|
bd7b55115f
|
Improvements to LMS code.
|
2012-11-02 00:06:56 -07:00 |
Alan Mishchenko
|
a20e32f9e3
|
Improvements to LMS code.
|
2012-11-01 22:03:37 -07:00 |
Alan Mishchenko
|
f23a17e0c6
|
Improvements to LMS code.
|
2012-11-01 16:24:36 -07:00 |