Alan Mishchenko
|
6c01e8b9f0
|
Fixed a number of small bugs and memory leaks.
|
2011-03-27 14:17:12 -07:00 |
Alan Mishchenko
|
1ec437d04b
|
C++ compilation fixes.
|
2011-03-27 11:52:56 -07:00 |
Alan Mishchenko
|
4dcf8cee2d
|
Improvements in Vec_Vec_t.
|
2011-03-27 11:35:31 -07:00 |
Alan Mishchenko
|
2fe534b06c
|
Fixed memory leak.
|
2011-03-27 11:34:00 -07:00 |
Alan Mishchenko
|
3a6f8688e2
|
Added printing MFFC sizes and deriving TT from SOP.
|
2011-03-18 19:48:42 -07:00 |
Alan Mishchenko
|
813db6e74d
|
Procedure to convert AIG into a netowrk of NAND gates.
|
2011-03-17 11:40:33 -07:00 |
Alan Mishchenko
|
326e5da48a
|
Added new procedure and other small changes.
|
2011-03-16 21:33:02 -07:00 |
Alan Mishchenko
|
290ea10c9e
|
Exploring fanout cofactoring ideas...
|
2011-03-14 11:56:09 -07:00 |
Alan Mishchenko
|
92a1c5b58e
|
Several bug fixes and other improvements.
|
2011-03-12 19:44:38 -08:00 |
Alan Mishchenko
|
a4aaf110ad
|
Exploration of Sasao's decomposition and minor improvements.
|
2011-03-11 20:18:02 -08:00 |
Alan Mishchenko
|
759c6596a5
|
Bug alert message in 'fraig'.
|
2011-03-10 11:48:25 -08:00 |
Alan Mishchenko
|
aa31e011a8
|
Added generation of MFFC for the network (improvements).
|
2011-03-09 20:49:32 -08:00 |
Alan Mishchenko
|
e15362a816
|
Added generation of MFFC for the network.
|
2011-03-09 18:39:00 -08:00 |
Alan Mishchenko
|
35f90a777d
|
Mffc-based structural decomposition of the network and bug fixes in reordering package.
|
2011-03-08 20:07:52 -08:00 |
Alan Mishchenko
|
937979d9dd
|
Improvements to the interpolation command 'int'; change of default switch -t.
|
2011-03-08 20:05:09 -08:00 |
Alan Mishchenko
|
eabc42a2d8
|
Fixing a typo bug Vec_IntStart instead of Vec_IntAlloc.
|
2011-03-08 17:32:38 -08:00 |
Alan Mishchenko
|
5f69ce8b8d
|
Fixing a corner case bug in 'enlarge'.
|
2011-03-05 13:08:39 -08:00 |
Alan Mishchenko
|
87d39b40aa
|
Missing type cast after one of the previous changes.
|
2011-03-04 17:11:33 -08:00 |
Alan Mishchenko
|
ef89333774
|
Improved the speed of refinement algorithm in &abs_refine.
|
2011-03-04 16:59:28 -08:00 |
Alan Mishchenko
|
148a786b69
|
Made abc.h independent of CUDD and Extra.
|
2011-03-03 12:28:52 -08:00 |
Alan Mishchenko
|
88bdf467d8
|
Bug fix in dprove, adding command option -p.
|
2011-03-03 10:02:32 -08:00 |
Alan Mishchenko
|
de984d7f90
|
Fixing corner-case bugs in &srm -s.
|
2011-02-28 21:55:40 -08:00 |
Alan Mishchenko
|
6119f7068a
|
Cumulative update to BDD-based reachability, speeding up &reachm and other changes.
|
2011-02-28 14:52:51 -08:00 |
Alan Mishchenko
|
39839c3feb
|
Updated read_status/write_status to correctly handle the case of seq cex without regs.
|
2011-02-27 20:57:27 -08:00 |
Alan Mishchenko
|
2f874d27fc
|
Fixed the problem with filtered equivalences (&srm -sf and &equiv_mark -f).
|
2011-02-22 12:47:55 -08:00 |
Alan Mishchenko
|
75ee395f91
|
Implemented additional filtering of equivalences (&srm -sf).
|
2011-02-21 15:09:51 -08:00 |
Alan Mishchenko
|
ab75993d28
|
Moved two new APIs for reading/writing CEX from/into ABC from abc.c to mainFrame.c.
|
2011-02-19 16:53:11 -08:00 |
Alan Mishchenko
|
e3f88c81c6
|
Changes to support sequential verification with reduction without speculation.
|
2011-02-19 16:47:05 -08:00 |
Alan Mishchenko
|
2619edf8c0
|
Added two new APIs for reading/writing CEX from/into ABC.
|
2011-02-19 16:43:00 -08:00 |
Alan Mishchenko
|
443cc01782
|
Another corner-case bug in zeropo.
|
2011-02-19 13:24:21 -08:00 |
Alan Mishchenko
|
0656af22fd
|
Adding one more control switch to CEC commands (i)prove.
|
2011-02-19 11:51:20 -08:00 |
Alan Mishchenko
|
c7ebd93211
|
Improvements to CEC command iprove.
|
2011-02-18 22:19:45 -08:00 |
Alan Mishchenko
|
06ae1644b2
|
Fixing the problem with writing/reading bug-free depth in status files.
|
2011-02-17 09:18:07 -08:00 |
Alan Mishchenko
|
71cbf17e7f
|
Unified the use of counter-examples in three packages.
|
2011-02-13 17:46:48 -08:00 |
Alan Mishchenko
|
686d38d667
|
Changes to enable C++ compilation after recent modifications.
|
2011-02-13 15:16:10 -08:00 |
Alan Mishchenko
|
bef084bd9b
|
Bug fix in setting the number of finished frames when reading a status file.
|
2011-02-11 13:57:57 -08:00 |
Alan Mishchenko
|
2a214a9283
|
Bug fix in zeropo.
|
2011-02-11 09:10:34 -08:00 |
Alan Mishchenko
|
21bb515b3c
|
Added handling runtime limit inside And and AndExist.
|
2011-02-07 15:58:29 -08:00 |
Alan Mishchenko
|
82e9de9000
|
Eneabled writing/reading pAbc->nFrames into/from status files.
|
2011-02-04 00:07:21 -08:00 |
Alan Mishchenko
|
e6f8744777
|
Make PDR return the number of completed frames.
|
2011-02-03 21:34:46 -08:00 |
Baruch Sterin
|
35e05b7e5a
|
merge pyabc changes into mainline
|
2011-02-01 16:19:38 -08:00 |
Alan Mishchenko
|
d4291dab37
|
Cumulative changes of the last two weeks.
|
2011-02-01 15:47:55 -08:00 |
Baruch Sterin
|
b538a5fad0
|
1. Replace system() with a function that responds to SIGINT. 2. Add functions to cleanup temporary files on SIGINT. 3. Fix bugs related to signal handling.
|
2011-02-01 11:13:53 -08:00 |
Baruch Sterin
|
ab80b015a4
|
merge changes from main branch
|
2011-01-13 22:42:54 +02:00 |
Alan Mishchenko
|
ae4b51351c
|
Cumulative changes in the last few weeks.
|
2011-01-13 12:38:59 -08:00 |
Baruch Sterin
|
c85a763444
|
pyabc: make the SIGINT signal handler clean up by sending SIGINT to child processes registered by the python code. Also provide functions to block SIGINT and unblock it, to allow for critical sections where signals are blocked
|
2011-01-13 22:11:37 +02:00 |
Alan Mishchenko
|
2adc30f56b
|
Initial integration of PDR
|
2010-12-03 01:20:51 -08:00 |
Alan Mishchenko
|
c9a6252486
|
Fixing memory leak in LTL property handling code
|
2010-12-02 19:30:19 -08:00 |
Alan Mishchenko
|
c7bb89d1b9
|
An option to output verbose stats about timeframe sizes during unrolling
|
2010-11-29 01:45:48 -08:00 |
Alan Mishchenko
|
5a192f026f
|
Bug fix: alloing "dsat" to work on multi-output cones
|
2010-11-29 01:43:14 -08:00 |