Alan Mishchenko
|
fbd6a08e73
|
Other changes to enable new features in the mapper (bug fix).
|
2011-07-16 17:49:35 +07:00 |
Alan Mishchenko
|
302f7d7a97
|
Other changes to enable new features in the mapper (bug fix).
|
2011-07-15 18:50:58 +07:00 |
Alan Mishchenko
|
96e44e313e
|
Other changes to enable new features in the mapper (bug fix).
|
2011-07-15 12:27:40 +07:00 |
Alan Mishchenko
|
6a020d6f69
|
Added switch to PDR to disable expensive generalization step.
|
2011-07-13 15:13:08 +07:00 |
Alan Mishchenko
|
669f390c6d
|
Other changes to enable new features in the mapper (bug fix).
|
2011-07-13 12:48:51 +07:00 |
Alan Mishchenko
|
73702835c6
|
Added equivalence class computation for flop outputs only in &equiv2.
|
2011-07-13 10:13:24 +07:00 |
Alan Mishchenko
|
204fac4dca
|
Other changes to enable new features in the mapper.
|
2011-07-10 13:56:05 +07:00 |
Alan Mishchenko
|
ebfd70cdf4
|
Initial changes to enable new features in the mapper
|
2011-07-08 19:40:07 -07:00 |
Alan Mishchenko
|
a37de7cc4d
|
Printing out the path/name of the resource file that is being sourced.
|
2011-07-02 17:17:55 -07:00 |
Alan Mishchenko
|
10953634c9
|
Fixing a typo, which led to not printing delay in 'ps' after SC mapping.
|
2011-07-02 17:05:14 -07:00 |
Alan Mishchenko
|
f866920eb5
|
Added a new demitering feature for dual-output miters.
|
2011-07-02 13:58:12 -07:00 |
Alan Mishchenko
|
6c2ac7661d
|
Added another specialized check to the mapper.
|
2011-06-27 20:17:52 -07:00 |
Alan Mishchenko
|
0985eaca6c
|
Updated 'iprove' to generate seq CEX when CEC fails (small fix).
|
2011-06-25 09:48:23 -07:00 |
Alan Mishchenko
|
49869d08ec
|
Merged two last changes.
|
2011-06-25 09:45:04 -07:00 |
Alan Mishchenko
|
15cc374fe3
|
Updated 'iprove' to generate seq CEX when CEC fails.
|
2011-06-25 09:23:44 -07:00 |
Alan Mishchenko
|
5b639818e9
|
Added dumping CEXes in AIGER format.
|
2011-06-21 19:54:31 -07:00 |
Alan Mishchenko
|
4669839b24
|
Added new mapping feature.
|
2011-06-20 22:23:32 -07:00 |
Alan Mishchenko
|
6fd29922d3
|
Added permute/unpermute.
|
2011-06-20 13:16:23 -07:00 |
Alan Mishchenko
|
3b77f2d16d
|
Added permute/unpermute.
|
2011-06-20 13:14:51 -07:00 |
Alan Mishchenko
|
51134ab81c
|
Disabled duplication of the network while removing POs in 'zeropo'.
|
2011-06-15 23:18:51 -07:00 |
Alan Mishchenko
|
68c79ee879
|
Added command &filter to filter equiv classes.
|
2011-06-15 00:31:11 -07:00 |
Alan Mishchenko
|
dcd95cac6f
|
Disabled duplication of the network while removing POs in 'removepo'.
|
2011-06-14 23:02:34 -07:00 |
Alan Mishchenko
|
b2dfa01370
|
Adding command 'srm2' (additional feature).
|
2011-06-08 11:34:51 -07:00 |
Alan Mishchenko
|
11f684c04d
|
Adding command 'srm2'.
|
2011-06-08 09:25:32 -07:00 |
Alan Mishchenko
|
bfbbfadfc4
|
Adding command 'srm2'.
|
2011-06-08 09:23:31 -07:00 |
Alan Mishchenko
|
ddb34e871c
|
Adding command 'removepo'.
|
2011-06-03 18:16:08 -07:00 |
Alan Mishchenko
|
3bdce84c5b
|
Bug fix in 'swappos'.
|
2011-06-03 17:54:12 -07:00 |
Alan Mishchenko
|
31360734b7
|
Added new command 'outdec'.
|
2011-05-19 11:43:11 +07:00 |
Alan Mishchenko
|
27311713c7
|
Special BLIF writing (bug fixes).
|
2011-05-18 15:03:19 +07:00 |
Alan Mishchenko
|
26fb1fcd14
|
Special BLIF writing.
|
2011-05-18 13:35:35 +07:00 |
Alan Mishchenko
|
3c7842be32
|
Improvements to timeout.
|
2011-05-11 22:14:12 +08:00 |
Alan Mishchenko
|
57daeee997
|
Updated technology mapping.
|
2011-05-08 00:22:32 -07:00 |
Alan Mishchenko
|
27bb2a684d
|
Updated technology mapping.
|
2011-05-07 20:19:45 -07:00 |
Alan Mishchenko
|
b8b75cf14f
|
Improvements in sequential verification.
|
2011-05-07 18:21:50 -07:00 |
Alan Mishchenko
|
e2e3f6a228
|
Improvements in sequential verification.
|
2011-05-06 20:33:06 -07:00 |
Alan Mishchenko
|
a0cc621566
|
Trying to fix a mysterious bug in reading the library files.
|
2011-05-06 19:27:00 -07:00 |
Alan Mishchenko
|
2140c5d980
|
Updating testcext to ignore the diff in register count and other things.
|
2011-05-01 15:36:39 -07:00 |
Alan Mishchenko
|
e4d0f4715a
|
Added new options to testcex.
|
2011-04-28 09:56:14 -04:00 |
Alan Mishchenko
|
631b50aa59
|
Commented out debug messages.
|
2011-04-26 22:56:04 -04:00 |
Alan Mishchenko
|
970200b932
|
Made testcex reset the number of the PO that failed.
|
2011-04-25 12:35:05 -05:00 |
Alan Mishchenko
|
3eae30a3c3
|
Added support for AIG returned in the output file.
|
2011-04-24 14:40:36 -07:00 |
Alan Mishchenko
|
affb43e2a3
|
Added switch to control duplication of logic after mapping.
|
2011-04-24 10:43:24 -07:00 |
Alan Mishchenko
|
2becb24a32
|
Bug fixes having to do with the use of chars.
|
2011-04-20 23:15:05 -07:00 |
Alan Mishchenko
|
d5555c51f0
|
Fixing c++ portability issues.
|
2011-04-20 00:27:35 -07:00 |
Alan Mishchenko
|
d8647f0b7b
|
Fixing compilation problem which resulting from defining 'int c' as 'char c'.
|
2011-04-19 23:16:12 -07:00 |
Alan Mishchenko
|
05b61206e4
|
Adding constant correspondence.
|
2011-04-18 23:27:51 -07:00 |
Alan Mishchenko
|
7bcd5ac979
|
Changes to incorporate AIG parsing in memory and user-specified PI/PO/FF numbers.
|
2011-04-17 19:11:57 -07:00 |
Alan Mishchenko
|
0aefe77ea5
|
Added command 'reconcile'.
|
2011-04-16 22:49:14 -07:00 |
Alan Mishchenko
|
ddd9758931
|
Added cex generation for clustered reachability (forgot one file).
|
2011-04-16 00:09:39 -07:00 |
Alan Mishchenko
|
dd71ca94f1
|
Added cex generation for clustered reachability.
|
2011-04-16 00:08:43 -07:00 |
Alan Mishchenko
|
813245b29a
|
Improving timeout in the interpolation package.
|
2011-04-15 09:29:13 -07:00 |
Alan Mishchenko
|
4635027478
|
Further improvements to reachability.
|
2011-04-15 00:06:54 -07:00 |
Alan Mishchenko
|
75e60ab2ee
|
Experiments with reachability.
|
2011-04-14 09:57:35 -07:00 |
Alan Mishchenko
|
6e74c46bcf
|
Enabled new BDD-based reachability engine 'reachy'.
|
2011-04-13 22:41:54 -07:00 |
Alan Mishchenko
|
8b22fd2856
|
Added print-out of area in terms of LUT library.
|
2011-04-13 08:24:35 -07:00 |
Alan Mishchenko
|
5222f382af
|
Adding SAT-solver-level timeouts to the BMC engines.
|
2011-04-08 15:35:59 -07:00 |
Alan Mishchenko
|
a28fe0d324
|
Unsuccessful attempt to improve PDR and a few minor changes.
|
2011-04-07 13:49:03 -07:00 |
Alan Mishchenko
|
1794bd37cd
|
Made gate library package Mio independent of CUDD.
|
2011-03-30 21:02:29 -07:00 |
Alan Mishchenko
|
02f7ede7c6
|
Added test package (new files).
|
2011-03-29 19:11:34 -07:00 |
Alan Mishchenko
|
2b336851a2
|
Added test package.
|
2011-03-29 13:04:21 -07:00 |
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 |
Alan Mishchenko
|
92420c2d1f
|
Rearranging data members in the structure (not a bug)
|
2010-11-29 01:37:13 -08:00 |
Alan Mishchenko
|
719d399a64
|
Bug fix to read flops with init state 3 (don't know)
|
2010-11-29 01:30:03 -08:00 |
Alan Mishchenko
|
0c337bc344
|
Added API Abc_FrameReadGia
|
2010-11-29 01:15:16 -08:00 |
Alan Mishchenko
|
584643747c
|
Fix for write_status/read_status to use PO index
|
2010-11-29 01:08:18 -08:00 |
Alan Mishchenko
|
c2c9a5cf8d
|
Added command "swappos".
|
2010-11-28 22:44:54 -08:00 |
Alan Mishchenko
|
a17a4e5ca4
|
NPN class computation.
|
2010-11-28 22:30:15 -08:00 |
Alan Mishchenko
|
98257daa82
|
Added command "testcex".
|
2010-11-28 19:32:19 -08:00 |
Alan Mishchenko
|
6130e39b18
|
initial commit of public abc
|
2010-11-01 01:35:04 -07:00 |
Alan Mishchenko
|
51a646a355
|
Version abc90901
committer: Baruch Sterin <baruchs@gmail.com>
|
2015-06-22 23:05:13 -07:00 |
Alan Mishchenko
|
3270783939
|
Version abc90813
committer: Baruch Sterin <baruchs@gmail.com>
|
2015-06-22 23:05:09 -07:00 |
Alan Mishchenko
|
4d1bc4a268
|
Version abc90809
committer: Baruch Sterin <baruchs@gmail.com>
|
2015-06-22 23:05:06 -07:00 |
Alan Mishchenko
|
b288bac6b3
|
Version abc90807
committer: Baruch Sterin <baruchs@gmail.com>
|
2015-06-22 23:05:02 -07:00 |
Alan Mishchenko
|
da65e88e3b
|
Version abc90804
committer: Baruch Sterin <baruchs@gmail.com>
|
2015-06-22 23:04:59 -07:00 |
Alan Mishchenko
|
270f6db246
|
Version abc90715
committer: Baruch Sterin <baruchs@gmail.com>
|
2015-06-22 23:04:56 -07:00 |
Alan Mishchenko
|
0398ced824
|
Version abc90714
committer: Baruch Sterin <baruchs@gmail.com>
|
2015-06-22 23:04:53 -07:00 |
Alan Mishchenko
|
70697f868a
|
Version abc90528
committer: Baruch Sterin <baruchs@gmail.com>
|
2015-06-22 23:04:43 -07:00 |
Alan Mishchenko
|
d5b0fdee74
|
Version abc90505
|
2009-05-05 08:01:00 -07:00 |
Alan Mishchenko
|
d7a048d738
|
Version abc90424
|
2009-04-24 08:01:00 -07:00 |
Alan Mishchenko
|
77fab468ad
|
Version abc90413
|
2009-04-13 08:01:00 -07:00 |
Alan Mishchenko
|
ccd1b57264
|
Version abc90410
|
2009-04-10 08:01:00 -07:00 |
Alan Mishchenko
|
df6fdd1dff
|
Version abc90408
|
2009-04-08 08:01:00 -07:00 |
Alan Mishchenko
|
e3e2918eb8
|
Version abc90405
|
2009-04-05 08:01:00 -07:00 |
Alan Mishchenko
|
23fd11037a
|
Version abc90329
|
2009-03-29 08:01:00 -07:00 |
Alan Mishchenko
|
d74d35aa42
|
Version abc90321
|
2009-03-21 08:01:00 -07:00 |
Alan Mishchenko
|
770bc99e79
|
Version abc90315
|
2009-03-15 08:01:00 -07:00 |
Alan Mishchenko
|
81b51657f5
|
Version abc90313
|
2009-03-13 08:01:00 -07:00 |
Alan Mishchenko
|
243cb29e56
|
Version abc90311
|
2009-03-11 08:01:00 -07:00 |
Alan Mishchenko
|
32314347ba
|
Version abc90310
|
2009-03-10 08:01:00 -07:00 |
Alan Mishchenko
|
c03f9b516b
|
Version abc90220
|
2009-02-20 08:01:00 -08:00 |
Alan Mishchenko
|
28d4f8696d
|
Version abc90217
|
2009-02-17 08:01:00 -08:00 |
Alan Mishchenko
|
0871bffae3
|
Version abc90215
|
2009-02-15 08:01:00 -08:00 |
Alan Mishchenko
|
f936cc0680
|
Version abc90118
|
2009-01-18 08:01:00 -08:00 |
Alan Mishchenko
|
c9ad5880cc
|
Version abc81029
|
2008-10-29 08:01:00 -07:00 |
Alan Mishchenko
|
d80ee832f3
|
Version abc81027
|
2008-10-27 08:01:00 -07:00 |
Alan Mishchenko
|
d2b735f794
|
Version abc81025
|
2008-10-25 08:01:00 -07:00 |
Alan Mishchenko
|
2418d9b08d
|
Version abc81014_2
|
2008-10-14 20:01:00 -07:00 |
Alan Mishchenko
|
a4bca40597
|
Version abc81014
|
2008-10-14 08:01:00 -07:00 |
Alan Mishchenko
|
e917dda1d3
|
Version abc81013
|
2008-10-13 08:01:00 -07:00 |
Alan Mishchenko
|
a2535d49a0
|
Version abc81005
|
2008-10-05 08:01:00 -07:00 |
Alan Mishchenko
|
eb75697fe0
|
Version abc81004
|
2008-10-04 08:01:00 -07:00 |