Alan Mishchenko
|
f3bab3e479
|
Updated Makefile as suggested by Mark Jarvin.
|
2013-05-19 22:15:55 -07:00 |
Alan Mishchenko
|
1e34a38b16
|
g++ warnings.
|
2013-05-19 22:14:50 -07:00 |
Alan Mishchenko
|
6ad94cd988
|
Making changes suggested by Mark Jarvin.
|
2013-05-19 21:50:09 -07:00 |
Alan Mishchenko
|
232fe09ee4
|
Bug fix in &frames.
|
2013-05-19 21:27:23 -07:00 |
Alan Mishchenko
|
6682d6b0e7
|
Bug fix in &mprove.
|
2013-05-19 12:22:03 -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
|
2a71e3e719
|
Potential improvement to &scorr.
|
2013-05-18 22:17:24 -07:00 |
Alan Mishchenko
|
68e1a07fdb
|
Improvements to 'bmc3'.
|
2013-05-18 17:31:23 -07:00 |
Alan Mishchenko
|
29a995685d
|
SAT variable profiling.
|
2013-05-18 15:02:26 -07:00 |
Alan Mishchenko
|
dfcdffe4be
|
Fixed gap timeout in 'pdr'.
|
2013-05-18 13:22:05 -07:00 |
Alan Mishchenko
|
c83e1d906a
|
SAT variable profiling.
|
2013-05-18 12:35:29 -07:00 |
Alan Mishchenko
|
5766472bb6
|
SAT variable profiling.
|
2013-05-18 11:30:13 -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
|
0328488bdf
|
SAT variable profiling.
|
2013-05-18 10:52:07 -07:00 |
Alan Mishchenko
|
29ee997bb9
|
SAT variable profiling (undo).
|
2013-05-18 00:35:21 -07:00 |
Alan Mishchenko
|
66ff650f48
|
SAT variable profiling.
|
2013-05-18 00:34:37 -07:00 |
Alan Mishchenko
|
84b3b91447
|
SAT variable profiling (undo).
|
2013-05-18 00:33:18 -07:00 |
Alan Mishchenko
|
86e38c2a36
|
SAT variable profiling.
|
2013-05-18 00:31:06 -07:00 |
Alan Mishchenko
|
92dcffcfb8
|
Adding support of XOR/MUX in GIA.
|
2013-05-17 17:09:29 -07:00 |
Alan Mishchenko
|
2afef15a1e
|
Adding support of XOR/MUX in GIA.
|
2013-05-17 17:06:27 -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
|
1dd80e1cfa
|
Bug fix in the timeout mechanism of 'pdr'.
|
2013-05-17 08:38:46 -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
|
7bcd75d80a
|
SAT sweeping under constraints (bug fix).
|
2013-05-12 10:19:33 -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
|
964c5cd5df
|
Typo in the comment.
|
2013-05-09 12:23:50 -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
|
68566713da
|
Bug fix in the sweeper.
|
2013-05-08 10:24:00 -07:00 |
Alan Mishchenko
|
e7e21b00fe
|
Bug fix in the sweeper.
|
2013-05-07 20:48:05 -07:00 |
Alan Mishchenko
|
027dbbd492
|
Making fanin ordering available for netlists, not only networks.
|
2013-05-07 18:57:40 -07:00 |
Alan Mishchenko
|
ccf3caddb8
|
Bug fix in 'blockpo'.
|
2013-05-07 18:39:24 -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
|
f321b27bb7
|
SAT sweeping under constraints.
|
2013-05-06 00:44:21 -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
|
a1ceb7617c
|
Making changes suggested by Mark Jarvin.
|
2013-05-05 09:06:53 -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 |