Alan Mishchenko
|
e881eaf693
|
Removing useless printout in &resim.
|
2011-03-02 18:48:51 -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
|
4704dbc798
|
Replaced remove() by unlink() to compile on Windows.
|
2011-02-27 20:43:02 -08:00 |
Baruch Sterin
|
34d59b0b91
|
fixes to pyabc kill mechanism
|
2011-02-27 18:33:56 -08:00 |
Alan Mishchenko
|
02081dba67
|
Added generation of counter-examples in &reachm.
|
2011-02-27 17:05:44 -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
|
a84b1cfc55
|
Fixed a critical bug in the previous update.
|
2011-02-21 21:32:28 -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
|
5b4ef503bd
|
Fixed Cudd_DumpDot() to not print leading zeros because of OS-dependent fprintf switch %p.
|
2011-02-16 12:21:58 -08:00 |
Baruch Sterin
|
9d02679ef7
|
fixes for dumb erros in utilSignal.c/h
|
2011-02-15 16:50:12 -08:00 |
Alan Mishchenko
|
a7e214bb01
|
Improved timeout in the BDD reachability engines.
|
2011-02-13 20:50:29 -08:00 |
Alan Mishchenko
|
573694f9bf
|
Fixing g++ compilation issue for tmpFile().
|
2011-02-13 19:48:30 -08:00 |
Alan Mishchenko
|
8cc7b43865
|
Unified the use of counter-examples in three packages (additional files).
|
2011-02-13 18:02:52 -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
|
8acd4edd5a
|
Removing 1.txt, which was added by mistake.
|
2011-02-13 13:43:14 -08:00 |
Alan Mishchenko
|
e7b544f111
|
Upgrade to the latest CUDD 2.4.2.
|
2011-02-13 13:42:25 -08:00 |
Alan Mishchenko
|
d99de60e6c
|
Portability changes to the st package.
|
2011-02-13 13:40:21 -08:00 |
Alan Mishchenko
|
350bedf53f
|
Minor change to the project file.
|
2011-02-13 13:39:56 -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
|
78aed3f6d5
|
LUT-size-based balancing (disabled by default).
|
2011-02-11 09:11:30 -08:00 |
Alan Mishchenko
|
2a214a9283
|
Bug fix in zeropo.
|
2011-02-11 09:10:34 -08:00 |
Alan Mishchenko
|
f74fb87dae
|
Improved timeout in &reachp.
|
2011-02-08 12:45:28 -08:00 |
Alan Mishchenko
|
ed253df750
|
Additional change to enable runtime limit in CUDD in variable reordering.
|
2011-02-08 12:43:32 -08:00 |
Alan Mishchenko
|
46075098da
|
Improved timeout in &reachm.
|
2011-02-08 11:36:02 -08:00 |
Alan Mishchenko
|
7977b2dd5d
|
Modificationd to CUDD to enable runtime-limit in variable reordering.
|
2011-02-08 11:09:12 -08:00 |
Alan Mishchenko
|
53217cdc8b
|
Yet another update to the runtime control in BDD operations.
|
2011-02-07 20:37:53 -08:00 |
Alan Mishchenko
|
21bb515b3c
|
Added handling runtime limit inside And and AndExist.
|
2011-02-07 15:58:29 -08:00 |
Alan Mishchenko
|
3e92b87362
|
Added timeout to &reachn.
|
2011-02-04 20:22:10 -08:00 |
Alan Mishchenko
|
82e9de9000
|
Eneabled writing/reading pAbc->nFrames into/from status files.
|
2011-02-04 00:07:21 -08:00 |
Alan Mishchenko
|
e5fb4fe550
|
Added writing signal names in AIGER writer for GIA package.
|
2011-02-03 22:11:47 -08:00 |
Alan Mishchenko
|
e6f8744777
|
Make PDR return the number of completed frames.
|
2011-02-03 21:34:46 -08:00 |
Alan Mishchenko
|
59d7455cf1
|
Minor changes while improving BDD-based reachability.
|
2011-02-03 13:05:01 -08:00 |
Alan Mishchenko
|
1d54983bc4
|
Minor changes to hash table and utilSignal.c.
|
2011-02-01 16:35:50 -08:00 |
Baruch Sterin
|
35e05b7e5a
|
merge pyabc changes into mainline
|
2011-02-01 16:19:38 -08:00 |
Baruch Sterin
|
3a41da37a2
|
src/misc/util/utilSignal.c
|
2011-02-01 15:54:01 -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 |
Alan Mishchenko
|
624af674a0
|
New code since Dec 2010.
|
2011-01-13 13:32:18 -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 |